| Step | Hyp | Ref
| Expression |
| 1 | | 1re 11261 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
| 2 | | elicopnf 13485 |
. . . . . . . . . . 11
⊢ (1 ∈
ℝ → (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
| 3 | 1, 2 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 1
≤ 𝑥)) |
| 4 | 3 | simplbi 497 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
𝑥 ∈
ℝ) |
| 5 | | 0red 11264 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) → 0
∈ ℝ) |
| 6 | | 1red 11262 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) → 1
∈ ℝ) |
| 7 | | 0lt1 11785 |
. . . . . . . . . . 11
⊢ 0 <
1 |
| 8 | 7 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) → 0
< 1) |
| 9 | 3 | simprbi 496 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) → 1
≤ 𝑥) |
| 10 | 5, 6, 4, 8, 9 | ltletrd 11421 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) → 0
< 𝑥) |
| 11 | 4, 10 | elrpd 13074 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) →
𝑥 ∈
ℝ+) |
| 12 | 11 | ssriv 3987 |
. . . . . . 7
⊢
(1[,)+∞) ⊆ ℝ+ |
| 13 | 12 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (1[,)+∞) ⊆ ℝ+) |
| 14 | | rpssre 13042 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
| 15 | 13, 14 | sstrdi 3996 |
. . . . 5
⊢ (⊤
→ (1[,)+∞) ⊆ ℝ) |
| 16 | 15 | resmptd 6058 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
| 17 | | chpcl 27167 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
| 18 | 4, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘𝑥) ∈
ℝ) |
| 19 | | peano2re 11434 |
. . . . . . . . . . 11
⊢
((ψ‘𝑥)
∈ ℝ → ((ψ‘𝑥) + 1) ∈ ℝ) |
| 20 | 18, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘𝑥) + 1)
∈ ℝ) |
| 21 | 11 | rprege0d 13084 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
| 22 | | flge0nn0 13860 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
(⌊‘𝑥) ∈
ℕ0) |
| 24 | | nn0p1nn 12565 |
. . . . . . . . . . 11
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
((⌊‘𝑥) + 1)
∈ ℕ) |
| 26 | 20, 25 | nndivred 12320 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
(((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
∈ ℝ) |
| 27 | 26 | recnd 11289 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) →
(((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
∈ ℂ) |
| 28 | | ax-1cn 11213 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
| 29 | | subcl 11507 |
. . . . . . . 8
⊢
(((((ψ‘𝑥)
+ 1) / ((⌊‘𝑥) +
1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈
ℂ) |
| 30 | 27, 28, 29 | sylancl 586 |
. . . . . . 7
⊢ (𝑥 ∈ (1[,)+∞) →
((((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
− 1) ∈ ℂ) |
| 31 | | fzfid 14014 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ →
(1...(⌊‘𝑥))
∈ Fin) |
| 32 | | elfznn 13593 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
| 33 | 32 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
| 34 | | nnrp 13046 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
| 35 | | pntrval.r |
. . . . . . . . . . . . . . 15
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
| 36 | 35 | pntrf 27607 |
. . . . . . . . . . . . . 14
⊢ 𝑅:ℝ+⟶ℝ |
| 37 | 36 | ffvelcdmi 7103 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℝ+
→ (𝑅‘𝑛) ∈
ℝ) |
| 38 | 34, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑅‘𝑛) ∈ ℝ) |
| 39 | | peano2nn 12278 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
| 40 | | nnmulcl 12290 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) →
(𝑛 · (𝑛 + 1)) ∈
ℕ) |
| 41 | 39, 40 | mpdan 687 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
| 42 | 38, 41 | nndivred 12320 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
| 43 | 33, 42 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
| 44 | 31, 43 | fsumrecl 15770 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
| 45 | 44 | recnd 11289 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
| 46 | 4, 45 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
| 47 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛)) |
| 48 | | fvoveq1 7454 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1))) |
| 49 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑚 − 1) = (𝑛 − 1)) |
| 50 | 48, 49 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) |
| 51 | 47, 50 | jca 511 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((1 / 𝑚) = (1 / 𝑛) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) |
| 52 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (1 / 𝑚) = (1 / (𝑛 + 1))) |
| 53 | | fvoveq1 7454 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) −
1))) |
| 54 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (𝑚 − 1) = ((𝑛 + 1) − 1)) |
| 55 | 53, 54 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) =
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) |
| 56 | 52, 55 | jca 511 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → ((1 / 𝑚) = (1 / (𝑛 + 1)) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) =
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)))) |
| 57 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (1 / 𝑚) = (1 / 1)) |
| 58 | | 1div1e1 11958 |
. . . . . . . . . . . 12
⊢ (1 / 1) =
1 |
| 59 | 57, 58 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → (1 / 𝑚) = 1) |
| 60 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) |
| 61 | | 1m1e0 12338 |
. . . . . . . . . . . . . . . 16
⊢ (1
− 1) = 0 |
| 62 | 60, 61 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) |
| 63 | 62 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) =
(ψ‘0)) |
| 64 | | 2pos 12369 |
. . . . . . . . . . . . . . 15
⊢ 0 <
2 |
| 65 | | 0re 11263 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
| 66 | | chpeq0 27252 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
ℝ → ((ψ‘0) = 0 ↔ 0 < 2)) |
| 67 | 65, 66 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
((ψ‘0) = 0 ↔ 0 < 2) |
| 68 | 64, 67 | mpbir 231 |
. . . . . . . . . . . . . 14
⊢
(ψ‘0) = 0 |
| 69 | 63, 68 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) =
0) |
| 70 | 69, 62 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = (0 −
0)) |
| 71 | | 0m0e0 12386 |
. . . . . . . . . . . 12
⊢ (0
− 0) = 0 |
| 72 | 70, 71 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) =
0) |
| 73 | 59, 72 | jca 511 |
. . . . . . . . . 10
⊢ (𝑚 = 1 → ((1 / 𝑚) = 1 ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) =
0)) |
| 74 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (1 / 𝑚) = (1 / ((⌊‘𝑥) + 1))) |
| 75 | | fvoveq1 7454 |
. . . . . . . . . . . 12
⊢ (𝑚 = ((⌊‘𝑥) + 1) →
(ψ‘(𝑚 − 1))
= (ψ‘(((⌊‘𝑥) + 1) − 1))) |
| 76 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑚 − 1) =
(((⌊‘𝑥) + 1)
− 1)) |
| 77 | 75, 76 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) →
((ψ‘(𝑚 −
1)) − (𝑚 − 1))
= ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) |
| 78 | 74, 77 | jca 511 |
. . . . . . . . . 10
⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((1 / 𝑚) = (1 / ((⌊‘𝑥) + 1)) ∧
((ψ‘(𝑚 −
1)) − (𝑚 − 1))
= ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1)))) |
| 79 | | nnuz 12921 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
| 80 | 25, 79 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
((⌊‘𝑥) + 1)
∈ (ℤ≥‘1)) |
| 81 | | elfznn 13593 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈
(1...((⌊‘𝑥) +
1)) → 𝑚 ∈
ℕ) |
| 82 | 81 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℕ) |
| 83 | 82 | nnrecred 12317 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (1 / 𝑚) ∈
ℝ) |
| 84 | 83 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (1 / 𝑚) ∈
ℂ) |
| 85 | 82 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℝ) |
| 86 | | peano2rem 11576 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℝ → (𝑚 − 1) ∈
ℝ) |
| 87 | 85, 86 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (𝑚 − 1)
∈ ℝ) |
| 88 | | chpcl 27167 |
. . . . . . . . . . . . 13
⊢ ((𝑚 − 1) ∈ ℝ
→ (ψ‘(𝑚
− 1)) ∈ ℝ) |
| 89 | 87, 88 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (ψ‘(𝑚
− 1)) ∈ ℝ) |
| 90 | 89, 87 | resubcld 11691 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℝ) |
| 91 | 90 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑚 ∈
(1...((⌊‘𝑥) +
1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℂ) |
| 92 | 51, 56, 73, 78, 80, 84, 91 | fsumparts 15842 |
. . . . . . . . 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 13838 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
(⌊‘𝑥) ∈
ℤ) |
| 94 | | fzval3 13773 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑥)
∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) |
| 95 | 93, 94 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
(1...(⌊‘𝑥)) =
(1..^((⌊‘𝑥) +
1))) |
| 96 | 95 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
(1..^((⌊‘𝑥) +
1)) = (1...(⌊‘𝑥))) |
| 97 | 32 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
| 98 | 97 | nncnd 12282 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℂ) |
| 99 | | pncan 11514 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
| 100 | 98, 28, 99 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
= 𝑛) |
| 101 | 97 | nnred 12281 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ) |
| 102 | 100, 101 | eqeltrd 2841 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
∈ ℝ) |
| 103 | | chpcl 27167 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 + 1) − 1) ∈ ℝ
→ (ψ‘((𝑛 +
1) − 1)) ∈ ℝ) |
| 104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) ∈ ℝ) |
| 105 | 104 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) ∈ ℂ) |
| 106 | 102 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
∈ ℂ) |
| 107 | | peano2rem 11576 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈
ℝ) |
| 108 | 101, 107 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℝ) |
| 109 | | chpcl 27167 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 − 1) ∈ ℝ
→ (ψ‘(𝑛
− 1)) ∈ ℝ) |
| 110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑛
− 1)) ∈ ℝ) |
| 111 | 110 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑛
− 1)) ∈ ℂ) |
| 112 | | 1cnd 11256 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℂ) |
| 113 | 98, 112 | subcld 11620 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℂ) |
| 114 | 105, 106,
111, 113 | sub4d 11669 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((ψ‘((𝑛 +
1) − 1)) − ((𝑛
+ 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = (((ψ‘((𝑛 + 1) − 1)) −
(ψ‘(𝑛 −
1))) − (((𝑛 + 1)
− 1) − (𝑛
− 1)))) |
| 115 | | vmacl 27161 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
| 116 | 97, 115 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
| 117 | 116 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℂ) |
| 118 | | nnm1nn0 12567 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
| 119 | 97, 118 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℕ0) |
| 120 | | chpp1 27198 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 − 1) ∈
ℕ0 → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) +
(Λ‘((𝑛 −
1) + 1)))) |
| 121 | 119, 120 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛
− 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) +
1)))) |
| 122 | | npcan 11517 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
| 123 | 98, 28, 122 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 − 1) + 1)
= 𝑛) |
| 124 | 123, 100 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 − 1) + 1)
= ((𝑛 + 1) −
1)) |
| 125 | 124 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛
− 1) + 1)) = (ψ‘((𝑛 + 1) − 1))) |
| 126 | 123 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘((𝑛
− 1) + 1)) = (Λ‘𝑛)) |
| 127 | 126 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑛
− 1)) + (Λ‘((𝑛 − 1) + 1))) = ((ψ‘(𝑛 − 1)) +
(Λ‘𝑛))) |
| 128 | 121, 125,
127 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛))) |
| 129 | 111, 117,
128 | mvrladdd 11676 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘((𝑛 +
1) − 1)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛)) |
| 130 | | peano2cn 11433 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℂ → (𝑛 + 1) ∈
ℂ) |
| 131 | 98, 130 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 + 1) ∈
ℂ) |
| 132 | 131, 98, 112 | nnncan2d 11655 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) − 1)
− (𝑛 − 1)) =
((𝑛 + 1) − 𝑛)) |
| 133 | | pncan2 11515 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 𝑛) =
1) |
| 134 | 98, 28, 133 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) −
𝑛) = 1) |
| 135 | 132, 134 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) − 1)
− (𝑛 − 1)) =
1) |
| 136 | 129, 135 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((ψ‘((𝑛 +
1) − 1)) − (ψ‘(𝑛 − 1))) − (((𝑛 + 1) − 1) − (𝑛 − 1))) = ((Λ‘𝑛) − 1)) |
| 137 | 114, 136 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((ψ‘((𝑛 +
1) − 1)) − ((𝑛
+ 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = ((Λ‘𝑛) − 1)) |
| 138 | 137 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 / 𝑛) ·
(((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = ((1 / 𝑛) · ((Λ‘𝑛) − 1))) |
| 139 | | peano2rem 11576 |
. . . . . . . . . . . . . 14
⊢
((Λ‘𝑛)
∈ ℝ → ((Λ‘𝑛) − 1) ∈ ℝ) |
| 140 | 116, 139 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
− 1) ∈ ℝ) |
| 141 | 140 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
− 1) ∈ ℂ) |
| 142 | 97 | nnne0d 12316 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ≠
0) |
| 143 | 141, 98, 142 | divrec2d 12047 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
− 1) / 𝑛) = ((1 /
𝑛) ·
((Λ‘𝑛) −
1))) |
| 144 | 138, 143 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 / 𝑛) ·
(((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = (((Λ‘𝑛) − 1) / 𝑛)) |
| 145 | 96, 144 | sumeq12rdv 15743 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))((1 / 𝑛) ·
(((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) |
| 146 | 23 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (1[,)+∞) →
(⌊‘𝑥) ∈
ℂ) |
| 147 | | pncan 11514 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⌊‘𝑥)
∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑥) + 1) − 1) =
(⌊‘𝑥)) |
| 148 | 146, 28, 147 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (1[,)+∞) →
(((⌊‘𝑥) + 1)
− 1) = (⌊‘𝑥)) |
| 149 | 148 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘(((⌊‘𝑥) + 1) − 1)) =
(ψ‘(⌊‘𝑥))) |
| 150 | | chpfl 27193 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ →
(ψ‘(⌊‘𝑥)) = (ψ‘𝑥)) |
| 151 | 4, 150 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘(⌊‘𝑥)) = (ψ‘𝑥)) |
| 152 | 149, 151 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘𝑥)) |
| 153 | 152 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1)) = ((ψ‘𝑥) − (((⌊‘𝑥) + 1) − 1))) |
| 154 | 18 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) →
(ψ‘𝑥) ∈
ℂ) |
| 155 | 25 | nncnd 12282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) →
((⌊‘𝑥) + 1)
∈ ℂ) |
| 156 | | 1cnd 11256 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) → 1
∈ ℂ) |
| 157 | 154, 155,
156 | subsub3d 11650 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘𝑥) −
(((⌊‘𝑥) + 1)
− 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) |
| 158 | 153, 157 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) |
| 159 | 158 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) = ((1 / ((⌊‘𝑥) + 1)) · (((ψ‘𝑥) + 1) −
((⌊‘𝑥) +
1)))) |
| 160 | 25 | nnrecred 12317 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) → (1
/ ((⌊‘𝑥) + 1))
∈ ℝ) |
| 161 | 160 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) → (1
/ ((⌊‘𝑥) + 1))
∈ ℂ) |
| 162 | | peano2cn 11433 |
. . . . . . . . . . . . . . 15
⊢
((ψ‘𝑥)
∈ ℂ → ((ψ‘𝑥) + 1) ∈ ℂ) |
| 163 | 154, 162 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) →
((ψ‘𝑥) + 1)
∈ ℂ) |
| 164 | 161, 163,
155 | subdid 11719 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) = (((1 /
((⌊‘𝑥) + 1))
· ((ψ‘𝑥) +
1)) − ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1)))) |
| 165 | 25 | nnne0d 12316 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1[,)+∞) →
((⌊‘𝑥) + 1)
≠ 0) |
| 166 | 163, 155,
165 | divrec2d 12047 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1[,)+∞) →
(((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1)) =
((1 / ((⌊‘𝑥) +
1)) · ((ψ‘𝑥) + 1))) |
| 167 | 166 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · ((ψ‘𝑥) + 1)) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) |
| 168 | 155, 165 | recid2d 12039 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · ((⌊‘𝑥) + 1)) = 1) |
| 169 | 167, 168 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1[,)+∞) →
(((1 / ((⌊‘𝑥) +
1)) · ((ψ‘𝑥) + 1)) − ((1 / ((⌊‘𝑥) + 1)) ·
((⌊‘𝑥) + 1))) =
((((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
− 1)) |
| 170 | 159, 164,
169 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
((1 / ((⌊‘𝑥) +
1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) |
| 171 | 28 | mul01i 11451 |
. . . . . . . . . . . . 13
⊢ (1
· 0) = 0 |
| 172 | 171 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) → (1
· 0) = 0) |
| 173 | 170, 172 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
(((1 / ((⌊‘𝑥) +
1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) −
(((⌊‘𝑥) + 1)
− 1))) − (1 · 0)) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) −
0)) |
| 174 | 30 | subid1d 11609 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
(((((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
− 1) − 0) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) |
| 175 | 173, 174 | eqtrd 2777 |
. . . . . . . . . 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 12317 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 ·
(𝑛 + 1))) ∈
ℝ) |
| 178 | 177 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 ·
(𝑛 + 1))) ∈
ℂ) |
| 179 | 97, 38 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘𝑛) ∈
ℝ) |
| 180 | 179 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘𝑛) ∈
ℂ) |
| 181 | 178, 180 | mulneg1d 11716 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (-(1 / (𝑛 ·
(𝑛 + 1))) · (𝑅‘𝑛)) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅‘𝑛))) |
| 182 | 98, 112 | mulcld 11281 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · 1)
∈ ℂ) |
| 183 | 98, 131 | mulcld 11281 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · (𝑛 + 1)) ∈
ℂ) |
| 184 | 176 | nnne0d 12316 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · (𝑛 + 1)) ≠ 0) |
| 185 | 131, 182,
183, 184 | divsubdird 12082 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) −
(𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1))))) |
| 186 | 98 | mulridd 11278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 · 1) =
𝑛) |
| 187 | 186 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) −
(𝑛 · 1)) = ((𝑛 + 1) − 𝑛)) |
| 188 | 187, 134 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) −
(𝑛 · 1)) =
1) |
| 189 | 188 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) −
(𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (1 / (𝑛 · (𝑛 + 1)))) |
| 190 | 131 | mulridd 11278 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) · 1)
= (𝑛 + 1)) |
| 191 | 131, 98 | mulcomd 11282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) ·
𝑛) = (𝑛 · (𝑛 + 1))) |
| 192 | 190, 191 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) ·
1) / ((𝑛 + 1) ·
𝑛)) = ((𝑛 + 1) / (𝑛 · (𝑛 + 1)))) |
| 193 | 97, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 + 1) ∈
ℕ) |
| 194 | 193 | nnne0d 12316 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 + 1) ≠
0) |
| 195 | 112, 98, 131, 142, 194 | divcan5d 12069 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) ·
1) / ((𝑛 + 1) ·
𝑛)) = (1 / 𝑛)) |
| 196 | 192, 195 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) / (𝑛 · (𝑛 + 1))) = (1 / 𝑛)) |
| 197 | 112, 131,
98, 194, 142 | divcan5d 12069 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 · 1) /
(𝑛 · (𝑛 + 1))) = (1 / (𝑛 + 1))) |
| 198 | 196, 197 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1)))) = ((1 / 𝑛) − (1 / (𝑛 + 1)))) |
| 199 | 185, 189,
198 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 ·
(𝑛 + 1))) = ((1 / 𝑛) − (1 / (𝑛 + 1)))) |
| 200 | 199 | negeqd 11502 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ -(1 / (𝑛 ·
(𝑛 + 1))) = -((1 / 𝑛) − (1 / (𝑛 + 1)))) |
| 201 | 97 | nnrecred 12317 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑛) ∈
ℝ) |
| 202 | 201 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑛) ∈
ℂ) |
| 203 | 193 | nnrecred 12317 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 + 1)) ∈
ℝ) |
| 204 | 203 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑛 + 1)) ∈
ℂ) |
| 205 | 202, 204 | negsubdi2d 11636 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ -((1 / 𝑛) − (1
/ (𝑛 + 1))) = ((1 / (𝑛 + 1)) − (1 / 𝑛))) |
| 206 | 200, 205 | eqtr2d 2778 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 / (𝑛 + 1))
− (1 / 𝑛)) = -(1 /
(𝑛 · (𝑛 + 1)))) |
| 207 | 97 | nnrpd 13075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
| 208 | 100, 207 | eqeltrd 2841 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
∈ ℝ+) |
| 209 | 35 | pntrval 27606 |
. . . . . . . . . . . . . . . 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 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘((𝑛 + 1) − 1)) = (𝑅‘𝑛)) |
| 212 | 210, 211 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘((𝑛 +
1) − 1)) − ((𝑛
+ 1) − 1)) = (𝑅‘𝑛)) |
| 213 | 206, 212 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((1 / (𝑛 + 1))
− (1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) = (-(1 / (𝑛
· (𝑛 + 1))) ·
(𝑅‘𝑛))) |
| 214 | 180, 183,
184 | divrec2d 12047 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = ((1 / (𝑛 · (𝑛 + 1))) · (𝑅‘𝑛))) |
| 215 | 214 | negeqd 11502 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅‘𝑛))) |
| 216 | 181, 213,
215 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ (((1 / (𝑛 + 1))
− (1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) = -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 217 | 96, 216 | sumeq12rdv 15743 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((1 / (𝑛 + 1)) −
(1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) = Σ𝑛
∈ (1...(⌊‘𝑥))-((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 218 | | fzfid 14014 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) →
(1...(⌊‘𝑥))
∈ Fin) |
| 219 | 97, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
| 220 | 219 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (1[,)+∞) ∧
𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
| 221 | 218, 220 | fsumneg 15823 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1...(⌊‘𝑥))-((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 222 | 217, 221 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((1 / (𝑛 + 1)) −
(1 / 𝑛)) ·
((ψ‘((𝑛 + 1)
− 1)) − ((𝑛 +
1) − 1))) = -Σ𝑛
∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 223 | 175, 222 | oveq12d 7449 |
. . . . . . . . 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 2785 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
| 225 | 30, 46 | subnegd 11627 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) →
(((((ψ‘𝑥) + 1) /
((⌊‘𝑥) + 1))
− 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) +
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
| 226 | 224, 225 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑥 ∈ (1[,)+∞) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
| 227 | 30, 46, 226 | mvrladdd 11676 |
. . . . . 6
⊢ (𝑥 ∈ (1[,)+∞) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) = Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 228 | 227 | mpteq2ia 5245 |
. . . . 5
⊢ (𝑥 ∈ (1[,)+∞) ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 229 | | fzfid 14014 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin) |
| 230 | 32 | adantl 481 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
| 231 | 230, 115 | syl 17 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) |
| 232 | 231, 139 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) −
1) ∈ ℝ) |
| 233 | 232, 230 | nndivred 12320 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛)
− 1) / 𝑛) ∈
ℝ) |
| 234 | 229, 233 | fsumrecl 15770 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) ∈
ℝ) |
| 235 | | rpre 13043 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
| 236 | 235 | adantl 481 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ) |
| 237 | 236, 17 | syl 17 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (ψ‘𝑥) ∈ ℝ) |
| 238 | 237, 19 | syl 17 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) + 1) ∈ ℝ) |
| 239 | | rprege0 13050 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
| 240 | 239, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℕ0) |
| 241 | 240 | adantl 481 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (⌊‘𝑥) ∈
ℕ0) |
| 242 | 241, 24 | syl 17 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((⌊‘𝑥) + 1) ∈ ℕ) |
| 243 | 238, 242 | nndivred 12320 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ) |
| 244 | | peano2rem 11576 |
. . . . . . . 8
⊢
((((ψ‘𝑥) +
1) / ((⌊‘𝑥) +
1)) ∈ ℝ → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈
ℝ) |
| 245 | 243, 244 | syl 17 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈
ℝ) |
| 246 | | reex 11246 |
. . . . . . . . . . . 12
⊢ ℝ
∈ V |
| 247 | 246, 14 | ssexi 5322 |
. . . . . . . . . . 11
⊢
ℝ+ ∈ V |
| 248 | 247 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ ℝ+ ∈ V) |
| 249 | 231, 230 | nndivred 12320 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℝ) |
| 250 | 249 | recnd 11289 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℂ) |
| 251 | 229, 250 | fsumcl 15769 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
| 252 | | relogcl 26617 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
| 253 | 252 | adantl 481 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ∈ ℝ) |
| 254 | 253 | recnd 11289 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ∈ ℂ) |
| 255 | 251, 254 | subcld 11620 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ) |
| 256 | 230 | nnrecred 12317 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈
ℝ) |
| 257 | 229, 256 | fsumrecl 15770 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℝ) |
| 258 | 257, 253 | resubcld 11691 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℝ) |
| 259 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)))) |
| 260 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥)))) |
| 261 | 248, 255,
258, 259, 260 | offval2 7717 |
. . . . . . . . 9
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))))) |
| 262 | 256 | recnd 11289 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈
ℂ) |
| 263 | 229, 250,
262 | fsumsub 15824 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))) |
| 264 | 231 | recnd 11289 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℂ) |
| 265 | | 1cnd 11256 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℂ) |
| 266 | 230 | nncnd 12282 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ) |
| 267 | 230 | nnne0d 12316 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0) |
| 268 | 264, 265,
266, 267 | divsubdird 12082 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛)
− 1) / 𝑛) =
(((Λ‘𝑛) /
𝑛) − (1 / 𝑛))) |
| 269 | 268 | sumeq2dv 15738 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛))) |
| 270 | 257 | recnd 11289 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℂ) |
| 271 | 251, 270,
254 | nnncan2d 11655 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))) |
| 272 | 263, 269,
271 | 3eqtr4rd 2788 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) |
| 273 | 272 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))) |
| 274 | 261, 273 | eqtrd 2777 |
. . . . . . . 8
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))) |
| 275 | | vmadivsum 27526 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) |
| 276 | 14 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ ℝ+ ⊆ ℝ) |
| 277 | 258 | recnd 11289 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℂ) |
| 278 | | 1red 11262 |
. . . . . . . . . 10
⊢ (⊤
→ 1 ∈ ℝ) |
| 279 | | harmoniclbnd 27052 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ≤
Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛)) |
| 280 | 279 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛)) |
| 281 | 253, 257,
280 | abssubge0d 15470 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) |
| 282 | 281 | adantrr 717 |
. . . . . . . . . . 11
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) |
| 283 | 235 | ad2antrl 728 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
| 284 | | simprr 773 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥) |
| 285 | | harmonicubnd 27053 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) → Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) ≤ ((log‘𝑥) + 1)) |
| 286 | 283, 284,
285 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1)) |
| 287 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 1 ∈ ℝ) |
| 288 | 257, 253,
287 | lesubadd2d 11862 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))) |
| 289 | 288 | adantrr 717 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))) |
| 290 | 286, 289 | mpbird 257 |
. . . . . . . . . . 11
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1) |
| 291 | 282, 290 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) − (log‘𝑥))) ≤ 1) |
| 292 | 276, 277,
278, 278, 291 | elo1d 15572 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) |
| 293 | | o1sub 15652 |
. . . . . . . . 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 2842 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) ∈
𝑂(1)) |
| 296 | 243 | recnd 11289 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ) |
| 297 | | 1cnd 11256 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 1 ∈ ℂ) |
| 298 | 237 | recnd 11289 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (ψ‘𝑥) ∈ ℂ) |
| 299 | | rpcnne0 13053 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
| 300 | 299 | adantl 481 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
| 301 | | divdir 11947 |
. . . . . . . . . . . 12
⊢
(((ψ‘𝑥)
∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) |
| 302 | 298, 297,
300, 301 | syl3anc 1373 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) |
| 303 | 302 | mpteq2dva 5242 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
(((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))) |
| 304 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ+) |
| 305 | 237, 304 | rerpdivcld 13108 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ) |
| 306 | | rpreccl 13061 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ+) |
| 307 | 306 | adantl 481 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1 / 𝑥) ∈
ℝ+) |
| 308 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
((ψ‘𝑥) / 𝑥))) |
| 309 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) |
| 310 | 248, 305,
307, 308, 309 | offval2 7717 |
. . . . . . . . . . 11
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) = (𝑥 ∈ ℝ+ ↦
(((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))) |
| 311 | | chpo1ub 27524 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈
𝑂(1) |
| 312 | | divrcnv 15888 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℂ → (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) |
| 313 | 28, 312 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
↦ (1 / 𝑥))
⇝𝑟 0 |
| 314 | | rlimo1 15653 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
↦ (1 / 𝑥))
⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) ∈
𝑂(1)) |
| 315 | 313, 314 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) |
| 316 | | o1add 15650 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈ 𝑂(1)
∧ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∘f +
(𝑥 ∈
ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1)) |
| 317 | 311, 315,
316 | sylancr 587 |
. . . . . . . . . . 11
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 /
𝑥))) ∈
𝑂(1)) |
| 318 | 310, 317 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1)) |
| 319 | 303, 318 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) ∈ 𝑂(1)) |
| 320 | 238, 304 | rerpdivcld 13108 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℝ) |
| 321 | | chpge0 27169 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ → 0 ≤
(ψ‘𝑥)) |
| 322 | 236, 321 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 0 ≤ (ψ‘𝑥)) |
| 323 | 237, 322 | ge0p1rpd 13107 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) + 1) ∈
ℝ+) |
| 324 | 323 | rprege0d 13084 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 ≤
((ψ‘𝑥) +
1))) |
| 325 | 242 | nnrpd 13075 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((⌊‘𝑥) + 1) ∈
ℝ+) |
| 326 | 325 | rpregt0d 13083 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 <
((⌊‘𝑥) +
1))) |
| 327 | | divge0 12137 |
. . . . . . . . . . . . 13
⊢
(((((ψ‘𝑥)
+ 1) ∈ ℝ ∧ 0 ≤ ((ψ‘𝑥) + 1)) ∧ (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0
< ((⌊‘𝑥) +
1))) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) |
| 328 | 324, 326,
327 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) |
| 329 | 243, 328 | absidd 15461 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) |
| 330 | 320 | recnd 11289 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℂ) |
| 331 | 330 | abscld 15475 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / 𝑥)) ∈ ℝ) |
| 332 | | fllep1 13841 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
| 333 | 236, 332 | syl 17 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
| 334 | | rpregt0 13049 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
| 335 | 334 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 < 𝑥)) |
| 336 | 323 | rpregt0d 13083 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 <
((ψ‘𝑥) +
1))) |
| 337 | | lediv2 12158 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℝ ∧ 0 <
𝑥) ∧
(((⌊‘𝑥) + 1)
∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1)) ∧ (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0
< ((ψ‘𝑥) +
1))) → (𝑥 ≤
((⌊‘𝑥) + 1)
↔ (((ψ‘𝑥) +
1) / ((⌊‘𝑥) +
1)) ≤ (((ψ‘𝑥)
+ 1) / 𝑥))) |
| 338 | 335, 326,
336, 337 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤
(((ψ‘𝑥) + 1) /
𝑥))) |
| 339 | 333, 338 | mpbid 232 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥)) |
| 340 | 320 | leabsd 15453 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥))) |
| 341 | 243, 320,
331, 339, 340 | letrd 11418 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥))) |
| 342 | 329, 341 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥))) |
| 343 | 342 | adantrr 717 |
. . . . . . . . 9
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤
(abs‘(((ψ‘𝑥) + 1) / 𝑥))) |
| 344 | 278, 319,
320, 296, 343 | o1le 15689 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ∈
𝑂(1)) |
| 345 | | o1const 15656 |
. . . . . . . . . 10
⊢
((ℝ+ ⊆ ℝ ∧ 1 ∈ ℂ) →
(𝑥 ∈
ℝ+ ↦ 1) ∈ 𝑂(1)) |
| 346 | 14, 28, 345 | mp2an 692 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
↦ 1) ∈ 𝑂(1) |
| 347 | 346 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ 1) ∈ 𝑂(1)) |
| 348 | 296, 297,
344, 347 | o1sub2 15662 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) ∈
𝑂(1)) |
| 349 | 234, 245,
295, 348 | o1sub2 15662 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈
𝑂(1)) |
| 350 | 13, 349 | o1res2 15599 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈
𝑂(1)) |
| 351 | 228, 350 | eqeltrrid 2846 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈
𝑂(1)) |
| 352 | 16, 351 | eqeltrd 2841 |
. . 3
⊢ (⊤
→ ((𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈
𝑂(1)) |
| 353 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 354 | 353, 45 | fmpti 7132 |
. . . . 5
⊢ (𝑥 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 +
1)))):ℝ⟶ℂ |
| 355 | 354 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 +
1)))):ℝ⟶ℂ) |
| 356 | | ssidd 4007 |
. . . 4
⊢ (⊤
→ ℝ ⊆ ℝ) |
| 357 | 355, 356,
278 | o1resb 15602 |
. . 3
⊢ (⊤
→ ((𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) ↔ ((𝑥 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈
𝑂(1))) |
| 358 | 352, 357 | mpbird 257 |
. 2
⊢ (⊤
→ (𝑥 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈
𝑂(1)) |
| 359 | 358 | mptru 1547 |
1
⊢ (𝑥 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) |