| Step | Hyp | Ref
| Expression |
| 1 | | 1red 11262 |
. 2
⊢ (𝜑 → 1 ∈
ℝ) |
| 2 | | pntrlog2bndlem3.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
| 3 | 2 | rpred 13077 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 4 | 3 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈
ℝ) |
| 5 | | fzfid 14014 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(1...(⌊‘𝑥))
∈ Fin) |
| 6 | | elfznn 13593 |
. . . . . . . 8
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
| 7 | 6 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
| 8 | 7 | nnred 12281 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ) |
| 9 | | elioore 13417 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) |
| 10 | 9 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℝ) |
| 11 | | 1rp 13038 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ+ |
| 12 | 11 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℝ+) |
| 13 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℝ) |
| 14 | | eliooord 13446 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) |
| 15 | 14 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) |
| 16 | 15 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥) |
| 17 | 13, 10, 16 | ltled 11409 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥) |
| 18 | 10, 12, 17 | rpgecld 13116 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℝ+) |
| 19 | 18 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ+) |
| 20 | 7 | nnrpd 13075 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
| 21 | 11 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ+) |
| 22 | 20, 21 | rpaddcld 13092 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 + 1) ∈
ℝ+) |
| 23 | 19, 22 | rpdivcld 13094 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / (𝑛 + 1)) ∈
ℝ+) |
| 24 | | pntrlog2bnd.r |
. . . . . . . . . . . 12
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
| 25 | 24 | pntrf 27607 |
. . . . . . . . . . 11
⊢ 𝑅:ℝ+⟶ℝ |
| 26 | 25 | ffvelcdmi 7103 |
. . . . . . . . . 10
⊢ ((𝑥 / (𝑛 + 1)) ∈ ℝ+ →
(𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ) |
| 27 | 23, 26 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ) |
| 28 | 27 | recnd 11289 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℂ) |
| 29 | 19, 20 | rpdivcld 13094 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ+) |
| 30 | 25 | ffvelcdmi 7103 |
. . . . . . . . . 10
⊢ ((𝑥 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
| 32 | 31 | recnd 11289 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑅‘(𝑥 / 𝑛)) ∈ ℂ) |
| 33 | 28, 32 | subcld 11620 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))) ∈ ℂ) |
| 34 | 33 | abscld 15475 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛)))) ∈ ℝ) |
| 35 | 8, 34 | remulcld 11291 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ·
(abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) ∈ ℝ) |
| 36 | 5, 35 | fsumrecl 15770 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) ∈ ℝ) |
| 37 | 10, 16 | rplogcld 26671 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℝ+) |
| 38 | 18, 37 | rpmulcld 13093 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈
ℝ+) |
| 39 | 36, 38 | rerpdivcld 13108 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
| 40 | | ioossre 13448 |
. . . 4
⊢
(1(,)+∞) ⊆ ℝ |
| 41 | 2 | rpcnd 13079 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 42 | | o1const 15656 |
. . . 4
⊢
(((1(,)+∞) ⊆ ℝ ∧ 𝐴 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈
𝑂(1)) |
| 43 | 40, 41, 42 | sylancr 587 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈
𝑂(1)) |
| 44 | | chpo1ubb 27525 |
. . . 4
⊢
∃𝑐 ∈
ℝ+ ∀𝑦 ∈ ℝ+
(ψ‘𝑦) ≤ (𝑐 · 𝑦) |
| 45 | | pntsval.1 |
. . . . . 6
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) |
| 46 | | simpl 482 |
. . . . . 6
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
ℝ+ (ψ‘𝑦) ≤ (𝑐 · 𝑦)) → 𝑐 ∈ ℝ+) |
| 47 | | simpr 484 |
. . . . . 6
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
ℝ+ (ψ‘𝑦) ≤ (𝑐 · 𝑦)) → ∀𝑦 ∈ ℝ+
(ψ‘𝑦) ≤ (𝑐 · 𝑦)) |
| 48 | 45, 24, 46, 47 | pntrlog2bndlem2 27622 |
. . . . 5
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
ℝ+ (ψ‘𝑦) ≤ (𝑐 · 𝑦)) → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
| 49 | 48 | rexlimiva 3147 |
. . . 4
⊢
(∃𝑐 ∈
ℝ+ ∀𝑦 ∈ ℝ+
(ψ‘𝑦) ≤ (𝑐 · 𝑦) → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
| 50 | 44, 49 | mp1i 13 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
| 51 | 4, 39, 43, 50 | o1mul2 15661 |
. 2
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (𝐴 · (Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥))))) ∈ 𝑂(1)) |
| 52 | 4, 39 | remulcld 11291 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · (Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ ℝ) |
| 53 | 32 | abscld 15475 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ) |
| 54 | 28 | abscld 15475 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℝ) |
| 55 | 53, 54 | resubcld 11691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℝ) |
| 56 | 45 | pntsf 27617 |
. . . . . . . . 9
⊢ 𝑆:ℝ⟶ℝ |
| 57 | 56 | ffvelcdmi 7103 |
. . . . . . . 8
⊢ (𝑛 ∈ ℝ → (𝑆‘𝑛) ∈ ℝ) |
| 58 | 8, 57 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑆‘𝑛) ∈
ℝ) |
| 59 | | 2re 12340 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
| 60 | 59 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 2 ∈ ℝ) |
| 61 | 20 | relogcld 26665 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℝ) |
| 62 | 8, 61 | remulcld 11291 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ·
(log‘𝑛)) ∈
ℝ) |
| 63 | 60, 62 | remulcld 11291 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (𝑛
· (log‘𝑛)))
∈ ℝ) |
| 64 | 58, 63 | resubcld 11691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈
ℝ) |
| 65 | 55, 64 | remulcld 11291 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ) |
| 66 | 5, 65 | fsumrecl 15770 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ) |
| 67 | 66, 38 | rerpdivcld 13108 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
| 68 | 67 | recnd 11289 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))) ∈ ℂ) |
| 69 | 68 | abscld 15475 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ ℝ) |
| 70 | 52 | recnd 11289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · (Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ ℂ) |
| 71 | 70 | abscld 15475 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(𝐴 ·
(Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥))))) ∈ ℝ) |
| 72 | 66 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ) |
| 73 | 72 | abscld 15475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ∈ ℝ) |
| 74 | 4, 36 | remulcld 11291 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛)))))) ∈ ℝ) |
| 75 | 65 | recnd 11289 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ) |
| 76 | 75 | abscld 15475 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ∈ ℝ) |
| 77 | 5, 76 | fsumrecl 15770 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ∈ ℝ) |
| 78 | 5, 75 | fsumabs 15837 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))) |
| 79 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐴 ∈
ℝ) |
| 80 | 79, 35 | remulcld 11291 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐴 · (𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛)))))) ∈ ℝ) |
| 81 | 55 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℂ) |
| 82 | 81 | abscld 15475 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))))) ∈ ℝ) |
| 83 | 64 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈
ℂ) |
| 84 | 83 | abscld 15475 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ) |
| 85 | 79, 8 | remulcld 11291 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐴 · 𝑛) ∈
ℝ) |
| 86 | 81 | absge0d 15483 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))))) |
| 87 | 83 | absge0d 15483 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
| 88 | 32, 28 | abs2difabsd 15498 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))))) ≤ (abs‘((𝑅‘(𝑥 / 𝑛)) − (𝑅‘(𝑥 / (𝑛 + 1)))))) |
| 89 | 32, 28 | abssubd 15492 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑅‘(𝑥 / 𝑛)) − (𝑅‘(𝑥 / (𝑛 + 1))))) = (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) |
| 90 | 88, 89 | breqtrd 5169 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))))) ≤ (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) |
| 91 | 58 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑆‘𝑛) ∈
ℂ) |
| 92 | 8 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℂ) |
| 93 | 7 | nnne0d 12316 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ≠
0) |
| 94 | 91, 92, 93 | divcld 12043 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑆‘𝑛) / 𝑛) ∈ ℂ) |
| 95 | | 2cnd 12344 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 2 ∈ ℂ) |
| 96 | 61 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℂ) |
| 97 | 95, 96 | mulcld 11281 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · (log‘𝑛)) ∈ ℂ) |
| 98 | 94, 97 | subcld 11620 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛))) ∈
ℂ) |
| 99 | 98, 92 | absmuld 15493 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛))) · 𝑛)) = ((abs‘(((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛)))) · (abs‘𝑛))) |
| 100 | 94, 97, 92 | subdird 11720 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛))) · 𝑛) = ((((𝑆‘𝑛) / 𝑛) · 𝑛) − ((2 · (log‘𝑛)) · 𝑛))) |
| 101 | 91, 92, 93 | divcan1d 12044 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((𝑆‘𝑛) / 𝑛) · 𝑛) = (𝑆‘𝑛)) |
| 102 | 95, 92, 96 | mul32d 11471 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝑛)
· (log‘𝑛)) =
((2 · (log‘𝑛))
· 𝑛)) |
| 103 | 95, 92, 96 | mulassd 11284 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝑛)
· (log‘𝑛)) =
(2 · (𝑛 ·
(log‘𝑛)))) |
| 104 | 102, 103 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((2 · (log‘𝑛)) · 𝑛) = (2 · (𝑛 · (log‘𝑛)))) |
| 105 | 101, 104 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((𝑆‘𝑛) / 𝑛) · 𝑛) − ((2 · (log‘𝑛)) · 𝑛)) = ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) |
| 106 | 100, 105 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛))) · 𝑛) = ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) |
| 107 | 106 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛))) · 𝑛)) = (abs‘((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
| 108 | 20 | rpge0d 13081 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ 𝑛) |
| 109 | 8, 108 | absidd 15461 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘𝑛) =
𝑛) |
| 110 | 109 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛)))) · (abs‘𝑛)) = ((abs‘(((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛)))) · 𝑛)) |
| 111 | 99, 107, 110 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) = ((abs‘(((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛)))) · 𝑛)) |
| 112 | 98 | abscld 15475 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛)))) ∈
ℝ) |
| 113 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑛 → (𝑆‘𝑦) = (𝑆‘𝑛)) |
| 114 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑛 → 𝑦 = 𝑛) |
| 115 | 113, 114 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑛 → ((𝑆‘𝑦) / 𝑦) = ((𝑆‘𝑛) / 𝑛)) |
| 116 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑛 → (log‘𝑦) = (log‘𝑛)) |
| 117 | 116 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑛 → (2 · (log‘𝑦)) = (2 ·
(log‘𝑛))) |
| 118 | 115, 117 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑛 → (((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦))) = (((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛)))) |
| 119 | 118 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑛 → (abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) = (abs‘(((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛))))) |
| 120 | 119 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑛 → ((abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴 ↔ (abs‘(((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛)))) ≤ 𝐴)) |
| 121 | | pntrlog2bndlem3.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴) |
| 122 | 121 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ∀𝑦 ∈
(1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴) |
| 123 | 7 | nnge1d 12314 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ 𝑛) |
| 124 | | 1re 11261 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
| 125 | | elicopnf 13485 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℝ → (𝑛 ∈
(1[,)+∞) ↔ (𝑛
∈ ℝ ∧ 1 ≤ 𝑛))) |
| 126 | 124, 125 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (1[,)+∞) ↔
(𝑛 ∈ ℝ ∧ 1
≤ 𝑛)) |
| 127 | 8, 123, 126 | sylanbrc 583 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
(1[,)+∞)) |
| 128 | 120, 122,
127 | rspcdva 3623 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛)))) ≤ 𝐴) |
| 129 | 112, 79, 8, 108, 128 | lemul1ad 12207 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(((𝑆‘𝑛) / 𝑛) − (2 · (log‘𝑛)))) · 𝑛) ≤ (𝐴 · 𝑛)) |
| 130 | 111, 129 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ≤ (𝐴 · 𝑛)) |
| 131 | 82, 34, 84, 85, 86, 87, 90, 130 | lemul12ad 12210 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))))) · (abs‘((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ≤ ((abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛)))) · (𝐴 · 𝑛))) |
| 132 | 81, 83 | absmuld 15493 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = ((abs‘((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))))) · (abs‘((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))) |
| 133 | 41 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐴 ∈
ℂ) |
| 134 | 34 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛)))) ∈ ℂ) |
| 135 | 133, 92, 134 | mulassd 11284 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝐴 · 𝑛) · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) = (𝐴 · (𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))))) |
| 136 | 133, 92 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐴 · 𝑛) ∈
ℂ) |
| 137 | 136, 134 | mulcomd 11282 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝐴 · 𝑛) · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) = ((abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛)))) · (𝐴 · 𝑛))) |
| 138 | 135, 137 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐴 · (𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛)))))) = ((abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛)))) · (𝐴 · 𝑛))) |
| 139 | 131, 132,
138 | 3brtr4d 5175 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ≤ (𝐴 · (𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))))) |
| 140 | 5, 76, 80, 139 | fsumle 15835 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(𝐴 · (𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))))) |
| 141 | 41 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈
ℂ) |
| 142 | 35 | recnd 11289 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ·
(abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) ∈ ℂ) |
| 143 | 5, 141, 142 | fsummulc2 15820 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝐴 · (𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))))) |
| 144 | 140, 143 | breqtrrd 5171 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ≤ (𝐴 · Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))))) |
| 145 | 73, 77, 74, 78, 144 | letrd 11418 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ≤ (𝐴 · Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))))) |
| 146 | 73, 74, 38, 145 | lediv1dd 13135 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) ≤ ((𝐴 · Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛)))))) / (𝑥 · (log‘𝑥)))) |
| 147 | 38 | rpcnd 13079 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈
ℂ) |
| 148 | 38 | rpne0d 13082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ≠ 0) |
| 149 | 72, 147, 148 | absdivd 15494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (abs‘(𝑥 · (log‘𝑥))))) |
| 150 | 38 | rpred 13077 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈
ℝ) |
| 151 | 38 | rpge0d 13081 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑥 · (log‘𝑥))) |
| 152 | 150, 151 | absidd 15461 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(𝑥 ·
(log‘𝑥))) = (𝑥 · (log‘𝑥))) |
| 153 | 152 | oveq2d 7447 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (abs‘(𝑥 · (log‘𝑥)))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) |
| 154 | 149, 153 | eqtr2d 2778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) |
| 155 | 36 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) ∈ ℂ) |
| 156 | 141, 155,
147, 148 | divassd 12078 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((𝐴 · Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛)))))) / (𝑥 · (log‘𝑥))) = (𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥))))) |
| 157 | 146, 154,
156 | 3brtr3d 5174 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ≤ (𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥))))) |
| 158 | 52 | leabsd 15453 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · (Σ𝑛 ∈
(1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥)))) ≤ (abs‘(𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥)))))) |
| 159 | 69, 52, 71, 157, 158 | letrd 11418 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ≤ (abs‘(𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥)))))) |
| 160 | 159 | adantrr 717 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ≤ (abs‘(𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥)))))) |
| 161 | 1, 51, 52, 68, 160 | o1le 15689 |
1
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |