| Step | Hyp | Ref
| Expression |
| 1 | | rpre 13043 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
| 2 | | chpcl 27167 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
| 3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℝ) |
| 4 | 3 | recnd 11289 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℂ) |
| 5 | | rprege0 13050 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
| 6 | | flge0nn0 13860 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
| 7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℕ0) |
| 8 | | nn0p1nn 12565 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
| 9 | 7, 8 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ ((⌊‘𝑥) +
1) ∈ ℕ) |
| 10 | 9 | nnrpd 13075 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((⌊‘𝑥) +
1) ∈ ℝ+) |
| 11 | 10 | relogcld 26665 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘((⌊‘𝑥) + 1)) ∈ ℝ) |
| 12 | 11 | recnd 11289 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (log‘((⌊‘𝑥) + 1)) ∈ ℂ) |
| 13 | | relogcl 26617 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
| 14 | 13 | recnd 11289 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℂ) |
| 15 | 12, 14 | subcld 11620 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℂ) |
| 16 | 4, 15 | mulcld 11281 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ ℂ) |
| 17 | | fzfid 14014 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) ∈ Fin) |
| 18 | | elfznn 13593 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
| 19 | 18 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
| 20 | 19 | nnrpd 13075 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
| 21 | | 1rp 13038 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ |
| 22 | | rpaddcl 13057 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℝ+
∧ 1 ∈ ℝ+) → (𝑛 + 1) ∈
ℝ+) |
| 23 | 21, 22 | mpan2 691 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (𝑛 + 1) ∈
ℝ+) |
| 24 | 23 | relogcld 26665 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ (log‘(𝑛 + 1))
∈ ℝ) |
| 25 | | relogcl 26617 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ (log‘𝑛) ∈
ℝ) |
| 26 | 24, 25 | resubcld 11691 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ ((log‘(𝑛 + 1))
− (log‘𝑛))
∈ ℝ) |
| 27 | | rpre 13043 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℝ) |
| 28 | | chpcl 27167 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ →
(ψ‘𝑛) ∈
ℝ) |
| 29 | 27, 28 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ (ψ‘𝑛)
∈ ℝ) |
| 30 | 26, 29 | remulcld 11291 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛))
∈ ℝ) |
| 31 | 30 | recnd 11289 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ+
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛))
∈ ℂ) |
| 32 | 20, 31 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛))
∈ ℂ) |
| 33 | 17, 32 | fsumcl 15769 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ) |
| 34 | | rpcnne0 13053 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
| 35 | | divsubdir 11961 |
. . . . . 6
⊢
((((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ ℂ ∧ Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → ((((ψ‘𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) / 𝑥) = ((((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) |
| 36 | 16, 33, 34, 35 | syl3anc 1373 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) / 𝑥) = ((((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) |
| 37 | 4, 12 | mulcld 11281 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· (log‘((⌊‘𝑥) + 1))) ∈ ℂ) |
| 38 | 4, 14 | mulcld 11281 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· (log‘𝑥))
∈ ℂ) |
| 39 | 37, 38, 33 | sub32d 11652 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· (log‘((⌊‘𝑥) + 1))) − ((ψ‘𝑥) · (log‘𝑥))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = ((((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) − ((ψ‘𝑥) · (log‘𝑥)))) |
| 40 | 4, 12, 14 | subdid 11719 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) = (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) −
((ψ‘𝑥) ·
(log‘𝑥)))) |
| 41 | 40 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = ((((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1))) − ((ψ‘𝑥) · (log‘𝑥))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)))) |
| 42 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (log‘𝑚) = (log‘𝑛)) |
| 43 | | fvoveq1 7454 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1))) |
| 44 | 42, 43 | jca 511 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((log‘𝑚) = (log‘𝑛) ∧ (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1)))) |
| 45 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (log‘𝑚) = (log‘(𝑛 + 1))) |
| 46 | | fvoveq1 7454 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) −
1))) |
| 47 | 45, 46 | jca 511 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → ((log‘𝑚) = (log‘(𝑛 + 1)) ∧ (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) −
1)))) |
| 48 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (log‘𝑚) =
(log‘1)) |
| 49 | | log1 26627 |
. . . . . . . . . . . 12
⊢
(log‘1) = 0 |
| 50 | 48, 49 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → (log‘𝑚) = 0) |
| 51 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) |
| 52 | | 1m1e0 12338 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) = 0 |
| 53 | 51, 52 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) |
| 54 | 53 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) =
(ψ‘0)) |
| 55 | | 2pos 12369 |
. . . . . . . . . . . . 13
⊢ 0 <
2 |
| 56 | | 0re 11263 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
| 57 | | chpeq0 27252 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
ℝ → ((ψ‘0) = 0 ↔ 0 < 2)) |
| 58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
((ψ‘0) = 0 ↔ 0 < 2) |
| 59 | 55, 58 | mpbir 231 |
. . . . . . . . . . . 12
⊢
(ψ‘0) = 0 |
| 60 | 54, 59 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) =
0) |
| 61 | 50, 60 | jca 511 |
. . . . . . . . . 10
⊢ (𝑚 = 1 → ((log‘𝑚) = 0 ∧ (ψ‘(𝑚 − 1)) =
0)) |
| 62 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (log‘𝑚) =
(log‘((⌊‘𝑥) + 1))) |
| 63 | | fvoveq1 7454 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) →
(ψ‘(𝑚 − 1))
= (ψ‘(((⌊‘𝑥) + 1) − 1))) |
| 64 | 62, 63 | jca 511 |
. . . . . . . . . 10
⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((log‘𝑚) =
(log‘((⌊‘𝑥) + 1)) ∧ (ψ‘(𝑚 − 1)) =
(ψ‘(((⌊‘𝑥) + 1) − 1)))) |
| 65 | | nnuz 12921 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
| 66 | 9, 65 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((⌊‘𝑥) +
1) ∈ (ℤ≥‘1)) |
| 67 | | elfznn 13593 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈
(1...((⌊‘𝑥) +
1)) → 𝑚 ∈
ℕ) |
| 68 | 67 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℕ) |
| 69 | 68 | nnrpd 13075 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℝ+) |
| 70 | 69 | relogcld 26665 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (log‘𝑚)
∈ ℝ) |
| 71 | 70 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (log‘𝑚)
∈ ℂ) |
| 72 | 68 | nnred 12281 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → 𝑚 ∈
ℝ) |
| 73 | | peano2rem 11576 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℝ → (𝑚 − 1) ∈
ℝ) |
| 74 | 72, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (𝑚 − 1)
∈ ℝ) |
| 75 | | chpcl 27167 |
. . . . . . . . . . . 12
⊢ ((𝑚 − 1) ∈ ℝ
→ (ψ‘(𝑚
− 1)) ∈ ℝ) |
| 76 | 74, 75 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (ψ‘(𝑚
− 1)) ∈ ℝ) |
| 77 | 76 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑚 ∈
(1...((⌊‘𝑥) +
1))) → (ψ‘(𝑚
− 1)) ∈ ℂ) |
| 78 | 44, 47, 61, 64, 66, 71, 77 | fsumparts 15842 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))((log‘𝑛) ·
((ψ‘((𝑛 + 1)
− 1)) − (ψ‘(𝑛 − 1)))) =
((((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0))
− Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((log‘(𝑛 + 1))
− (log‘𝑛))
· (ψ‘((𝑛 +
1) − 1))))) |
| 79 | 7 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℤ) |
| 80 | | fzval3 13773 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑥)
∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) |
| 81 | 79, 80 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) |
| 82 | 81 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥))) |
| 83 | | nnm1nn0 12567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
| 84 | 19, 83 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℕ0) |
| 85 | 84 | nn0red 12588 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℝ) |
| 86 | | chpcl 27167 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 − 1) ∈ ℝ
→ (ψ‘(𝑛
− 1)) ∈ ℝ) |
| 87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑛
− 1)) ∈ ℝ) |
| 88 | 87 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑛
− 1)) ∈ ℂ) |
| 89 | | vmacl 27161 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
| 90 | 19, 89 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
| 91 | 90 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℂ) |
| 92 | 19 | nncnd 12282 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℂ) |
| 93 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
| 94 | | pncan 11514 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 + 1)
− 1) = 𝑛) |
| 95 | 92, 93, 94 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
= 𝑛) |
| 96 | | npcan 11517 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
| 97 | 92, 93, 96 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 − 1) + 1)
= 𝑛) |
| 98 | 95, 97 | eqtr4d 2780 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑛 + 1) − 1)
= ((𝑛 − 1) +
1)) |
| 99 | 98 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) = (ψ‘((𝑛 − 1) + 1))) |
| 100 | | chpp1 27198 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 − 1) ∈
ℕ0 → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) +
(Λ‘((𝑛 −
1) + 1)))) |
| 101 | 84, 100 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛
− 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) +
1)))) |
| 102 | 97 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘((𝑛
− 1) + 1)) = (Λ‘𝑛)) |
| 103 | 102 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑛
− 1)) + (Λ‘((𝑛 − 1) + 1))) = ((ψ‘(𝑛 − 1)) +
(Λ‘𝑛))) |
| 104 | 99, 101, 103 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛))) |
| 105 | 88, 91, 104 | mvrladdd 11676 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘((𝑛 +
1) − 1)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛)) |
| 106 | 105 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘𝑛)
· ((ψ‘((𝑛
+ 1) − 1)) − (ψ‘(𝑛 − 1)))) = ((log‘𝑛) · (Λ‘𝑛))) |
| 107 | 20 | relogcld 26665 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℝ) |
| 108 | 107 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℂ) |
| 109 | 91, 108 | mulcomd 11282 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (log‘𝑛)) =
((log‘𝑛) ·
(Λ‘𝑛))) |
| 110 | 106, 109 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘𝑛)
· ((ψ‘((𝑛
+ 1) − 1)) − (ψ‘(𝑛 − 1)))) = ((Λ‘𝑛) · (log‘𝑛))) |
| 111 | 82, 110 | sumeq12rdv 15743 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))((log‘𝑛) ·
((ψ‘((𝑛 + 1)
− 1)) − (ψ‘(𝑛 − 1)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛))) |
| 112 | 7 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℂ) |
| 113 | | pncan 11514 |
. . . . . . . . . . . . . . . . 17
⊢
(((⌊‘𝑥)
∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑥) + 1) − 1) =
(⌊‘𝑥)) |
| 114 | 112, 93, 113 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
→ (((⌊‘𝑥)
+ 1) − 1) = (⌊‘𝑥)) |
| 115 | 114 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ (ψ‘(((⌊‘𝑥) + 1) − 1)) =
(ψ‘(⌊‘𝑥))) |
| 116 | | chpfl 27193 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ →
(ψ‘(⌊‘𝑥)) = (ψ‘𝑥)) |
| 117 | 1, 116 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ (ψ‘(⌊‘𝑥)) = (ψ‘𝑥)) |
| 118 | 115, 117 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘𝑥)) |
| 119 | 118 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) =
((log‘((⌊‘𝑥) + 1)) · (ψ‘𝑥))) |
| 120 | 12, 4 | mulcomd 11282 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) · (ψ‘𝑥)) = ((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1)))) |
| 121 | 119, 120 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) = ((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1)))) |
| 122 | | 0cn 11253 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℂ |
| 123 | 122 | mul01i 11451 |
. . . . . . . . . . . . 13
⊢ (0
· 0) = 0 |
| 124 | 123 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (0 · 0) = 0) |
| 125 | 121, 124 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0)) =
(((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1))) − 0)) |
| 126 | 37 | subid1d 11609 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· (log‘((⌊‘𝑥) + 1))) − 0) = ((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1)))) |
| 127 | 125, 126 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0)) =
((ψ‘𝑥) ·
(log‘((⌊‘𝑥) + 1)))) |
| 128 | 95 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘((𝑛 +
1) − 1)) = (ψ‘𝑛)) |
| 129 | 128 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘((𝑛 +
1) − 1))) = (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) |
| 130 | 82, 129 | sumeq12rdv 15743 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((log‘(𝑛 + 1))
− (log‘𝑛))
· (ψ‘((𝑛 +
1) − 1))) = Σ𝑛
∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) |
| 131 | 127, 130 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((((log‘((⌊‘𝑥) + 1)) ·
(ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0))
− Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((log‘(𝑛 + 1))
− (log‘𝑛))
· (ψ‘((𝑛 +
1) − 1)))) = (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)))) |
| 132 | 78, 111, 131 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) = (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)))) |
| 133 | 132 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) = ((((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) − ((ψ‘𝑥) · (log‘𝑥)))) |
| 134 | 39, 41, 133 | 3eqtr4d 2787 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥)))) |
| 135 | 134 | oveq1d 7446 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) |
| 136 | | div23 11941 |
. . . . . . 7
⊢
(((ψ‘𝑥)
∈ ℂ ∧ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((ψ‘𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) = (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) |
| 137 | 4, 15, 34, 136 | syl3anc 1373 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) = (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) |
| 138 | 137 | oveq1d 7446 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥)
· ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)) = ((((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) |
| 139 | 36, 135, 138 | 3eqtr3rd 2786 |
. . . 4
⊢ (𝑥 ∈ ℝ+
→ ((((ψ‘𝑥) /
𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) |
| 140 | 139 | mpteq2ia 5245 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ ((((ψ‘𝑥)
/ 𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) |
| 141 | | ovexd 7466 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ V) |
| 142 | | ovexd 7466 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥) ∈ V) |
| 143 | | reex 11246 |
. . . . . . . 8
⊢ ℝ
∈ V |
| 144 | | rpssre 13042 |
. . . . . . . 8
⊢
ℝ+ ⊆ ℝ |
| 145 | 143, 144 | ssexi 5322 |
. . . . . . 7
⊢
ℝ+ ∈ V |
| 146 | 145 | a1i 11 |
. . . . . 6
⊢ (⊤
→ ℝ+ ∈ V) |
| 147 | | ovexd 7466 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ V) |
| 148 | 15 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈
ℂ) |
| 149 | | eqidd 2738 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) = (𝑥 ∈ ℝ+ ↦
((ψ‘𝑥) / 𝑥))) |
| 150 | | eqidd 2738 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) |
| 151 | 146, 147,
148, 149, 150 | offval2 7717 |
. . . . 5
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f · (𝑥 ∈ ℝ+
↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
(((ψ‘𝑥) / 𝑥) ·
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))))) |
| 152 | | chpo1ub 27524 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈
𝑂(1) |
| 153 | | 0red 11264 |
. . . . . . . 8
⊢ (⊤
→ 0 ∈ ℝ) |
| 154 | | 1red 11262 |
. . . . . . . 8
⊢ (⊤
→ 1 ∈ ℝ) |
| 155 | | divrcnv 15888 |
. . . . . . . . 9
⊢ (1 ∈
ℂ → (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) |
| 156 | 93, 155 | mp1i 13 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (1 / 𝑥)) ⇝𝑟
0) |
| 157 | | rpreccl 13061 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ+) |
| 158 | 157 | rpred 13077 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (1 / 𝑥) ∈
ℝ) |
| 159 | 158 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1 / 𝑥) ∈ ℝ) |
| 160 | 11, 13 | resubcld 11691 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℝ) |
| 161 | 160 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈
ℝ) |
| 162 | | rpaddcl 13057 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 1 ∈ ℝ+) → (𝑥 + 1) ∈
ℝ+) |
| 163 | 21, 162 | mpan2 691 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 + 1) ∈
ℝ+) |
| 164 | 163 | relogcld 26665 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (log‘(𝑥 + 1))
∈ ℝ) |
| 165 | 164, 13 | resubcld 11691 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((log‘(𝑥 + 1))
− (log‘𝑥))
∈ ℝ) |
| 166 | 7 | nn0red 12588 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
∈ ℝ) |
| 167 | | 1red 11262 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ 1 ∈ ℝ) |
| 168 | | flle 13839 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ≤
𝑥) |
| 169 | 1, 168 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ (⌊‘𝑥)
≤ 𝑥) |
| 170 | 166, 1, 167, 169 | leadd1dd 11877 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ ((⌊‘𝑥) +
1) ≤ (𝑥 +
1)) |
| 171 | 10, 163 | logled 26669 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (((⌊‘𝑥)
+ 1) ≤ (𝑥 + 1) ↔
(log‘((⌊‘𝑥) + 1)) ≤ (log‘(𝑥 + 1)))) |
| 172 | 170, 171 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (log‘((⌊‘𝑥) + 1)) ≤ (log‘(𝑥 + 1))) |
| 173 | 11, 164, 13, 172 | lesub1dd 11879 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ≤ ((log‘(𝑥 + 1)) − (log‘𝑥))) |
| 174 | | logdifbnd 27037 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ ((log‘(𝑥 + 1))
− (log‘𝑥)) ≤
(1 / 𝑥)) |
| 175 | 160, 165,
158, 173, 174 | letrd 11418 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ≤ (1 / 𝑥)) |
| 176 | 175 | ad2antrl 728 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ≤ (1 / 𝑥)) |
| 177 | | fllep1 13841 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
| 178 | 1, 177 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≤
((⌊‘𝑥) +
1)) |
| 179 | | logleb 26645 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ+
∧ ((⌊‘𝑥) +
1) ∈ ℝ+) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (log‘𝑥) ≤ (log‘((⌊‘𝑥) + 1)))) |
| 180 | 10, 179 | mpdan 687 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ≤
((⌊‘𝑥) + 1)
↔ (log‘𝑥) ≤
(log‘((⌊‘𝑥) + 1)))) |
| 181 | 178, 180 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ≤
(log‘((⌊‘𝑥) + 1))) |
| 182 | 11, 13 | subge0d 11853 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (0 ≤ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ↔ (log‘𝑥) ≤ (log‘((⌊‘𝑥) + 1)))) |
| 183 | 181, 182 | mpbird 257 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) |
| 184 | 183 | ad2antrl 728 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤
((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) |
| 185 | 153, 154,
156, 159, 161, 176, 184 | rlimsqz2 15687 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ⇝𝑟
0) |
| 186 | | rlimo1 15653 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ⇝𝑟 0 →
(𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ 𝑂(1)) |
| 187 | 185, 186 | syl 17 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ 𝑂(1)) |
| 188 | | o1mul 15651 |
. . . . . 6
⊢ (((𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∈ 𝑂(1)
∧ (𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥)) ∘f
· (𝑥 ∈
ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) ∈ 𝑂(1)) |
| 189 | 152, 187,
188 | sylancr 587 |
. . . . 5
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f · (𝑥 ∈ ℝ+
↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) ∈ 𝑂(1)) |
| 190 | 151, 189 | eqeltrrd 2842 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) ∈
𝑂(1)) |
| 191 | | nnrp 13046 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ+) |
| 192 | 191 | ssriv 3987 |
. . . . . . . 8
⊢ ℕ
⊆ ℝ+ |
| 193 | 192 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ ℕ ⊆ ℝ+) |
| 194 | 193 | sselda 3983 |
. . . . . 6
⊢
((⊤ ∧ 𝑛
∈ ℕ) → 𝑛
∈ ℝ+) |
| 195 | 194, 31 | syl 17 |
. . . . 5
⊢
((⊤ ∧ 𝑛
∈ ℕ) → (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ) |
| 196 | | chpo1ub 27524 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ+
↦ ((ψ‘𝑛) /
𝑛)) ∈
𝑂(1) |
| 197 | 196 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ (𝑛 ∈
ℝ+ ↦ ((ψ‘𝑛) / 𝑛)) ∈ 𝑂(1)) |
| 198 | | rerpdivcl 13065 |
. . . . . . . . 9
⊢
(((ψ‘𝑛)
∈ ℝ ∧ 𝑛
∈ ℝ+) → ((ψ‘𝑛) / 𝑛) ∈ ℝ) |
| 199 | 29, 198 | mpancom 688 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ+
→ ((ψ‘𝑛) /
𝑛) ∈
ℝ) |
| 200 | 199 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑛
∈ ℝ+) → ((ψ‘𝑛) / 𝑛) ∈ ℝ) |
| 201 | 31 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑛
∈ ℝ+) → (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ) |
| 202 | | rpreccl 13061 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ (1 / 𝑛) ∈
ℝ+) |
| 203 | 202 | rpred 13077 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ (1 / 𝑛) ∈
ℝ) |
| 204 | | chpge0 27169 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ → 0 ≤
(ψ‘𝑛)) |
| 205 | 27, 204 | syl 17 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ (ψ‘𝑛)) |
| 206 | | logdifbnd 27037 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ ((log‘(𝑛 + 1))
− (log‘𝑛)) ≤
(1 / 𝑛)) |
| 207 | 26, 203, 29, 205, 206 | lemul1ad 12207 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛))
≤ ((1 / 𝑛) ·
(ψ‘𝑛))) |
| 208 | 27 | lep1d 12199 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ≤ (𝑛 + 1)) |
| 209 | | logleb 26645 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℝ+
∧ (𝑛 + 1) ∈
ℝ+) → (𝑛 ≤ (𝑛 + 1) ↔ (log‘𝑛) ≤ (log‘(𝑛 + 1)))) |
| 210 | 23, 209 | mpdan 687 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℝ+
→ (𝑛 ≤ (𝑛 + 1) ↔ (log‘𝑛) ≤ (log‘(𝑛 + 1)))) |
| 211 | 208, 210 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (log‘𝑛) ≤
(log‘(𝑛 +
1))) |
| 212 | 24, 25 | subge0d 11853 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (0 ≤ ((log‘(𝑛 + 1)) − (log‘𝑛)) ↔ (log‘𝑛) ≤ (log‘(𝑛 + 1)))) |
| 213 | 211, 212 | mpbird 257 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ ((log‘(𝑛 + 1)) − (log‘𝑛))) |
| 214 | 26, 29, 213, 205 | mulge0d 11840 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) |
| 215 | 30, 214 | absidd 15461 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (abs‘(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) |
| 216 | | rpregt0 13049 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (𝑛 ∈ ℝ
∧ 0 < 𝑛)) |
| 217 | | divge0 12137 |
. . . . . . . . . . . 12
⊢
((((ψ‘𝑛)
∈ ℝ ∧ 0 ≤ (ψ‘𝑛)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → 0 ≤
((ψ‘𝑛) / 𝑛)) |
| 218 | 29, 205, 216, 217 | syl21anc 838 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ ((ψ‘𝑛) / 𝑛)) |
| 219 | 199, 218 | absidd 15461 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ (abs‘((ψ‘𝑛) / 𝑛)) = ((ψ‘𝑛) / 𝑛)) |
| 220 | 29 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ (ψ‘𝑛)
∈ ℂ) |
| 221 | | rpcn 13045 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℂ) |
| 222 | | rpne0 13051 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ≠
0) |
| 223 | 220, 221,
222 | divrec2d 12047 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ ((ψ‘𝑛) /
𝑛) = ((1 / 𝑛) · (ψ‘𝑛))) |
| 224 | 219, 223 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (abs‘((ψ‘𝑛) / 𝑛)) = ((1 / 𝑛) · (ψ‘𝑛))) |
| 225 | 207, 215,
224 | 3brtr4d 5175 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ+
→ (abs‘(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) ≤ (abs‘((ψ‘𝑛) / 𝑛))) |
| 226 | 225 | ad2antrl 728 |
. . . . . . 7
⊢
((⊤ ∧ (𝑛
∈ ℝ+ ∧ 1 ≤ 𝑛)) → (abs‘(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) ≤
(abs‘((ψ‘𝑛)
/ 𝑛))) |
| 227 | 154, 197,
200, 201, 226 | o1le 15689 |
. . . . . 6
⊢ (⊤
→ (𝑛 ∈
ℝ+ ↦ (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) ∈ 𝑂(1)) |
| 228 | 193, 227 | o1res2 15599 |
. . . . 5
⊢ (⊤
→ (𝑛 ∈ ℕ
↦ (((log‘(𝑛 +
1)) − (log‘𝑛))
· (ψ‘𝑛)))
∈ 𝑂(1)) |
| 229 | 195, 228 | o1fsum 15849 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)) ∈ 𝑂(1)) |
| 230 | 141, 142,
190, 229 | o1sub2 15662 |
. . 3
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈
(1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) ∈ 𝑂(1)) |
| 231 | 140, 230 | eqeltrrid 2846 |
. 2
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)) |
| 232 | 231 | mptru 1547 |
1
⊢ (𝑥 ∈ ℝ+
↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) ∈ 𝑂(1) |