Step | Hyp | Ref
| Expression |
1 | | 1re 10975 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
2 | | elicopnf 13177 |
. . . . . . . . . . 11
⊢ (1 ∈
ℝ → (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 1
≤ 𝑥)) |
4 | 3 | simplbi 498 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
𝑥 ∈
ℝ) |
5 | | 0red 10978 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) → 0
∈ ℝ) |
6 | | 1red 10976 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) → 1
∈ ℝ) |
7 | | 0lt1 11497 |
. . . . . . . . . . 11
⊢ 0 <
1 |
8 | 7 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) → 0
< 1) |
9 | 3 | simprbi 497 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) → 1
≤ 𝑥) |
10 | 5, 6, 4, 8, 9 | ltletrd 11135 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) → 0
< 𝑥) |
11 | 4, 10 | elrpd 12769 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) →
𝑥 ∈
ℝ+) |
12 | 11 | ssriv 3925 |
. . . . . . 7
⊢
(1[,)+∞) ⊆ ℝ+ |
13 | 12 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (1[,)+∞) ⊆ ℝ+) |
14 | | rpssre 12737 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
15 | 13, 14 | sstrdi 3933 |
. . . . 5
⊢ (⊤
→ (1[,)+∞) ⊆ ℝ) |
16 | 15 | resmptd 5948 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
17 | | chpcl 26273 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
18 | 4, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘𝑥) ∈
ℝ) |
19 | | peano2re 11148 |
. . . . . . . . . . 11
⊢
((ψ‘𝑥)
∈ ℝ → ((ψ‘𝑥) + 1) ∈ ℝ) |
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘𝑥) + 1)
∈ ℝ) |
21 | 11 | rprege0d 12779 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
22 | | flge0nn0 13540 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
(⌊‘𝑥) ∈
ℕ0) |
24 | | nn0p1nn 12272 |
. . . . . . . . . . 11
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
25 | 23, 24 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
((⌊‘𝑥) + 1)
∈ ℕ) |
26 | 20, 25 | nndivred 12027 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
(((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
∈ ℝ) |
27 | 26 | recnd 11003 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) →
(((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
∈ ℂ) |
28 | | ax-1cn 10929 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
29 | | subcl 11220 |
. . . . . . . 8
⊢
(((((ψ‘𝑥)
+ 1) / ((⌊‘𝑥) +
1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈
ℂ) |
30 | 27, 28, 29 | sylancl 586 |
. . . . . . 7
⊢ (𝑥 ∈ (1[,)+∞) →
((((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
− 1) ∈ ℂ) |
31 | | fzfid 13693 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ →
(1...(⌊‘𝑥))
∈ Fin) |
32 | | elfznn 13285 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
33 | 32 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
34 | | nnrp 12741 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
35 | | pntrval.r |
. . . . . . . . . . . . . . 15
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
36 | 35 | pntrf 26711 |
. . . . . . . . . . . . . 14
⊢ 𝑅:ℝ+⟶ℝ |
37 | 36 | ffvelrni 6960 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℝ+
→ (𝑅‘𝑛) ∈
ℝ) |
38 | 34, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑅‘𝑛) ∈ ℝ) |
39 | | peano2nn 11985 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
40 | | nnmulcl 11997 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) →
(𝑛 · (𝑛 + 1)) ∈
ℕ) |
41 | 39, 40 | mpdan 684 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
42 | 38, 41 | nndivred 12027 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
43 | 33, 42 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
44 | 31, 43 | fsumrecl 15446 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
45 | 44 | recnd 11003 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
46 | 4, 45 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
47 | | oveq2 7283 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛)) |
48 | | fvoveq1 7298 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1))) |
49 | | oveq1 7282 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑚 − 1) = (𝑛 − 1)) |
50 | 48, 49 | oveq12d 7293 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) |
51 | 47, 50 | jca 512 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((1 / 𝑚) = (1 / 𝑛) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) |
52 | | oveq2 7283 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (1 / 𝑚) = (1 / (𝑛 + 1))) |
53 | | fvoveq1 7298 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) −
1))) |
54 | | oveq1 7282 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (𝑚 − 1) = ((𝑛 + 1) − 1)) |
55 | 53, 54 | oveq12d 7293 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) =
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) |
56 | 52, 55 | jca 512 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → ((1 / 𝑚) = (1 / (𝑛 + 1)) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) =
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)))) |
57 | | oveq2 7283 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (1 / 𝑚) = (1 / 1)) |
58 | | 1div1e1 11665 |
. . . . . . . . . . . 12
⊢ (1 / 1) =
1 |
59 | 57, 58 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → (1 / 𝑚) = 1) |
60 | | oveq1 7282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) |
61 | | 1m1e0 12045 |
. . . . . . . . . . . . . . . 16
⊢ (1
− 1) = 0 |
62 | 60, 61 | eqtrdi 2794 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) |
63 | 62 | fveq2d 6778 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) =
(ψ‘0)) |
64 | | 2pos 12076 |
. . . . . . . . . . . . . . 15
⊢ 0 <
2 |
65 | | 0re 10977 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
66 | | chpeq0 26356 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
ℝ → ((ψ‘0) = 0 ↔ 0 < 2)) |
67 | 65, 66 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
((ψ‘0) = 0 ↔ 0 < 2) |
68 | 64, 67 | mpbir 230 |
. . . . . . . . . . . . . 14
⊢
(ψ‘0) = 0 |
69 | 63, 68 | eqtrdi 2794 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) =
0) |
70 | 69, 62 | oveq12d 7293 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = (0 −
0)) |
71 | | 0m0e0 12093 |
. . . . . . . . . . . 12
⊢ (0
− 0) = 0 |
72 | 70, 71 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) =
0) |
73 | 59, 72 | jca 512 |
. . . . . . . . . 10
⊢ (𝑚 = 1 → ((1 / 𝑚) = 1 ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) =
0)) |
74 | | oveq2 7283 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (1 / 𝑚) = (1 / ((⌊‘𝑥) + 1))) |
75 | | fvoveq1 7298 |
. . . . . . . . . . . 12
⊢ (𝑚 = ((⌊‘𝑥) + 1) →
(ψ‘(𝑚 − 1))
= (ψ‘(((⌊‘𝑥) + 1) − 1))) |
76 | | oveq1 7282 |
. . . . . . . . . . . 12
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑚 − 1) =
(((⌊‘𝑥) + 1)
− 1)) |
77 | 75, 76 | oveq12d 7293 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) →
((ψ‘(𝑚 −
1)) − (𝑚 − 1))
= ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) |
78 | 74, 77 | jca 512 |
. . . . . . . . . 10
⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((1 / 𝑚) = (1 / ((⌊‘𝑥) + 1)) ∧
((ψ‘(𝑚 −
1)) − (𝑚 − 1))
= ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1)))) |
79 | | nnuz 12621 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
80 | 25, 79 | eleqtrdi 2849 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
((⌊‘𝑥) + 1)
∈ (ℤ≥‘1)) |
81 | | elfznn 13285 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈
(1...((⌊‘𝑥) +
1)) → 𝑚 ∈
ℕ) |
82 | 81 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℕ) |
83 | 82 | nnrecred 12024 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (1 / 𝑚) ∈
ℝ) |
84 | 83 | recnd 11003 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (1 / 𝑚) ∈
ℂ) |
85 | 82 | nnred 11988 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℝ) |
86 | | peano2rem 11288 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℝ → (𝑚 − 1) ∈
ℝ) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (𝑚 − 1)
∈ ℝ) |
88 | | chpcl 26273 |
. . . . . . . . . . . . 13
⊢ ((𝑚 − 1) ∈ ℝ
→ (ψ‘(𝑚
− 1)) ∈ ℝ) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (ψ‘(𝑚
− 1)) ∈ ℝ) |
90 | 89, 87 | resubcld 11403 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℝ) |
91 | 90 | recnd 11003 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℂ) |
92 | 51, 56, 73, 78, 80, 84, 91 | fsumparts 15518 |
. . . . . . . . 9
⊢ (𝑥 ∈ (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))))) |
93 | 4 | flcld 13518 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
(⌊‘𝑥) ∈
ℤ) |
94 | | fzval3 13456 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑥)
∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
(1...(⌊‘𝑥)) =
(1..^((⌊‘𝑥) +
1))) |
96 | 95 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
(1..^((⌊‘𝑥) +
1)) = (1...(⌊‘𝑥))) |
97 | 32 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
98 | 97 | nncnd 11989 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℂ) |
99 | | pncan 11227 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
100 | 98, 28, 99 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
= 𝑛) |
101 | 97 | nnred 11988 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ) |
102 | 100, 101 | eqeltrd 2839 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
∈ ℝ) |
103 | | chpcl 26273 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 + 1) − 1) ∈ ℝ
→ (ψ‘((𝑛 +
1) − 1)) ∈ ℝ) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) ∈ ℝ) |
105 | 104 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) ∈ ℂ) |
106 | 102 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
∈ ℂ) |
107 | | peano2rem 11288 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) |
108 | 101, 107 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℝ) |
109 | | chpcl 26273 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 − 1) ∈ ℝ
→ (ψ‘(𝑛
− 1)) ∈ ℝ) |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑛
− 1)) ∈ ℝ) |
111 | 110 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑛
− 1)) ∈ ℂ) |
112 | | 1cnd 10970 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℂ) |
113 | 98, 112 | subcld 11332 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℂ) |
114 | 105, 106,
111, 113 | sub4d 11381 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((ψ‘((𝑛 +
1) − 1)) − ((𝑛
+ 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = (((ψ‘((𝑛 + 1) − 1)) −
(ψ‘(𝑛 −
1))) − (((𝑛 + 1)
− 1) − (𝑛
− 1)))) |
115 | | vmacl 26267 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
116 | 97, 115 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
117 | 116 | recnd 11003 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℂ) |
118 | | nnm1nn0 12274 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
119 | 97, 118 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℕ0) |
120 | | chpp1 26304 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 − 1) ∈
ℕ0 → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) +
(Λ‘((𝑛 −
1) + 1)))) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛
− 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) +
1)))) |
122 | | npcan 11230 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
123 | 98, 28, 122 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 − 1) + 1)
= 𝑛) |
124 | 123, 100 | eqtr4d 2781 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 − 1) + 1)
= ((𝑛 + 1) −
1)) |
125 | 124 | fveq2d 6778 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛
− 1) + 1)) = (ψ‘((𝑛 + 1) − 1))) |
126 | 123 | fveq2d 6778 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘((𝑛
− 1) + 1)) = (Λ‘𝑛)) |
127 | 126 | oveq2d 7291 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑛
− 1)) + (Λ‘((𝑛 − 1) + 1))) = ((ψ‘(𝑛 − 1)) +
(Λ‘𝑛))) |
128 | 121, 125,
127 | 3eqtr3d 2786 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛))) |
129 | 111, 117,
128 | mvrladdd 11388 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘((𝑛 +
1) − 1)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛)) |
130 | | peano2cn 11147 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℂ → (𝑛 + 1) ∈
ℂ) |
131 | 98, 130 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 + 1) ∈
ℂ) |
132 | 131, 98, 112 | nnncan2d 11367 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) − 1)
− (𝑛 − 1)) =
((𝑛 + 1) − 𝑛)) |
133 | | pncan2 11228 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 𝑛) =
1) |
134 | 98, 28, 133 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) −
𝑛) = 1) |
135 | 132, 134 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) − 1)
− (𝑛 − 1)) =
1) |
136 | 129, 135 | oveq12d 7293 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((ψ‘((𝑛 +
1) − 1)) − (ψ‘(𝑛 − 1))) − (((𝑛 + 1) − 1) − (𝑛 − 1))) = ((Λ‘𝑛) − 1)) |
137 | 114, 136 | eqtrd 2778 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((ψ‘((𝑛 +
1) − 1)) − ((𝑛
+ 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = ((Λ‘𝑛) − 1)) |
138 | 137 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 / 𝑛) ·
(((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = ((1 / 𝑛) · ((Λ‘𝑛) − 1))) |
139 | | peano2rem 11288 |
. . . . . . . . . . . . . 14
⊢
((Λ‘𝑛)
∈ ℝ → ((Λ‘𝑛) − 1) ∈ ℝ) |
140 | 116, 139 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
− 1) ∈ ℝ) |
141 | 140 | recnd 11003 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
− 1) ∈ ℂ) |
142 | 97 | nnne0d 12023 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ≠
0) |
143 | 141, 98, 142 | divrec2d 11755 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
− 1) / 𝑛) = ((1 /
𝑛) ·
((Λ‘𝑛) −
1))) |
144 | 138, 143 | eqtr4d 2781 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 / 𝑛) ·
(((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = (((Λ‘𝑛) − 1) / 𝑛)) |
145 | 96, 144 | sumeq12rdv 15419 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))((1 / 𝑛) ·
(((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) |
146 | 23 | nn0cnd 12295 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (1[,)+∞) →
(⌊‘𝑥) ∈
ℂ) |
147 | | pncan 11227 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⌊‘𝑥)
∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑥) + 1) − 1) =
(⌊‘𝑥)) |
148 | 146, 28, 147 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (1[,)+∞) →
(((⌊‘𝑥) + 1)
− 1) = (⌊‘𝑥)) |
149 | 148 | fveq2d 6778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘(((⌊‘𝑥) + 1) − 1)) =
(ψ‘(⌊‘𝑥))) |
150 | | chpfl 26299 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ →
(ψ‘(⌊‘𝑥)) = (ψ‘𝑥)) |
151 | 4, 150 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘(⌊‘𝑥)) = (ψ‘𝑥)) |
152 | 149, 151 | eqtrd 2778 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘𝑥)) |
153 | 152 | oveq1d 7290 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1)) = ((ψ‘𝑥) − (((⌊‘𝑥) + 1) − 1))) |
154 | 18 | recnd 11003 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘𝑥) ∈
ℂ) |
155 | 25 | nncnd 11989 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) →
((⌊‘𝑥) + 1)
∈ ℂ) |
156 | | 1cnd 10970 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) → 1
∈ ℂ) |
157 | 154, 155,
156 | subsub3d 11362 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘𝑥) −
(((⌊‘𝑥) + 1)
− 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) |
158 | 153, 157 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) |
159 | 158 | oveq2d 7291 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) = ((1 / ((⌊‘𝑥) + 1)) · (((ψ‘𝑥) + 1) −
((⌊‘𝑥) +
1)))) |
160 | 25 | nnrecred 12024 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) → (1
/ ((⌊‘𝑥) + 1))
∈ ℝ) |
161 | 160 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) → (1
/ ((⌊‘𝑥) + 1))
∈ ℂ) |
162 | | peano2cn 11147 |
. . . . . . . . . . . . . . 15
⊢
((ψ‘𝑥)
∈ ℂ → ((ψ‘𝑥) + 1) ∈ ℂ) |
163 | 154, 162 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘𝑥) + 1)
∈ ℂ) |
164 | 161, 163,
155 | subdid 11431 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) = (((1 /
((⌊‘𝑥) + 1))
· ((ψ‘𝑥) +
1)) − ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1)))) |
165 | 25 | nnne0d 12023 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) →
((⌊‘𝑥) + 1)
≠ 0) |
166 | 163, 155,
165 | divrec2d 11755 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) →
(((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1)) =
((1 / ((⌊‘𝑥) +
1)) · ((ψ‘𝑥) + 1))) |
167 | 166 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · ((ψ‘𝑥) + 1)) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) |
168 | 155, 165 | recid2d 11747 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · ((⌊‘𝑥) + 1)) = 1) |
169 | 167, 168 | oveq12d 7293 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1[,)+∞) →
(((1 / ((⌊‘𝑥) +
1)) · ((ψ‘𝑥) + 1)) − ((1 / ((⌊‘𝑥) + 1)) ·
((⌊‘𝑥) + 1))) =
((((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
− 1)) |
170 | 159, 164,
169 | 3eqtrd 2782 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) |
171 | 28 | mul01i 11165 |
. . . . . . . . . . . . 13
⊢ (1
· 0) = 0 |
172 | 171 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) → (1
· 0) = 0) |
173 | 170, 172 | oveq12d 7293 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
(((1 / ((⌊‘𝑥) +
1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) − (1 · 0)) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) −
0)) |
174 | 30 | subid1d 11321 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
(((((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
− 1) − 0) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) |
175 | 173, 174 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
(((1 / ((⌊‘𝑥) +
1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) − (1 · 0)) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) |
176 | 97, 41 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · (𝑛 + 1)) ∈
ℕ) |
177 | 176 | nnrecred 12024 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 ·
(𝑛 + 1))) ∈
ℝ) |
178 | 177 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 ·
(𝑛 + 1))) ∈
ℂ) |
179 | 97, 38 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘𝑛) ∈
ℝ) |
180 | 179 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘𝑛) ∈
ℂ) |
181 | 178, 180 | mulneg1d 11428 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (-(1 / (𝑛 ·
(𝑛 + 1))) · (𝑅‘𝑛)) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅‘𝑛))) |
182 | 98, 112 | mulcld 10995 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · 1)
∈ ℂ) |
183 | 98, 131 | mulcld 10995 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · (𝑛 + 1)) ∈
ℂ) |
184 | 176 | nnne0d 12023 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · (𝑛 + 1)) ≠ 0) |
185 | 131, 182,
183, 184 | divsubdird 11790 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) −
(𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1))))) |
186 | 98 | mulid1d 10992 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · 1) =
𝑛) |
187 | 186 | oveq2d 7291 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) −
(𝑛 · 1)) = ((𝑛 + 1) − 𝑛)) |
188 | 187, 134 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) −
(𝑛 · 1)) =
1) |
189 | 188 | oveq1d 7290 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) −
(𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (1 / (𝑛 · (𝑛 + 1)))) |
190 | 131 | mulid1d 10992 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) · 1)
= (𝑛 + 1)) |
191 | 131, 98 | mulcomd 10996 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) ·
𝑛) = (𝑛 · (𝑛 + 1))) |
192 | 190, 191 | oveq12d 7293 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) ·
1) / ((𝑛 + 1) ·
𝑛)) = ((𝑛 + 1) / (𝑛 · (𝑛 + 1)))) |
193 | 97, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 + 1) ∈
ℕ) |
194 | 193 | nnne0d 12023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 + 1) ≠
0) |
195 | 112, 98, 131, 142, 194 | divcan5d 11777 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) ·
1) / ((𝑛 + 1) ·
𝑛)) = (1 / 𝑛)) |
196 | 192, 195 | eqtr3d 2780 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) / (𝑛 · (𝑛 + 1))) = (1 / 𝑛)) |
197 | 112, 131,
98, 194, 142 | divcan5d 11777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 · 1) /
(𝑛 · (𝑛 + 1))) = (1 / (𝑛 + 1))) |
198 | 196, 197 | oveq12d 7293 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1)))) = ((1 / 𝑛) − (1 / (𝑛 + 1)))) |
199 | 185, 189,
198 | 3eqtr3d 2786 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 ·
(𝑛 + 1))) = ((1 / 𝑛) − (1 / (𝑛 + 1)))) |
200 | 199 | negeqd 11215 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ -(1 / (𝑛 ·
(𝑛 + 1))) = -((1 / 𝑛) − (1 / (𝑛 + 1)))) |
201 | 97 | nnrecred 12024 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑛) ∈
ℝ) |
202 | 201 | recnd 11003 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑛) ∈
ℂ) |
203 | 193 | nnrecred 12024 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 + 1)) ∈
ℝ) |
204 | 203 | recnd 11003 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 + 1)) ∈
ℂ) |
205 | 202, 204 | negsubdi2d 11348 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ -((1 / 𝑛) − (1
/ (𝑛 + 1))) = ((1 / (𝑛 + 1)) − (1 / 𝑛))) |
206 | 200, 205 | eqtr2d 2779 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 / (𝑛 + 1))
− (1 / 𝑛)) = -(1 /
(𝑛 · (𝑛 + 1)))) |
207 | 97 | nnrpd 12770 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
208 | 100, 207 | eqeltrd 2839 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
∈ ℝ+) |
209 | 35 | pntrval 26710 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 + 1) − 1) ∈
ℝ+ → (𝑅‘((𝑛 + 1) − 1)) = ((ψ‘((𝑛 + 1) − 1)) −
((𝑛 + 1) −
1))) |
210 | 208, 209 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘((𝑛 + 1) − 1)) =
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) |
211 | 100 | fveq2d 6778 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘((𝑛 + 1) − 1)) = (𝑅‘𝑛)) |
212 | 210, 211 | eqtr3d 2780 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘((𝑛 +
1) − 1)) − ((𝑛
+ 1) − 1)) = (𝑅‘𝑛)) |
213 | 206, 212 | oveq12d 7293 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((1 / (𝑛 + 1))
− (1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) = (-(1 / (𝑛
· (𝑛 + 1))) ·
(𝑅‘𝑛))) |
214 | 180, 183,
184 | divrec2d 11755 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = ((1 / (𝑛 · (𝑛 + 1))) · (𝑅‘𝑛))) |
215 | 214 | negeqd 11215 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅‘𝑛))) |
216 | 181, 213,
215 | 3eqtr4d 2788 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((1 / (𝑛 + 1))
− (1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) = -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
217 | 96, 216 | sumeq12rdv 15419 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((1 / (𝑛 + 1)) −
(1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) = Σ𝑛
∈ (1...(⌊‘𝑥))-((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
218 | | fzfid 13693 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
(1...(⌊‘𝑥))
∈ Fin) |
219 | 97, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
220 | 219 | recnd 11003 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
221 | 218, 220 | fsumneg 15499 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1...(⌊‘𝑥))-((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
222 | 217, 221 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((1 / (𝑛 + 1)) −
(1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) = -Σ𝑛
∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
223 | 175, 222 | oveq12d 7293 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
((((1 / ((⌊‘𝑥)
+ 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) − (1 · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)))) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
224 | 92, 145, 223 | 3eqtr3d 2786 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
225 | 30, 46 | subnegd 11339 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) →
(((((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
− 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) +
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
226 | 224, 225 | eqtrd 2778 |
. . . . . . 7
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
227 | 30, 46, 226 | mvrladdd 11388 |
. . . . . 6
⊢ (𝑥 ∈ (1[,)+∞) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) = Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
228 | 227 | mpteq2ia 5177 |
. . . . 5
⊢ (𝑥 ∈ (1[,)+∞) ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
229 | | fzfid 13693 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin) |
230 | 32 | adantl 482 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
231 | 230, 115 | syl 17 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) |
232 | 231, 139 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) −
1) ∈ ℝ) |
233 | 232, 230 | nndivred 12027 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛)
− 1) / 𝑛) ∈
ℝ) |
234 | 229, 233 | fsumrecl 15446 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) ∈
ℝ) |
235 | | rpre 12738 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
236 | 235 | adantl 482 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ) |
237 | 236, 17 | syl 17 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (ψ‘𝑥) ∈ ℝ) |
238 | 237, 19 | syl 17 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) + 1) ∈ ℝ) |
239 | | rprege0 12745 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
240 | 239, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℕ0) |
241 | 240 | adantl 482 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (⌊‘𝑥) ∈
ℕ0) |
242 | 241, 24 | syl 17 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((⌊‘𝑥) + 1) ∈ ℕ) |
243 | 238, 242 | nndivred 12027 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ) |
244 | | peano2rem 11288 |
. . . . . . . 8
⊢
((((ψ‘𝑥) +
1) / ((⌊‘𝑥) +
1)) ∈ ℝ → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈
ℝ) |
245 | 243, 244 | syl 17 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈
ℝ) |
246 | | reex 10962 |
. . . . . . . . . . . 12
⊢ ℝ
∈ V |
247 | 246, 14 | ssexi 5246 |
. . . . . . . . . . 11
⊢
ℝ+ ∈ V |
248 | 247 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ ℝ+ ∈ V) |
249 | 231, 230 | nndivred 12027 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℝ) |
250 | 249 | recnd 11003 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℂ) |
251 | 229, 250 | fsumcl 15445 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
252 | | relogcl 25731 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
253 | 252 | adantl 482 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ∈ ℝ) |
254 | 253 | recnd 11003 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ∈ ℂ) |
255 | 251, 254 | subcld 11332 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ) |
256 | 230 | nnrecred 12024 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈
ℝ) |
257 | 229, 256 | fsumrecl 15446 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℝ) |
258 | 257, 253 | resubcld 11403 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℝ) |
259 | | eqidd 2739 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)))) |
260 | | eqidd 2739 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥)))) |
261 | 248, 255,
258, 259, 260 | offval2 7553 |
. . . . . . . . 9
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))))) |
262 | 256 | recnd 11003 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈
ℂ) |
263 | 229, 250,
262 | fsumsub 15500 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))) |
264 | 231 | recnd 11003 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℂ) |
265 | | 1cnd 10970 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℂ) |
266 | 230 | nncnd 11989 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ) |
267 | 230 | nnne0d 12023 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0) |
268 | 264, 265,
266, 267 | divsubdird 11790 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛)
− 1) / 𝑛) =
(((Λ‘𝑛) /
𝑛) − (1 / 𝑛))) |
269 | 268 | sumeq2dv 15415 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛))) |
270 | 257 | recnd 11003 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℂ) |
271 | 251, 270,
254 | nnncan2d 11367 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))) |
272 | 263, 269,
271 | 3eqtr4rd 2789 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) |
273 | 272 | mpteq2dva 5174 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))) |
274 | 261, 273 | eqtrd 2778 |
. . . . . . . 8
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))) |
275 | | vmadivsum 26630 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) |
276 | 14 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ ℝ+ ⊆ ℝ) |
277 | 258 | recnd 11003 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℂ) |
278 | | 1red 10976 |
. . . . . . . . . 10
⊢ (⊤
→ 1 ∈ ℝ) |
279 | | harmoniclbnd 26158 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ≤
Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛)) |
280 | 279 | adantl 482 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛)) |
281 | 253, 257,
280 | abssubge0d 15143 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) |
282 | 281 | adantrr 714 |
. . . . . . . . . . 11
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) |
283 | 235 | ad2antrl 725 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
284 | | simprr 770 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥) |
285 | | harmonicubnd 26159 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) → Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) ≤ ((log‘𝑥) + 1)) |
286 | 283, 284,
285 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1)) |
287 | | 1red 10976 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 1 ∈ ℝ) |
288 | 257, 253,
287 | lesubadd2d 11574 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))) |
289 | 288 | adantrr 714 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))) |
290 | 286, 289 | mpbird 256 |
. . . . . . . . . . 11
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1) |
291 | 282, 290 | eqbrtrd 5096 |
. . . . . . . . . 10
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥))) ≤ 1) |
292 | 276, 277,
278, 278, 291 | elo1d 15245 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) |
293 | | o1sub 15325 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥))) ∈ 𝑂(1)) →
((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥)))) ∈
𝑂(1)) |
294 | 275, 292,
293 | sylancr 587 |
. . . . . . . 8
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥)))) ∈
𝑂(1)) |
295 | 274, 294 | eqeltrrd 2840 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) ∈
𝑂(1)) |
296 | 243 | recnd 11003 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ) |
297 | | 1cnd 10970 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 1 ∈ ℂ) |
298 | 237 | recnd 11003 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (ψ‘𝑥) ∈ ℂ) |
299 | | rpcnne0 12748 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
300 | 299 | adantl 482 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
301 | | divdir 11658 |
. . . . . . . . . . . 12
⊢
(((ψ‘𝑥)
∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) |
302 | 298, 297,
300, 301 | syl3anc 1370 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) |
303 | 302 | mpteq2dva 5174 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
(((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))) |
304 | | simpr 485 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ+) |
305 | 237, 304 | rerpdivcld 12803 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ) |
306 | | rpreccl 12756 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ+) |
307 | 306 | adantl 482 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1 / 𝑥) ∈
ℝ+) |
308 | | eqidd 2739 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
((ψ‘𝑥) / 𝑥))) |
309 | | eqidd 2739 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) |
310 | 248, 305,
307, 308, 309 | offval2 7553 |
. . . . . . . . . . 11
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) = (𝑥 ∈ ℝ+ ↦
(((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))) |
311 | | chpo1ub 26628 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈
𝑂(1) |
312 | | divrcnv 15564 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℂ → (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) |
313 | 28, 312 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
↦ (1 / 𝑥))
⇝𝑟 0 |
314 | | rlimo1 15326 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
↦ (1 / 𝑥))
⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) ∈
𝑂(1)) |
315 | 313, 314 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) |
316 | | o1add 15323 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈ 𝑂(1)
∧ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∘f +
(𝑥 ∈
ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1)) |
317 | 311, 315,
316 | sylancr 587 |
. . . . . . . . . . 11
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) ∈
𝑂(1)) |
318 | 310, 317 | eqeltrrd 2840 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1)) |
319 | 303, 318 | eqeltrd 2839 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) ∈ 𝑂(1)) |
320 | 238, 304 | rerpdivcld 12803 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℝ) |
321 | | chpge0 26275 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ → 0 ≤
(ψ‘𝑥)) |
322 | 236, 321 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 0 ≤ (ψ‘𝑥)) |
323 | 237, 322 | ge0p1rpd 12802 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) + 1) ∈
ℝ+) |
324 | 323 | rprege0d 12779 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 ≤
((ψ‘𝑥) +
1))) |
325 | 242 | nnrpd 12770 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((⌊‘𝑥) + 1) ∈
ℝ+) |
326 | 325 | rpregt0d 12778 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 <
((⌊‘𝑥) +
1))) |
327 | | divge0 11844 |
. . . . . . . . . . . . 13
⊢
(((((ψ‘𝑥)
+ 1) ∈ ℝ ∧ 0 ≤ ((ψ‘𝑥) + 1)) ∧ (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0
< ((⌊‘𝑥) +
1))) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) |
328 | 324, 326,
327 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) |
329 | 243, 328 | absidd 15134 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) |
330 | 320 | recnd 11003 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℂ) |
331 | 330 | abscld 15148 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / 𝑥)) ∈ ℝ) |
332 | | fllep1 13521 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
333 | 236, 332 | syl 17 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
334 | | rpregt0 12744 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
335 | 334 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 < 𝑥)) |
336 | 323 | rpregt0d 12778 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 <
((ψ‘𝑥) +
1))) |
337 | | lediv2 11865 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ ∧ 0 <
𝑥) ∧
(((⌊‘𝑥) + 1)
∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1)) ∧ (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0
< ((ψ‘𝑥) +
1))) → (𝑥 ≤
((⌊‘𝑥) + 1)
↔ (((ψ‘𝑥) +
1) / ((⌊‘𝑥) +
1)) ≤ (((ψ‘𝑥)
+ 1) / 𝑥))) |
338 | 335, 326,
336, 337 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤
(((ψ‘𝑥) + 1) /
𝑥))) |
339 | 333, 338 | mpbid 231 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥)) |
340 | 320 | leabsd 15126 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥))) |
341 | 243, 320,
331, 339, 340 | letrd 11132 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥))) |
342 | 329, 341 | eqbrtrd 5096 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥))) |
343 | 342 | adantrr 714 |
. . . . . . . . 9
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤
(abs‘(((ψ‘𝑥) + 1) / 𝑥))) |
344 | 278, 319,
320, 296, 343 | o1le 15364 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ∈
𝑂(1)) |
345 | | o1const 15329 |
. . . . . . . . . 10
⊢
((ℝ+ ⊆ ℝ ∧ 1 ∈ ℂ) →
(𝑥 ∈
ℝ+ ↦ 1) ∈ 𝑂(1)) |
346 | 14, 28, 345 | mp2an 689 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ 1) ∈ 𝑂(1) |
347 | 346 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ 1) ∈ 𝑂(1)) |
348 | 296, 297,
344, 347 | o1sub2 15335 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) ∈
𝑂(1)) |
349 | 234, 245,
295, 348 | o1sub2 15335 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈
𝑂(1)) |
350 | 13, 349 | o1res2 15272 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈
𝑂(1)) |
351 | 228, 350 | eqeltrrid 2844 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈
𝑂(1)) |
352 | 16, 351 | eqeltrd 2839 |
. . 3
⊢ (⊤
→ ((𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈
𝑂(1)) |
353 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
354 | 353, 45 | fmpti 6986 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 +
1)))):ℝ⟶ℂ |
355 | 354 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 +
1)))):ℝ⟶ℂ) |
356 | | ssidd 3944 |
. . . 4
⊢ (⊤
→ ℝ ⊆ ℝ) |
357 | 355, 356,
278 | o1resb 15275 |
. . 3
⊢ (⊤
→ ((𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) ↔ ((𝑥 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈
𝑂(1))) |
358 | 352, 357 | mpbird 256 |
. 2
⊢ (⊤
→ (𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈
𝑂(1)) |
359 | 358 | mptru 1546 |
1
⊢ (𝑥 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) |