Proof of Theorem pntrlog2bndlem5
| Step | Hyp | Ref
| Expression |
| 1 | | elioore 13417 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) |
| 2 | 1 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℝ) |
| 3 | | 1rp 13038 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ |
| 4 | 3 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℝ+) |
| 5 | | 1red 11262 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℝ) |
| 6 | | eliooord 13446 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) |
| 7 | 6 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) |
| 8 | 7 | simpld 494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥) |
| 9 | 5, 2, 8 | ltled 11409 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥) |
| 10 | 2, 4, 9 | rpgecld 13116 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℝ+) |
| 11 | | pntrlog2bnd.r |
. . . . . . . . . . . . 13
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
| 12 | 11 | pntrf 27607 |
. . . . . . . . . . . 12
⊢ 𝑅:ℝ+⟶ℝ |
| 13 | 12 | ffvelcdmi 7103 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) ∈
ℝ) |
| 14 | 10, 13 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℝ) |
| 15 | 14 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℂ) |
| 16 | 15 | abscld 15475 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(𝑅‘𝑥)) ∈
ℝ) |
| 17 | 16 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(𝑅‘𝑥)) ∈
ℂ) |
| 18 | 10 | relogcld 26665 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℝ) |
| 19 | 18 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℂ) |
| 20 | 17, 19 | mulcld 11281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈
ℂ) |
| 21 | | 2cnd 12344 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈
ℂ) |
| 22 | 2, 8 | rplogcld 26671 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℝ+) |
| 23 | 22 | rpne0d 13082 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ≠
0) |
| 24 | 21, 19, 23 | divcld 12043 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 /
(log‘𝑥)) ∈
ℂ) |
| 25 | | fzfid 14014 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(1...(⌊‘𝑥))
∈ Fin) |
| 26 | 10 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ+) |
| 27 | | elfznn 13593 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
| 28 | 27 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
| 29 | 28 | nnrpd 13075 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
| 30 | 26, 29 | rpdivcld 13094 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ+) |
| 31 | 12 | ffvelcdmi 7103 |
. . . . . . . . . . . . 13
⊢ ((𝑥 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
| 33 | 32 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘(𝑥 / 𝑛)) ∈ ℂ) |
| 34 | 33 | abscld 15475 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ) |
| 35 | 29 | relogcld 26665 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℝ) |
| 36 | | 1red 11262 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
| 37 | 35, 36 | readdcld 11290 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘𝑛) + 1)
∈ ℝ) |
| 38 | 34, 37 | remulcld 11291 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) ∈ ℝ) |
| 39 | 38 | recnd 11289 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) ∈ ℂ) |
| 40 | 25, 39 | fsumcl 15769 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) ∈ ℂ) |
| 41 | 24, 40 | mulcld 11281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) ∈ ℂ) |
| 42 | 20, 41 | subcld 11620 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) ∈ ℂ) |
| 43 | 34 | recnd 11289 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℂ) |
| 44 | 25, 43 | fsumcl 15769 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℂ) |
| 45 | 24, 44 | mulcld 11281 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) ∈ ℂ) |
| 46 | 2 | recnd 11289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℂ) |
| 47 | 10 | rpne0d 13082 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0) |
| 48 | 42, 45, 46, 47 | divdird 12081 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))) / 𝑥) = (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥))) |
| 49 | 16, 18 | remulcld 11291 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈
ℝ) |
| 50 | 49 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈
ℂ) |
| 51 | 50, 41, 45 | subsubd 11648 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))))) = ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))))) |
| 52 | 24, 40, 44 | subdid 11719 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 /
(log‘𝑥)) ·
(Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))))) |
| 53 | 25, 39, 43 | fsumsub 15824 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))) |
| 54 | 37 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘𝑛) + 1)
∈ ℂ) |
| 55 | | 1cnd 11256 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℂ) |
| 56 | 43, 54, 55 | subdid 11719 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((log‘𝑛) + 1) − 1)) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · 1))) |
| 57 | 35 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℂ) |
| 58 | 57, 55 | pncand 11621 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((log‘𝑛) + 1)
− 1) = (log‘𝑛)) |
| 59 | 58 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((log‘𝑛) + 1) − 1)) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) |
| 60 | 43 | mulridd 11278 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) · 1) = (abs‘(𝑅‘(𝑥 / 𝑛)))) |
| 61 | 60 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · 1)) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − (abs‘(𝑅‘(𝑥 / 𝑛))))) |
| 62 | 56, 59, 61 | 3eqtr3rd 2786 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) |
| 63 | 62 | sumeq2dv 15738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) |
| 64 | 53, 63 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) |
| 65 | 64 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 /
(log‘𝑥)) ·
(Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) |
| 66 | 52, 65 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) |
| 67 | 66 | oveq2d 7447 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))) |
| 68 | 51, 67 | eqtr3d 2779 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))) |
| 69 | 68 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))) / 𝑥) = ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) |
| 70 | 48, 69 | eqtr3d 2779 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥)) = ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) |
| 71 | 70 | mpteq2dva 5242 |
. 2
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦
(((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥))) = (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥))) |
| 72 | | 2re 12340 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
| 73 | 72 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈
ℝ) |
| 74 | 73, 22 | rerpdivcld 13108 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 /
(log‘𝑥)) ∈
ℝ) |
| 75 | 25, 38 | fsumrecl 15770 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) ∈ ℝ) |
| 76 | 74, 75 | remulcld 11291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) ∈ ℝ) |
| 77 | 49, 76 | resubcld 11691 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) ∈ ℝ) |
| 78 | 77, 10 | rerpdivcld 13108 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) ∈ ℝ) |
| 79 | 25, 34 | fsumrecl 15770 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ) |
| 80 | 74, 79 | remulcld 11291 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) ∈ ℝ) |
| 81 | 80, 10 | rerpdivcld 13108 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℝ) |
| 82 | | 1red 11262 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
| 83 | | pntsval.1 |
. . . . . 6
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) |
| 84 | | pntrlog2bnd.t |
. . . . . 6
⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0)) |
| 85 | 83, 11, 84 | pntrlog2bndlem4 27624 |
. . . . 5
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1) |
| 86 | 85 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1)) |
| 87 | 28 | nnred 12281 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ) |
| 88 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+)
→ 𝑎 ∈
ℝ) |
| 89 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+)
→ 𝑎 ∈
ℝ+) |
| 90 | 89 | relogcld 26665 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+)
→ (log‘𝑎) ∈
ℝ) |
| 91 | 88, 90 | remulcld 11291 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+)
→ (𝑎 ·
(log‘𝑎)) ∈
ℝ) |
| 92 | | 0red 11264 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℝ ∧ ¬
𝑎 ∈
ℝ+) → 0 ∈ ℝ) |
| 93 | 91, 92 | ifclda 4561 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℝ → if(𝑎 ∈ ℝ+,
(𝑎 ·
(log‘𝑎)), 0) ∈
ℝ) |
| 94 | 84, 93 | fmpti 7132 |
. . . . . . . . . . . 12
⊢ 𝑇:ℝ⟶ℝ |
| 95 | 94 | ffvelcdmi 7103 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) ∈ ℝ) |
| 96 | 87, 95 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑇‘𝑛) ∈
ℝ) |
| 97 | 87, 36 | resubcld 11691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 − 1) ∈
ℝ) |
| 98 | 94 | ffvelcdmi 7103 |
. . . . . . . . . . 11
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑇‘(𝑛 − 1)) ∈
ℝ) |
| 99 | 97, 98 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑇‘(𝑛 − 1)) ∈
ℝ) |
| 100 | 96, 99 | resubcld 11691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ∈
ℝ) |
| 101 | 34, 100 | remulcld 11291 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℝ) |
| 102 | 25, 101 | fsumrecl 15770 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℝ) |
| 103 | 74, 102 | remulcld 11291 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ∈
ℝ) |
| 104 | 49, 103 | resubcld 11691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈
ℝ) |
| 105 | 104, 10 | rerpdivcld 13108 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥) ∈ ℝ) |
| 106 | | 2rp 13039 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ+ |
| 107 | 106 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈
ℝ+) |
| 108 | 107 | rpge0d 13081 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤
2) |
| 109 | 73, 22, 108 | divge0d 13117 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (2 /
(log‘𝑥))) |
| 110 | 33 | absge0d 15483 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘(𝑅‘(𝑥 / 𝑛)))) |
| 111 | 29 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
𝑛 ∈
ℝ+) |
| 112 | 111 | rpcnd 13079 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
𝑛 ∈
ℂ) |
| 113 | 57 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(log‘𝑛) ∈
ℂ) |
| 114 | 112, 113 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(𝑛 ·
(log‘𝑛)) ∈
ℂ) |
| 115 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) → 1
< 𝑛) |
| 116 | | 1re 11261 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ |
| 117 | 111 | rpred 13077 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
𝑛 ∈
ℝ) |
| 118 | | difrp 13073 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℝ ∧ 𝑛
∈ ℝ) → (1 < 𝑛 ↔ (𝑛 − 1) ∈
ℝ+)) |
| 119 | 116, 117,
118 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) → (1
< 𝑛 ↔ (𝑛 − 1) ∈
ℝ+)) |
| 120 | 115, 119 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(𝑛 − 1) ∈
ℝ+) |
| 121 | 120 | relogcld 26665 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(log‘(𝑛 − 1))
∈ ℝ) |
| 122 | 121 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(log‘(𝑛 − 1))
∈ ℂ) |
| 123 | 112, 122 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(𝑛 ·
(log‘(𝑛 − 1)))
∈ ℂ) |
| 124 | 114, 123,
122 | subsubd 11648 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑛 ·
(log‘𝑛)) −
((𝑛 ·
(log‘(𝑛 − 1)))
− (log‘(𝑛
− 1)))) = (((𝑛
· (log‘𝑛))
− (𝑛 ·
(log‘(𝑛 − 1))))
+ (log‘(𝑛 −
1)))) |
| 125 | | rpre 13043 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℝ) |
| 126 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑛 → (𝑎 ∈ ℝ+ ↔ 𝑛 ∈
ℝ+)) |
| 127 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑛 → 𝑎 = 𝑛) |
| 128 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑛 → (log‘𝑎) = (log‘𝑛)) |
| 129 | 127, 128 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑛 → (𝑎 · (log‘𝑎)) = (𝑛 · (log‘𝑛))) |
| 130 | 126, 129 | ifbieq1d 4550 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑛 → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0)) |
| 131 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 · (log‘𝑛)) ∈ V |
| 132 | | c0ex 11255 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
V |
| 133 | 131, 132 | ifex 4576 |
. . . . . . . . . . . . . . . . . 18
⊢ if(𝑛 ∈ ℝ+,
(𝑛 ·
(log‘𝑛)), 0) ∈
V |
| 134 | 130, 84, 133 | fvmpt 7016 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0)) |
| 135 | 125, 134 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℝ+
→ (𝑇‘𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0)) |
| 136 | | iftrue 4531 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℝ+
→ if(𝑛 ∈
ℝ+, (𝑛
· (log‘𝑛)), 0)
= (𝑛 ·
(log‘𝑛))) |
| 137 | 135, 136 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℝ+
→ (𝑇‘𝑛) = (𝑛 · (log‘𝑛))) |
| 138 | 111, 137 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(𝑇‘𝑛) = (𝑛 · (log‘𝑛))) |
| 139 | | rpre 13043 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 − 1) ∈
ℝ+ → (𝑛 − 1) ∈ ℝ) |
| 140 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = (𝑛 − 1) → (𝑎 ∈ ℝ+ ↔ (𝑛 − 1) ∈
ℝ+)) |
| 141 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (𝑛 − 1) → 𝑎 = (𝑛 − 1)) |
| 142 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (𝑛 − 1) → (log‘𝑎) = (log‘(𝑛 − 1))) |
| 143 | 141, 142 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = (𝑛 − 1) → (𝑎 · (log‘𝑎)) = ((𝑛 − 1) · (log‘(𝑛 − 1)))) |
| 144 | 140, 143 | ifbieq1d 4550 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = (𝑛 − 1) → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if((𝑛 − 1) ∈ ℝ+,
((𝑛 − 1) ·
(log‘(𝑛 − 1))),
0)) |
| 145 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 − 1) ·
(log‘(𝑛 − 1)))
∈ V |
| 146 | 145, 132 | ifex 4576 |
. . . . . . . . . . . . . . . . . . 19
⊢ if((𝑛 − 1) ∈
ℝ+, ((𝑛
− 1) · (log‘(𝑛 − 1))), 0) ∈ V |
| 147 | 144, 84, 146 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑇‘(𝑛 − 1)) = if((𝑛 − 1) ∈
ℝ+, ((𝑛
− 1) · (log‘(𝑛 − 1))), 0)) |
| 148 | 139, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 − 1) ∈
ℝ+ → (𝑇‘(𝑛 − 1)) = if((𝑛 − 1) ∈ ℝ+,
((𝑛 − 1) ·
(log‘(𝑛 − 1))),
0)) |
| 149 | | iftrue 4531 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 − 1) ∈
ℝ+ → if((𝑛 − 1) ∈ ℝ+,
((𝑛 − 1) ·
(log‘(𝑛 − 1))),
0) = ((𝑛 − 1)
· (log‘(𝑛
− 1)))) |
| 150 | 148, 149 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 − 1) ∈
ℝ+ → (𝑇‘(𝑛 − 1)) = ((𝑛 − 1) · (log‘(𝑛 − 1)))) |
| 151 | 120, 150 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(𝑇‘(𝑛 − 1)) = ((𝑛 − 1) ·
(log‘(𝑛 −
1)))) |
| 152 | | 1cnd 11256 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) → 1
∈ ℂ) |
| 153 | 112, 152,
122 | subdird 11720 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑛 − 1) ·
(log‘(𝑛 − 1)))
= ((𝑛 ·
(log‘(𝑛 − 1)))
− (1 · (log‘(𝑛 − 1))))) |
| 154 | 122 | mullidd 11279 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) → (1
· (log‘(𝑛
− 1))) = (log‘(𝑛 − 1))) |
| 155 | 154 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑛 ·
(log‘(𝑛 − 1)))
− (1 · (log‘(𝑛 − 1)))) = ((𝑛 · (log‘(𝑛 − 1))) − (log‘(𝑛 − 1)))) |
| 156 | 151, 153,
155 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(𝑇‘(𝑛 − 1)) = ((𝑛 · (log‘(𝑛 − 1))) −
(log‘(𝑛 −
1)))) |
| 157 | 138, 156 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) = ((𝑛 · (log‘𝑛)) − ((𝑛 · (log‘(𝑛 − 1))) − (log‘(𝑛 − 1))))) |
| 158 | 112, 113,
122 | subdid 11719 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(𝑛 ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
= ((𝑛 ·
(log‘𝑛)) −
(𝑛 ·
(log‘(𝑛 −
1))))) |
| 159 | 158 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑛 ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
+ (log‘(𝑛 −
1))) = (((𝑛 ·
(log‘𝑛)) −
(𝑛 ·
(log‘(𝑛 − 1))))
+ (log‘(𝑛 −
1)))) |
| 160 | 124, 157,
159 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) = ((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) + (log‘(𝑛 − 1)))) |
| 161 | 111 | relogcld 26665 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(log‘𝑛) ∈
ℝ) |
| 162 | 161, 121 | resubcld 11691 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((log‘𝑛) −
(log‘(𝑛 − 1)))
∈ ℝ) |
| 163 | 162 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((log‘𝑛) −
(log‘(𝑛 − 1)))
∈ ℂ) |
| 164 | 112, 152,
163 | subdird 11720 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑛 − 1) ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
= ((𝑛 ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
− (1 · ((log‘𝑛) − (log‘(𝑛 − 1)))))) |
| 165 | 163 | mullidd 11279 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) → (1
· ((log‘𝑛)
− (log‘(𝑛
− 1)))) = ((log‘𝑛) − (log‘(𝑛 − 1)))) |
| 166 | 165 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑛 ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
− (1 · ((log‘𝑛) − (log‘(𝑛 − 1))))) = ((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) − ((log‘𝑛) − (log‘(𝑛 − 1))))) |
| 167 | 117, 162 | remulcld 11291 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(𝑛 ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
∈ ℝ) |
| 168 | 167 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(𝑛 ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
∈ ℂ) |
| 169 | 168, 113,
122 | subsub3d 11650 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑛 ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
− ((log‘𝑛)
− (log‘(𝑛
− 1)))) = (((𝑛
· ((log‘𝑛)
− (log‘(𝑛
− 1)))) + (log‘(𝑛 − 1))) − (log‘𝑛))) |
| 170 | 164, 166,
169 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑛 − 1) ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
= (((𝑛 ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
+ (log‘(𝑛 −
1))) − (log‘𝑛))) |
| 171 | 112, 152 | npcand 11624 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑛 − 1) + 1) = 𝑛) |
| 172 | 171 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(log‘((𝑛 − 1) +
1)) = (log‘𝑛)) |
| 173 | 172 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((log‘((𝑛 − 1)
+ 1)) − (log‘(𝑛
− 1))) = ((log‘𝑛) − (log‘(𝑛 − 1)))) |
| 174 | | logdifbnd 27037 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 − 1) ∈
ℝ+ → ((log‘((𝑛 − 1) + 1)) − (log‘(𝑛 − 1))) ≤ (1 / (𝑛 − 1))) |
| 175 | 120, 174 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((log‘((𝑛 − 1)
+ 1)) − (log‘(𝑛
− 1))) ≤ (1 / (𝑛
− 1))) |
| 176 | 173, 175 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((log‘𝑛) −
(log‘(𝑛 − 1)))
≤ (1 / (𝑛 −
1))) |
| 177 | | 1red 11262 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) → 1
∈ ℝ) |
| 178 | 162, 177,
120 | lemuldiv2d 13127 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(((𝑛 − 1) ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
≤ 1 ↔ ((log‘𝑛) − (log‘(𝑛 − 1))) ≤ (1 / (𝑛 − 1)))) |
| 179 | 176, 178 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑛 − 1) ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
≤ 1) |
| 180 | 170, 179 | eqbrtrrd 5167 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
(((𝑛 ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
+ (log‘(𝑛 −
1))) − (log‘𝑛))
≤ 1) |
| 181 | 167, 121 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑛 ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
+ (log‘(𝑛 −
1))) ∈ ℝ) |
| 182 | 181, 161,
177 | lesubadd2d 11862 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((((𝑛 ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
+ (log‘(𝑛 −
1))) − (log‘𝑛))
≤ 1 ↔ ((𝑛 ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
+ (log‘(𝑛 −
1))) ≤ ((log‘𝑛) +
1))) |
| 183 | 180, 182 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑛 ·
((log‘𝑛) −
(log‘(𝑛 − 1))))
+ (log‘(𝑛 −
1))) ≤ ((log‘𝑛) +
1)) |
| 184 | 160, 183 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 < 𝑛) →
((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ≤ ((log‘𝑛) + 1)) |
| 185 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → (𝑇‘𝑛) = (𝑇‘1)) |
| 186 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 1 → 𝑎 = 1) |
| 187 | 186, 3 | eqeltrdi 2849 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 1 → 𝑎 ∈ ℝ+) |
| 188 | 187 | iftrued 4533 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 1 → if(𝑎 ∈ ℝ+,
(𝑎 ·
(log‘𝑎)), 0) = (𝑎 · (log‘𝑎))) |
| 189 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = 1 → (log‘𝑎) =
(log‘1)) |
| 190 | | log1 26627 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(log‘1) = 0 |
| 191 | 189, 190 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 1 → (log‘𝑎) = 0) |
| 192 | 186, 191 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 1 → (𝑎 · (log‘𝑎)) = (1 · 0)) |
| 193 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℂ |
| 194 | 193 | mul01i 11451 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1
· 0) = 0 |
| 195 | 192, 194 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 1 → (𝑎 · (log‘𝑎)) = 0) |
| 196 | 188, 195 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 1 → if(𝑎 ∈ ℝ+,
(𝑎 ·
(log‘𝑎)), 0) =
0) |
| 197 | 196, 84, 132 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℝ → (𝑇‘1)
= 0) |
| 198 | 116, 197 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇‘1) = 0 |
| 199 | 185, 198 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 1 → (𝑇‘𝑛) = 0) |
| 200 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 1 → (𝑛 − 1) = (1 − 1)) |
| 201 | | 1m1e0 12338 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1
− 1) = 0 |
| 202 | 200, 201 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 1 → (𝑛 − 1) = 0) |
| 203 | 202 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 1 → (𝑇‘(𝑛 − 1)) = (𝑇‘0)) |
| 204 | | 0re 11263 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
| 205 | | rpne0 13051 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℝ+
→ 𝑎 ≠
0) |
| 206 | 205 | necon2bi 2971 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 0 → ¬ 𝑎 ∈
ℝ+) |
| 207 | 206 | iffalsed 4536 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 0 → if(𝑎 ∈ ℝ+,
(𝑎 ·
(log‘𝑎)), 0) =
0) |
| 208 | 207, 84, 132 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ℝ → (𝑇‘0)
= 0) |
| 209 | 204, 208 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇‘0) = 0 |
| 210 | 203, 209 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 1 → (𝑇‘(𝑛 − 1)) = 0) |
| 211 | 199, 210 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 1 → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) = (0 −
0)) |
| 212 | | 0m0e0 12386 |
. . . . . . . . . . . . . . 15
⊢ (0
− 0) = 0 |
| 213 | 211, 212 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 1 → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) = 0) |
| 214 | 213 | eqcoms 2745 |
. . . . . . . . . . . . 13
⊢ (1 =
𝑛 → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) = 0) |
| 215 | 214 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 = 𝑛) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) = 0) |
| 216 | | 0red 11264 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ∈ ℝ) |
| 217 | 28 | nnge1d 12314 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ 𝑛) |
| 218 | 87, 217 | logge0d 26672 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (log‘𝑛)) |
| 219 | 35 | lep1d 12199 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ≤
((log‘𝑛) +
1)) |
| 220 | 216, 35, 37, 218, 219 | letrd 11418 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((log‘𝑛) + 1)) |
| 221 | 220 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 = 𝑛) → 0 ≤
((log‘𝑛) +
1)) |
| 222 | 215, 221 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 1 = 𝑛) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ≤ ((log‘𝑛) + 1)) |
| 223 | | elfzle1 13567 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 1 ≤ 𝑛) |
| 224 | 223 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ 𝑛) |
| 225 | 36, 87 | leloed 11404 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 ≤ 𝑛 ↔ (1
< 𝑛 ∨ 1 = 𝑛))) |
| 226 | 224, 225 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 < 𝑛 ∨ 1 =
𝑛)) |
| 227 | 184, 222,
226 | mpjaodan 961 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ≤ ((log‘𝑛) + 1)) |
| 228 | 100, 37, 34, 110, 227 | lemul2ad 12208 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ≤ ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) |
| 229 | 25, 101, 38, 228 | fsumle 15835 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) |
| 230 | 102, 75, 74, 109, 229 | lemul2ad 12208 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ≤ ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) |
| 231 | 103, 76, 49, 230 | lesub2dd 11880 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) ≤ (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) |
| 232 | 77, 104, 10, 231 | lediv1dd 13135 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) ≤ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) |
| 233 | 232 | adantrr 717 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) ≤ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) |
| 234 | 82, 86, 105, 78, 233 | lo1le 15688 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥)) ∈ ≤𝑂(1)) |
| 235 | 106 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℝ+) |
| 236 | | pntrlog2bndlem5.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
| 237 | 235, 236 | rpmulcld 13093 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝐵) ∈
ℝ+) |
| 238 | 237 | rpred 13077 |
. . . . . 6
⊢ (𝜑 → (2 · 𝐵) ∈
ℝ) |
| 239 | 238 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 ·
𝐵) ∈
ℝ) |
| 240 | 5, 22 | rerpdivcld 13108 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1 /
(log‘𝑥)) ∈
ℝ) |
| 241 | 5, 240 | readdcld 11290 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1 + (1 /
(log‘𝑥))) ∈
ℝ) |
| 242 | | ioossre 13448 |
. . . . . 6
⊢
(1(,)+∞) ⊆ ℝ |
| 243 | | lo1const 15657 |
. . . . . 6
⊢
(((1(,)+∞) ⊆ ℝ ∧ (2 · 𝐵) ∈ ℝ) → (𝑥 ∈ (1(,)+∞) ↦ (2 ·
𝐵)) ∈
≤𝑂(1)) |
| 244 | 242, 238,
243 | sylancr 587 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (2 ·
𝐵)) ∈
≤𝑂(1)) |
| 245 | | lo1const 15657 |
. . . . . . 7
⊢
(((1(,)+∞) ⊆ ℝ ∧ 1 ∈ ℝ) → (𝑥 ∈ (1(,)+∞) ↦
1) ∈ ≤𝑂(1)) |
| 246 | 242, 82, 245 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 1) ∈
≤𝑂(1)) |
| 247 | | divlogrlim 26677 |
. . . . . . . 8
⊢ (𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 |
| 248 | | rlimo1 15653 |
. . . . . . . 8
⊢ ((𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 /
(log‘𝑥))) ∈
𝑂(1)) |
| 249 | 247, 248 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (1 /
(log‘𝑥))) ∈
𝑂(1)) |
| 250 | 240, 249 | o1lo1d 15575 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (1 /
(log‘𝑥))) ∈
≤𝑂(1)) |
| 251 | 5, 240, 246, 250 | lo1add 15663 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (1 + (1 /
(log‘𝑥)))) ∈
≤𝑂(1)) |
| 252 | 237 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 ·
𝐵) ∈
ℝ+) |
| 253 | 252 | rpge0d 13081 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (2
· 𝐵)) |
| 254 | 239, 241,
244, 251, 253 | lo1mul 15664 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((2 ·
𝐵) · (1 + (1 /
(log‘𝑥))))) ∈
≤𝑂(1)) |
| 255 | 239, 241 | remulcld 11291 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 ·
𝐵) · (1 + (1 /
(log‘𝑥)))) ∈
ℝ) |
| 256 | 79, 10 | rerpdivcld 13108 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ∈ ℝ) |
| 257 | 18, 5 | readdcld 11290 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((log‘𝑥) + 1) ∈
ℝ) |
| 258 | 236 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐵 ∈
ℝ+) |
| 259 | 258 | rpred 13077 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐵 ∈
ℝ) |
| 260 | 257, 259 | remulcld 11291 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((log‘𝑥) + 1)
· 𝐵) ∈
ℝ) |
| 261 | 28 | nnrecred 12317 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑛) ∈
ℝ) |
| 262 | 25, 261 | fsumrecl 15770 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) ∈
ℝ) |
| 263 | 262, 259 | remulcld 11291 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) · 𝐵) ∈
ℝ) |
| 264 | 34, 26 | rerpdivcld 13108 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ∈ ℝ) |
| 265 | 259 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐵 ∈
ℝ) |
| 266 | 261, 265 | remulcld 11291 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 / 𝑛) ·
𝐵) ∈
ℝ) |
| 267 | 30 | rpcnd 13079 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℂ) |
| 268 | 30 | rpne0d 13082 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ≠ 0) |
| 269 | 33, 267, 268 | absdivd 15494 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) / (abs‘(𝑥 / 𝑛)))) |
| 270 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ) |
| 271 | 270, 28 | nndivred 12320 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ) |
| 272 | 30 | rpge0d 13081 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (𝑥 / 𝑛)) |
| 273 | 271, 272 | absidd 15461 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑥 /
𝑛)) = (𝑥 / 𝑛)) |
| 274 | 273 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) / (abs‘(𝑥 / 𝑛))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) / (𝑥 / 𝑛))) |
| 275 | 269, 274 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) / (𝑥 / 𝑛))) |
| 276 | 46 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℂ) |
| 277 | 87 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℂ) |
| 278 | 47 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ≠
0) |
| 279 | 28 | nnne0d 12316 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ≠
0) |
| 280 | 43, 276, 277, 278, 279 | divdiv2d 12075 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) / (𝑥 / 𝑛)) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · 𝑛) / 𝑥)) |
| 281 | 43, 277, 276, 278 | div23d 12080 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((abs‘(𝑅‘(𝑥 / 𝑛))) · 𝑛) / 𝑥) = (((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) · 𝑛)) |
| 282 | 275, 280,
281 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) = (((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) · 𝑛)) |
| 283 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑥 / 𝑛) → (𝑅‘𝑦) = (𝑅‘(𝑥 / 𝑛))) |
| 284 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑥 / 𝑛) → 𝑦 = (𝑥 / 𝑛)) |
| 285 | 283, 284 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑥 / 𝑛) → ((𝑅‘𝑦) / 𝑦) = ((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) |
| 286 | 285 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 / 𝑛) → (abs‘((𝑅‘𝑦) / 𝑦)) = (abs‘((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)))) |
| 287 | 286 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 / 𝑛) → ((abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐵 ↔ (abs‘((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) ≤ 𝐵)) |
| 288 | | pntrlog2bndlem5.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑦 ∈ ℝ+
(abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐵) |
| 289 | 288 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ∀𝑦 ∈
ℝ+ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐵) |
| 290 | 287, 289,
30 | rspcdva 3623 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) ≤ 𝐵) |
| 291 | 282, 290 | eqbrtrrd 5167 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) · 𝑛) ≤ 𝐵) |
| 292 | 264, 265,
29 | lemuldivd 13126 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) · 𝑛) ≤ 𝐵 ↔ ((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ≤ (𝐵 / 𝑛))) |
| 293 | 291, 292 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ≤ (𝐵 / 𝑛)) |
| 294 | 265 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐵 ∈
ℂ) |
| 295 | 294, 277,
279 | divrec2d 12047 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐵 / 𝑛) = ((1 / 𝑛) · 𝐵)) |
| 296 | 293, 295 | breqtrd 5169 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ≤ ((1 / 𝑛) · 𝐵)) |
| 297 | 25, 264, 266, 296 | fsumle 15835 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 / 𝑛) · 𝐵)) |
| 298 | 25, 46, 43, 47 | fsumdivc 15822 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥)) |
| 299 | 258 | rpcnd 13079 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐵 ∈
ℂ) |
| 300 | 261 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑛) ∈
ℂ) |
| 301 | 25, 299, 300 | fsummulc1 15821 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) · 𝐵) = Σ𝑛 ∈ (1...(⌊‘𝑥))((1 / 𝑛) · 𝐵)) |
| 302 | 297, 298,
301 | 3brtr4d 5175 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) · 𝐵)) |
| 303 | 258 | rpge0d 13081 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ 𝐵) |
| 304 | | harmonicubnd 27053 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) → Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) ≤ ((log‘𝑥) + 1)) |
| 305 | 2, 9, 304 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) ≤ ((log‘𝑥) + 1)) |
| 306 | 262, 257,
259, 303, 305 | lemul1ad 12207 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(1 /
𝑛) · 𝐵) ≤ (((log‘𝑥) + 1) · 𝐵)) |
| 307 | 256, 263,
260, 302, 306 | letrd 11418 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ≤ (((log‘𝑥) + 1) · 𝐵)) |
| 308 | 256, 260,
74, 109, 307 | lemul2ad 12208 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 /
(log‘𝑥)) ·
(Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥)) ≤ ((2 / (log‘𝑥)) · (((log‘𝑥) + 1) · 𝐵))) |
| 309 | 24, 44, 46, 47 | divassd 12078 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥) = ((2 / (log‘𝑥)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥))) |
| 310 | 241 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1 + (1 /
(log‘𝑥))) ∈
ℂ) |
| 311 | 21, 299, 310 | mul32d 11471 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 ·
𝐵) · (1 + (1 /
(log‘𝑥)))) = ((2
· (1 + (1 / (log‘𝑥)))) · 𝐵)) |
| 312 | | 1cnd 11256 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℂ) |
| 313 | 19, 312, 19, 23 | divdird 12081 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((log‘𝑥) + 1) /
(log‘𝑥)) =
(((log‘𝑥) /
(log‘𝑥)) + (1 /
(log‘𝑥)))) |
| 314 | 19, 23 | dividd 12041 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((log‘𝑥) /
(log‘𝑥)) =
1) |
| 315 | 314 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((log‘𝑥) /
(log‘𝑥)) + (1 /
(log‘𝑥))) = (1 + (1 /
(log‘𝑥)))) |
| 316 | 313, 315 | eqtr2d 2778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1 + (1 /
(log‘𝑥))) =
(((log‘𝑥) + 1) /
(log‘𝑥))) |
| 317 | 316 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (1
+ (1 / (log‘𝑥)))) =
(2 · (((log‘𝑥)
+ 1) / (log‘𝑥)))) |
| 318 | 19, 312 | addcld 11280 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((log‘𝑥) + 1) ∈
ℂ) |
| 319 | 21, 19, 318, 23 | div32d 12066 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 /
(log‘𝑥)) ·
((log‘𝑥) + 1)) = (2
· (((log‘𝑥) +
1) / (log‘𝑥)))) |
| 320 | 317, 319 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (1
+ (1 / (log‘𝑥)))) =
((2 / (log‘𝑥))
· ((log‘𝑥) +
1))) |
| 321 | 320 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 ·
(1 + (1 / (log‘𝑥))))
· 𝐵) = (((2 /
(log‘𝑥)) ·
((log‘𝑥) + 1))
· 𝐵)) |
| 322 | 24, 318, 299 | mulassd 11284 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 /
(log‘𝑥)) ·
((log‘𝑥) + 1))
· 𝐵) = ((2 /
(log‘𝑥)) ·
(((log‘𝑥) + 1)
· 𝐵))) |
| 323 | 311, 321,
322 | 3eqtrd 2781 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 ·
𝐵) · (1 + (1 /
(log‘𝑥)))) = ((2 /
(log‘𝑥)) ·
(((log‘𝑥) + 1)
· 𝐵))) |
| 324 | 308, 309,
323 | 3brtr4d 5175 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥) ≤ ((2 · 𝐵) · (1 + (1 / (log‘𝑥))))) |
| 325 | 324 | adantrr 717 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥) ≤ ((2 · 𝐵) · (1 + (1 / (log‘𝑥))))) |
| 326 | 82, 254, 255, 81, 325 | lo1le 15688 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥)) ∈ ≤𝑂(1)) |
| 327 | 78, 81, 234, 326 | lo1add 15663 |
. 2
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦
(((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥))) ∈ ≤𝑂(1)) |
| 328 | 71, 327 | eqeltrrd 2842 |
1
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ ≤𝑂(1)) |