Step | Hyp | Ref
| Expression |
1 | | 1re 10039 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
2 | | elicopnf 12269 |
. . . . . . . . . . 11
⊢ (1 ∈
ℝ → (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 1
≤ 𝑥)) |
4 | 3 | simplbi 476 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
𝑥 ∈
ℝ) |
5 | | 0red 10041 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) → 0
∈ ℝ) |
6 | | 1red 10055 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) → 1
∈ ℝ) |
7 | | 0lt1 10550 |
. . . . . . . . . . 11
⊢ 0 <
1 |
8 | 7 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) → 0
< 1) |
9 | 3 | simprbi 480 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) → 1
≤ 𝑥) |
10 | 5, 6, 4, 8, 9 | ltletrd 10197 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) → 0
< 𝑥) |
11 | 4, 10 | elrpd 11869 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) →
𝑥 ∈
ℝ+) |
12 | 11 | ssriv 3607 |
. . . . . . 7
⊢
(1[,)+∞) ⊆ ℝ+ |
13 | 12 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (1[,)+∞) ⊆ ℝ+) |
14 | | rpssre 11843 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
15 | 13, 14 | syl6ss 3615 |
. . . . 5
⊢ (⊤
→ (1[,)+∞) ⊆ ℝ) |
16 | 15 | resmptd 5452 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
17 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛)) |
18 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑚 − 1) = (𝑛 − 1)) |
19 | 18 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1))) |
20 | 19, 18 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) |
21 | 17, 20 | jca 554 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((1 / 𝑚) = (1 / 𝑛) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) |
22 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (1 / 𝑚) = (1 / (𝑛 + 1))) |
23 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → (𝑚 − 1) = ((𝑛 + 1) − 1)) |
24 | 23 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) −
1))) |
25 | 24, 23 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) =
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) |
26 | 22, 25 | jca 554 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → ((1 / 𝑚) = (1 / (𝑛 + 1)) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) =
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)))) |
27 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 1 → (1 / 𝑚) = (1 / 1)) |
28 | | 1div1e1 10717 |
. . . . . . . . . . . . 13
⊢ (1 / 1) =
1 |
29 | 27, 28 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (1 / 𝑚) = 1) |
30 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) |
31 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . . 17
⊢ (1
− 1) = 0 |
32 | 30, 31 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) |
33 | 32 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) =
(ψ‘0)) |
34 | | 2pos 11112 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
2 |
35 | | 0re 10040 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ |
36 | | chpeq0 24933 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
ℝ → ((ψ‘0) = 0 ↔ 0 < 2)) |
37 | 35, 36 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
((ψ‘0) = 0 ↔ 0 < 2) |
38 | 34, 37 | mpbir 221 |
. . . . . . . . . . . . . . 15
⊢
(ψ‘0) = 0 |
39 | 33, 38 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) =
0) |
40 | 39, 32 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = (0 −
0)) |
41 | | 0m0e0 11130 |
. . . . . . . . . . . . 13
⊢ (0
− 0) = 0 |
42 | 40, 41 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) =
0) |
43 | 29, 42 | jca 554 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → ((1 / 𝑚) = 1 ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) =
0)) |
44 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (1 / 𝑚) = (1 / ((⌊‘𝑥) + 1))) |
45 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑚 − 1) =
(((⌊‘𝑥) + 1)
− 1)) |
46 | 45 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ((⌊‘𝑥) + 1) →
(ψ‘(𝑚 − 1))
= (ψ‘(((⌊‘𝑥) + 1) − 1))) |
47 | 46, 45 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑚 = ((⌊‘𝑥) + 1) →
((ψ‘(𝑚 −
1)) − (𝑚 − 1))
= ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) |
48 | 44, 47 | jca 554 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((1 / 𝑚) = (1 / ((⌊‘𝑥) + 1)) ∧
((ψ‘(𝑚 −
1)) − (𝑚 − 1))
= ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1)))) |
49 | 11 | rprege0d 11879 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) →
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
50 | | flge0nn0 12621 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1[,)+∞) →
(⌊‘𝑥) ∈
ℕ0) |
52 | | nn0p1nn 11332 |
. . . . . . . . . . . . 13
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
((⌊‘𝑥) + 1)
∈ ℕ) |
54 | | nnuz 11723 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
55 | 53, 54 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
((⌊‘𝑥) + 1)
∈ (ℤ≥‘1)) |
56 | | elfznn 12370 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈
(1...((⌊‘𝑥) +
1)) → 𝑚 ∈
ℕ) |
57 | 56 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℕ) |
58 | 57 | nnrecred 11066 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (1 / 𝑚) ∈
ℝ) |
59 | 58 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (1 / 𝑚) ∈
ℂ) |
60 | 57 | nnred 11035 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℝ) |
61 | | peano2rem 10348 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℝ → (𝑚 − 1) ∈
ℝ) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (𝑚 − 1)
∈ ℝ) |
63 | | chpcl 24850 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 − 1) ∈ ℝ
→ (ψ‘(𝑚
− 1)) ∈ ℝ) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (ψ‘(𝑚
− 1)) ∈ ℝ) |
65 | 64, 62 | resubcld 10458 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℝ) |
66 | 65 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℂ) |
67 | 21, 26, 43, 48, 55, 59, 66 | fsumparts 14538 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))((1 / 𝑛) ·
(((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = ((((1 /
((⌊‘𝑥) + 1))
· ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) − (1 · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))))) |
68 | 4 | flcld 12599 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1[,)+∞) →
(⌊‘𝑥) ∈
ℤ) |
69 | | fzval3 12536 |
. . . . . . . . . . . . 13
⊢
((⌊‘𝑥)
∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
(1...(⌊‘𝑥)) =
(1..^((⌊‘𝑥) +
1))) |
71 | 70 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
(1..^((⌊‘𝑥) +
1)) = (1...(⌊‘𝑥))) |
72 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
73 | 72 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
74 | 73 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℂ) |
75 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ |
76 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
77 | 74, 75, 76 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
= 𝑛) |
78 | 73 | nnred 11035 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ) |
79 | 77, 78 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
∈ ℝ) |
80 | | chpcl 24850 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 + 1) − 1) ∈ ℝ
→ (ψ‘((𝑛 +
1) − 1)) ∈ ℝ) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) ∈ ℝ) |
82 | 81 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) ∈ ℂ) |
83 | 79 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
∈ ℂ) |
84 | | peano2rem 10348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) |
85 | 78, 84 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℝ) |
86 | | chpcl 24850 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 − 1) ∈ ℝ
→ (ψ‘(𝑛
− 1)) ∈ ℝ) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑛
− 1)) ∈ ℝ) |
88 | 87 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑛
− 1)) ∈ ℂ) |
89 | | 1cnd 10056 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℂ) |
90 | 74, 89 | subcld 10392 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℂ) |
91 | 82, 83, 88, 90 | sub4d 10441 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((ψ‘((𝑛 +
1) − 1)) − ((𝑛
+ 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = (((ψ‘((𝑛 + 1) − 1)) −
(ψ‘(𝑛 −
1))) − (((𝑛 + 1)
− 1) − (𝑛
− 1)))) |
92 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
93 | 73, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℕ0) |
94 | | chpp1 24881 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 − 1) ∈
ℕ0 → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) +
(Λ‘((𝑛 −
1) + 1)))) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛
− 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) +
1)))) |
96 | | npcan 10290 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
97 | 74, 75, 96 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 − 1) + 1)
= 𝑛) |
98 | 97, 77 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 − 1) + 1)
= ((𝑛 + 1) −
1)) |
99 | 98 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛
− 1) + 1)) = (ψ‘((𝑛 + 1) − 1))) |
100 | 97 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘((𝑛
− 1) + 1)) = (Λ‘𝑛)) |
101 | 100 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑛
− 1)) + (Λ‘((𝑛 − 1) + 1))) = ((ψ‘(𝑛 − 1)) +
(Λ‘𝑛))) |
102 | 95, 99, 101 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛))) |
103 | 102 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘((𝑛 +
1) − 1)) − (ψ‘(𝑛 − 1))) = (((ψ‘(𝑛 − 1)) +
(Λ‘𝑛)) −
(ψ‘(𝑛 −
1)))) |
104 | | vmacl 24844 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
105 | 73, 104 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
106 | 105 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℂ) |
107 | 88, 106 | pncan2d 10394 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((ψ‘(𝑛
− 1)) + (Λ‘𝑛)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛)) |
108 | 103, 107 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘((𝑛 +
1) − 1)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛)) |
109 | | peano2cn 10208 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℂ → (𝑛 + 1) ∈
ℂ) |
110 | 74, 109 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 + 1) ∈
ℂ) |
111 | 110, 74, 89 | nnncan2d 10427 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) − 1)
− (𝑛 − 1)) =
((𝑛 + 1) − 𝑛)) |
112 | | pncan2 10288 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 𝑛) =
1) |
113 | 74, 75, 112 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) −
𝑛) = 1) |
114 | 111, 113 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) − 1)
− (𝑛 − 1)) =
1) |
115 | 108, 114 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((ψ‘((𝑛 +
1) − 1)) − (ψ‘(𝑛 − 1))) − (((𝑛 + 1) − 1) − (𝑛 − 1))) = ((Λ‘𝑛) − 1)) |
116 | 91, 115 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((ψ‘((𝑛 +
1) − 1)) − ((𝑛
+ 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = ((Λ‘𝑛) − 1)) |
117 | 116 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 / 𝑛) ·
(((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = ((1 / 𝑛) · ((Λ‘𝑛) − 1))) |
118 | | peano2rem 10348 |
. . . . . . . . . . . . . . 15
⊢
((Λ‘𝑛)
∈ ℝ → ((Λ‘𝑛) − 1) ∈ ℝ) |
119 | 105, 118 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
− 1) ∈ ℝ) |
120 | 119 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
− 1) ∈ ℂ) |
121 | 73 | nnne0d 11065 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ≠
0) |
122 | 120, 74, 121 | divrec2d 10805 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
− 1) / 𝑛) = ((1 /
𝑛) ·
((Λ‘𝑛) −
1))) |
123 | 117, 122 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 / 𝑛) ·
(((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = (((Λ‘𝑛) − 1) / 𝑛)) |
124 | 71, 123 | sumeq12rdv 14438 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))((1 / 𝑛) ·
(((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) |
125 | 51 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (1[,)+∞) →
(⌊‘𝑥) ∈
ℂ) |
126 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⌊‘𝑥)
∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑥) + 1) − 1) =
(⌊‘𝑥)) |
127 | 125, 75, 126 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (1[,)+∞) →
(((⌊‘𝑥) + 1)
− 1) = (⌊‘𝑥)) |
128 | 127 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘(((⌊‘𝑥) + 1) − 1)) =
(ψ‘(⌊‘𝑥))) |
129 | | chpfl 24876 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ →
(ψ‘(⌊‘𝑥)) = (ψ‘𝑥)) |
130 | 4, 129 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘(⌊‘𝑥)) = (ψ‘𝑥)) |
131 | 128, 130 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘𝑥)) |
132 | 131 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1)) = ((ψ‘𝑥) − (((⌊‘𝑥) + 1) − 1))) |
133 | | chpcl 24850 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
134 | 4, 133 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘𝑥) ∈
ℝ) |
135 | 134 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘𝑥) ∈
ℂ) |
136 | 53 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1[,)+∞) →
((⌊‘𝑥) + 1)
∈ ℂ) |
137 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1[,)+∞) → 1
∈ ℂ) |
138 | 135, 136,
137 | subsub3d 10422 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘𝑥) −
(((⌊‘𝑥) + 1)
− 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) |
139 | 132, 138 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) |
140 | 139 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) = ((1 / ((⌊‘𝑥) + 1)) · (((ψ‘𝑥) + 1) −
((⌊‘𝑥) +
1)))) |
141 | 53 | nnrecred 11066 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) → (1
/ ((⌊‘𝑥) + 1))
∈ ℝ) |
142 | 141 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) → (1
/ ((⌊‘𝑥) + 1))
∈ ℂ) |
143 | | peano2cn 10208 |
. . . . . . . . . . . . . . . 16
⊢
((ψ‘𝑥)
∈ ℂ → ((ψ‘𝑥) + 1) ∈ ℂ) |
144 | 135, 143 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘𝑥) + 1)
∈ ℂ) |
145 | 142, 144,
136 | subdid 10486 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) = (((1 /
((⌊‘𝑥) + 1))
· ((ψ‘𝑥) +
1)) − ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1)))) |
146 | 53 | nnne0d 11065 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1[,)+∞) →
((⌊‘𝑥) + 1)
≠ 0) |
147 | 144, 136,
146 | divrec2d 10805 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) →
(((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1)) =
((1 / ((⌊‘𝑥) +
1)) · ((ψ‘𝑥) + 1))) |
148 | 147 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · ((ψ‘𝑥) + 1)) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) |
149 | 136, 146 | recid2d 10797 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · ((⌊‘𝑥) + 1)) = 1) |
150 | 148, 149 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) →
(((1 / ((⌊‘𝑥) +
1)) · ((ψ‘𝑥) + 1)) − ((1 / ((⌊‘𝑥) + 1)) ·
((⌊‘𝑥) + 1))) =
((((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
− 1)) |
151 | 140, 145,
150 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) |
152 | 75 | mul01i 10226 |
. . . . . . . . . . . . . 14
⊢ (1
· 0) = 0 |
153 | 152 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1[,)+∞) → (1
· 0) = 0) |
154 | 151, 153 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
(((1 / ((⌊‘𝑥) +
1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) − (1 · 0)) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) −
0)) |
155 | | peano2re 10209 |
. . . . . . . . . . . . . . . . 17
⊢
((ψ‘𝑥)
∈ ℝ → ((ψ‘𝑥) + 1) ∈ ℝ) |
156 | 134, 155 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘𝑥) + 1)
∈ ℝ) |
157 | 156, 53 | nndivred 11069 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) →
(((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
∈ ℝ) |
158 | 157 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) →
(((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
∈ ℂ) |
159 | | subcl 10280 |
. . . . . . . . . . . . . 14
⊢
(((((ψ‘𝑥)
+ 1) / ((⌊‘𝑥) +
1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈
ℂ) |
160 | 158, 75, 159 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1[,)+∞) →
((((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
− 1) ∈ ℂ) |
161 | 160 | subid1d 10381 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
(((((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
− 1) − 0) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) |
162 | 154, 161 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
(((1 / ((⌊‘𝑥) +
1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) − (1 · 0)) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) |
163 | | peano2nn 11032 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
164 | | nnmulcl 11043 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) →
(𝑛 · (𝑛 + 1)) ∈
ℕ) |
165 | 163, 164 | mpdan 702 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
166 | 73, 165 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · (𝑛 + 1)) ∈
ℕ) |
167 | 166 | nnrecred 11066 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 ·
(𝑛 + 1))) ∈
ℝ) |
168 | 167 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 ·
(𝑛 + 1))) ∈
ℂ) |
169 | | nnrp 11842 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
170 | | pntrval.r |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
171 | 170 | pntrf 25252 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑅:ℝ+⟶ℝ |
172 | 171 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℝ+
→ (𝑅‘𝑛) ∈
ℝ) |
173 | 169, 172 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑅‘𝑛) ∈ ℝ) |
174 | 73, 173 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘𝑛) ∈
ℝ) |
175 | 174 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘𝑛) ∈
ℂ) |
176 | 168, 175 | mulneg1d 10483 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (-(1 / (𝑛 ·
(𝑛 + 1))) · (𝑅‘𝑛)) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅‘𝑛))) |
177 | 74, 89 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · 1)
∈ ℂ) |
178 | 74, 110 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · (𝑛 + 1)) ∈
ℂ) |
179 | 166 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · (𝑛 + 1)) ≠ 0) |
180 | 110, 177,
178, 179 | divsubdird 10840 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) −
(𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1))))) |
181 | 74 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · 1) =
𝑛) |
182 | 181 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) −
(𝑛 · 1)) = ((𝑛 + 1) − 𝑛)) |
183 | 182, 113 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) −
(𝑛 · 1)) =
1) |
184 | 183 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) −
(𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (1 / (𝑛 · (𝑛 + 1)))) |
185 | 110 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) · 1)
= (𝑛 + 1)) |
186 | 110, 74 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) ·
𝑛) = (𝑛 · (𝑛 + 1))) |
187 | 185, 186 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) ·
1) / ((𝑛 + 1) ·
𝑛)) = ((𝑛 + 1) / (𝑛 · (𝑛 + 1)))) |
188 | 73, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 + 1) ∈
ℕ) |
189 | 188 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 + 1) ≠
0) |
190 | 89, 74, 110, 121, 189 | divcan5d 10827 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) ·
1) / ((𝑛 + 1) ·
𝑛)) = (1 / 𝑛)) |
191 | 187, 190 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) / (𝑛 · (𝑛 + 1))) = (1 / 𝑛)) |
192 | 89, 110, 74, 189, 121 | divcan5d 10827 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 · 1) /
(𝑛 · (𝑛 + 1))) = (1 / (𝑛 + 1))) |
193 | 191, 192 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1)))) = ((1 / 𝑛) − (1 / (𝑛 + 1)))) |
194 | 180, 184,
193 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 ·
(𝑛 + 1))) = ((1 / 𝑛) − (1 / (𝑛 + 1)))) |
195 | 194 | negeqd 10275 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ -(1 / (𝑛 ·
(𝑛 + 1))) = -((1 / 𝑛) − (1 / (𝑛 + 1)))) |
196 | 73 | nnrecred 11066 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑛) ∈
ℝ) |
197 | 196 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑛) ∈
ℂ) |
198 | 188 | nnrecred 11066 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 + 1)) ∈
ℝ) |
199 | 198 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 + 1)) ∈
ℂ) |
200 | 197, 199 | negsubdi2d 10408 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ -((1 / 𝑛) − (1
/ (𝑛 + 1))) = ((1 / (𝑛 + 1)) − (1 / 𝑛))) |
201 | 195, 200 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 / (𝑛 + 1))
− (1 / 𝑛)) = -(1 /
(𝑛 · (𝑛 + 1)))) |
202 | 73 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
203 | 77, 202 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
∈ ℝ+) |
204 | 170 | pntrval 25251 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 + 1) − 1) ∈
ℝ+ → (𝑅‘((𝑛 + 1) − 1)) = ((ψ‘((𝑛 + 1) − 1)) −
((𝑛 + 1) −
1))) |
205 | 203, 204 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘((𝑛 + 1) − 1)) =
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) |
206 | 77 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘((𝑛 + 1) − 1)) = (𝑅‘𝑛)) |
207 | 205, 206 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘((𝑛 +
1) − 1)) − ((𝑛
+ 1) − 1)) = (𝑅‘𝑛)) |
208 | 201, 207 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((1 / (𝑛 + 1))
− (1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) = (-(1 / (𝑛
· (𝑛 + 1))) ·
(𝑅‘𝑛))) |
209 | 175, 178,
179 | divrec2d 10805 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = ((1 / (𝑛 · (𝑛 + 1))) · (𝑅‘𝑛))) |
210 | 209 | negeqd 10275 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅‘𝑛))) |
211 | 176, 208,
210 | 3eqtr4d 2666 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((1 / (𝑛 + 1))
− (1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) = -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
212 | 71, 211 | sumeq12rdv 14438 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((1 / (𝑛 + 1)) −
(1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) = Σ𝑛
∈ (1...(⌊‘𝑥))-((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
213 | | fzfid 12772 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1[,)+∞) →
(1...(⌊‘𝑥))
∈ Fin) |
214 | 173, 165 | nndivred 11069 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
215 | 73, 214 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
216 | 215 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
217 | 213, 216 | fsumneg 14519 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1...(⌊‘𝑥))-((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
218 | 212, 217 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((1 / (𝑛 + 1)) −
(1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) = -Σ𝑛
∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
219 | 162, 218 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
((((1 / ((⌊‘𝑥)
+ 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) − (1 · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)))) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
220 | 67, 124, 219 | 3eqtr3d 2664 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
221 | | fzfid 12772 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ →
(1...(⌊‘𝑥))
∈ Fin) |
222 | 72 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
223 | 222, 214 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
224 | 221, 223 | fsumrecl 14465 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
225 | 224 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
226 | 4, 225 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
227 | 160, 226 | subnegd 10399 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
(((((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
− 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) +
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
228 | 220, 227 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
229 | 228 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑥 ∈ (1[,)+∞) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) = ((((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) +
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) −
1))) |
230 | 160, 226 | pncan2d 10394 |
. . . . . . 7
⊢ (𝑥 ∈ (1[,)+∞) →
((((((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
− 1) + Σ𝑛
∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) =
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
231 | 229, 230 | eqtrd 2656 |
. . . . . 6
⊢ (𝑥 ∈ (1[,)+∞) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) = Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
232 | 231 | mpteq2ia 4740 |
. . . . 5
⊢ (𝑥 ∈ (1[,)+∞) ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
233 | | fzfid 12772 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin) |
234 | 72 | adantl 482 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
235 | 234, 104 | syl 17 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) |
236 | 235, 118 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) −
1) ∈ ℝ) |
237 | 236, 234 | nndivred 11069 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛)
− 1) / 𝑛) ∈
ℝ) |
238 | 233, 237 | fsumrecl 14465 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) ∈
ℝ) |
239 | | rpre 11839 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
240 | 239 | adantl 482 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ) |
241 | 240, 133 | syl 17 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (ψ‘𝑥) ∈ ℝ) |
242 | 241, 155 | syl 17 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) + 1) ∈ ℝ) |
243 | | rprege0 11847 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
244 | 243, 50 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℕ0) |
245 | 244 | adantl 482 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (⌊‘𝑥) ∈
ℕ0) |
246 | 245, 52 | syl 17 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((⌊‘𝑥) + 1) ∈ ℕ) |
247 | 242, 246 | nndivred 11069 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ) |
248 | | peano2rem 10348 |
. . . . . . . 8
⊢
((((ψ‘𝑥) +
1) / ((⌊‘𝑥) +
1)) ∈ ℝ → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈
ℝ) |
249 | 247, 248 | syl 17 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈
ℝ) |
250 | | reex 10027 |
. . . . . . . . . . . 12
⊢ ℝ
∈ V |
251 | 250, 14 | ssexi 4803 |
. . . . . . . . . . 11
⊢
ℝ+ ∈ V |
252 | 251 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ ℝ+ ∈ V) |
253 | 235, 234 | nndivred 11069 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℝ) |
254 | 253 | recnd 10068 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℂ) |
255 | 233, 254 | fsumcl 14464 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
256 | | relogcl 24322 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
257 | 256 | adantl 482 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ∈ ℝ) |
258 | 257 | recnd 10068 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ∈ ℂ) |
259 | 255, 258 | subcld 10392 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ) |
260 | 234 | nnrecred 11066 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈
ℝ) |
261 | 233, 260 | fsumrecl 14465 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℝ) |
262 | 261, 257 | resubcld 10458 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℝ) |
263 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)))) |
264 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥)))) |
265 | 252, 259,
262, 263, 264 | offval2 6914 |
. . . . . . . . 9
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 −
(𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))))) |
266 | 260 | recnd 10068 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈
ℂ) |
267 | 233, 254,
266 | fsumsub 14520 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))) |
268 | 235 | recnd 10068 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℂ) |
269 | | 1cnd 10056 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℂ) |
270 | 234 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ) |
271 | 234 | nnne0d 11065 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0) |
272 | 268, 269,
270, 271 | divsubdird 10840 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛)
− 1) / 𝑛) =
(((Λ‘𝑛) /
𝑛) − (1 / 𝑛))) |
273 | 272 | sumeq2dv 14433 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛))) |
274 | 261 | recnd 10068 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℂ) |
275 | 255, 274,
258 | nnncan2d 10427 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))) |
276 | 267, 273,
275 | 3eqtr4rd 2667 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) |
277 | 276 | mpteq2dva 4744 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))) |
278 | 265, 277 | eqtrd 2656 |
. . . . . . . 8
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 −
(𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))) |
279 | | vmadivsum 25171 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) |
280 | 14 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ ℝ+ ⊆ ℝ) |
281 | 262 | recnd 10068 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℂ) |
282 | | 1red 10055 |
. . . . . . . . . 10
⊢ (⊤
→ 1 ∈ ℝ) |
283 | | harmoniclbnd 24735 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ≤
Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛)) |
284 | 283 | adantl 482 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛)) |
285 | 257, 261,
284 | abssubge0d 14170 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) |
286 | 285 | adantrr 753 |
. . . . . . . . . . 11
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) |
287 | 239 | ad2antrl 764 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
288 | | simprr 796 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥) |
289 | | harmonicubnd 24736 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) → Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) ≤ ((log‘𝑥) + 1)) |
290 | 287, 288,
289 | syl2anc 693 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1)) |
291 | | 1red 10055 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 1 ∈ ℝ) |
292 | 261, 257,
291 | lesubadd2d 10626 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))) |
293 | 292 | adantrr 753 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))) |
294 | 290, 293 | mpbird 247 |
. . . . . . . . . . 11
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1) |
295 | 286, 294 | eqbrtrd 4675 |
. . . . . . . . . 10
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥))) ≤ 1) |
296 | 280, 281,
282, 282, 295 | elo1d 14267 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) |
297 | | o1sub 14346 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥))) ∈ 𝑂(1)) →
((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 −
(𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) ∈ 𝑂(1)) |
298 | 279, 296,
297 | sylancr 695 |
. . . . . . . 8
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 −
(𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) ∈ 𝑂(1)) |
299 | 278, 298 | eqeltrrd 2702 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) ∈
𝑂(1)) |
300 | 247 | recnd 10068 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ) |
301 | | 1cnd 10056 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 1 ∈ ℂ) |
302 | 241 | recnd 10068 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (ψ‘𝑥) ∈ ℂ) |
303 | | rpcnne0 11850 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
304 | 303 | adantl 482 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
305 | | divdir 10710 |
. . . . . . . . . . . 12
⊢
(((ψ‘𝑥)
∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) |
306 | 302, 301,
304, 305 | syl3anc 1326 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) |
307 | 306 | mpteq2dva 4744 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
(((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))) |
308 | | simpr 477 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ+) |
309 | 241, 308 | rerpdivcld 11903 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ) |
310 | | rpreccl 11857 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ+) |
311 | 310 | adantl 482 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1 / 𝑥) ∈
ℝ+) |
312 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
((ψ‘𝑥) / 𝑥))) |
313 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) |
314 | 252, 309,
311, 312, 313 | offval2 6914 |
. . . . . . . . . . 11
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+
↦ (1 / 𝑥))) = (𝑥 ∈ ℝ+
↦ (((ψ‘𝑥) /
𝑥) + (1 / 𝑥)))) |
315 | | chpo1ub 25169 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈
𝑂(1) |
316 | | divrcnv 14584 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℂ → (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) |
317 | 75, 316 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
↦ (1 / 𝑥))
⇝𝑟 0 |
318 | | rlimo1 14347 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
↦ (1 / 𝑥))
⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) ∈
𝑂(1)) |
319 | 317, 318 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) |
320 | | o1add 14344 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈ 𝑂(1)
∧ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥))
∘𝑓 + (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) ∈
𝑂(1)) |
321 | 315, 319,
320 | sylancr 695 |
. . . . . . . . . . 11
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+
↦ (1 / 𝑥))) ∈
𝑂(1)) |
322 | 314, 321 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1)) |
323 | 307, 322 | eqeltrd 2701 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) ∈ 𝑂(1)) |
324 | 242, 308 | rerpdivcld 11903 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℝ) |
325 | | chpge0 24852 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ → 0 ≤
(ψ‘𝑥)) |
326 | 240, 325 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 0 ≤ (ψ‘𝑥)) |
327 | 241, 326 | ge0p1rpd 11902 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) + 1) ∈
ℝ+) |
328 | 327 | rprege0d 11879 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 ≤
((ψ‘𝑥) +
1))) |
329 | 246 | nnrpd 11870 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((⌊‘𝑥) + 1) ∈
ℝ+) |
330 | 329 | rpregt0d 11878 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 <
((⌊‘𝑥) +
1))) |
331 | | divge0 10892 |
. . . . . . . . . . . . 13
⊢
(((((ψ‘𝑥)
+ 1) ∈ ℝ ∧ 0 ≤ ((ψ‘𝑥) + 1)) ∧ (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0
< ((⌊‘𝑥) +
1))) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) |
332 | 328, 330,
331 | syl2anc 693 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) |
333 | 247, 332 | absidd 14161 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) |
334 | 324 | recnd 10068 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℂ) |
335 | 334 | abscld 14175 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / 𝑥)) ∈ ℝ) |
336 | | fllep1 12602 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
337 | 240, 336 | syl 17 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
338 | | rpregt0 11846 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
339 | 338 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 < 𝑥)) |
340 | 327 | rpregt0d 11878 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 <
((ψ‘𝑥) +
1))) |
341 | | lediv2 10913 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ ∧ 0 <
𝑥) ∧
(((⌊‘𝑥) + 1)
∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1)) ∧ (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0
< ((ψ‘𝑥) +
1))) → (𝑥 ≤
((⌊‘𝑥) + 1)
↔ (((ψ‘𝑥) +
1) / ((⌊‘𝑥) +
1)) ≤ (((ψ‘𝑥)
+ 1) / 𝑥))) |
342 | 339, 330,
340, 341 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤
(((ψ‘𝑥) + 1) /
𝑥))) |
343 | 337, 342 | mpbid 222 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥)) |
344 | 324 | leabsd 14153 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥))) |
345 | 247, 324,
335, 343, 344 | letrd 10194 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥))) |
346 | 333, 345 | eqbrtrd 4675 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥))) |
347 | 346 | adantrr 753 |
. . . . . . . . 9
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤
(abs‘(((ψ‘𝑥) + 1) / 𝑥))) |
348 | 282, 323,
324, 300, 347 | o1le 14383 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ∈
𝑂(1)) |
349 | | o1const 14350 |
. . . . . . . . . 10
⊢
((ℝ+ ⊆ ℝ ∧ 1 ∈ ℂ) →
(𝑥 ∈
ℝ+ ↦ 1) ∈ 𝑂(1)) |
350 | 14, 75, 349 | mp2an 708 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ 1) ∈ 𝑂(1) |
351 | 350 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ 1) ∈ 𝑂(1)) |
352 | 300, 301,
348, 351 | o1sub2 14356 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) ∈
𝑂(1)) |
353 | 238, 249,
299, 352 | o1sub2 14356 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈
𝑂(1)) |
354 | 13, 353 | o1res2 14294 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈
𝑂(1)) |
355 | 232, 354 | syl5eqelr 2706 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈
𝑂(1)) |
356 | 16, 355 | eqeltrd 2701 |
. . 3
⊢ (⊤
→ ((𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈
𝑂(1)) |
357 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
358 | 357, 225 | fmpti 6383 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 +
1)))):ℝ⟶ℂ |
359 | 358 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 +
1)))):ℝ⟶ℂ) |
360 | | ssid 3624 |
. . . . 5
⊢ ℝ
⊆ ℝ |
361 | 360 | a1i 11 |
. . . 4
⊢ (⊤
→ ℝ ⊆ ℝ) |
362 | 359, 361,
282 | o1resb 14297 |
. . 3
⊢ (⊤
→ ((𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) ↔ ((𝑥 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈
𝑂(1))) |
363 | 356, 362 | mpbird 247 |
. 2
⊢ (⊤
→ (𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈
𝑂(1)) |
364 | 363 | trud 1493 |
1
⊢ (𝑥 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) |