Proof of Theorem dchrvmasumlem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1red 11262 | . 2
⊢ (𝜑 → 1 ∈
ℝ) | 
| 2 |  | dchrvmasum.c | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) | 
| 3 |  | elrege0 13494 | . . . . . . 7
⊢ (𝐶 ∈ (0[,)+∞) ↔
(𝐶 ∈ ℝ ∧ 0
≤ 𝐶)) | 
| 4 | 2, 3 | sylib 218 | . . . . . 6
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) | 
| 5 | 4 | simpld 494 | . . . . 5
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 6 | 5 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈
ℝ) | 
| 7 |  | fzfid 14014 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) | 
| 8 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) | 
| 9 |  | elfznn 13593 | . . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℕ) | 
| 10 | 9 | nnrpd 13075 | . . . . . . . 8
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℝ+) | 
| 11 |  | rpdivcl 13060 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
ℝ+) → (𝑥 / 𝑑) ∈
ℝ+) | 
| 12 | 8, 10, 11 | syl2an 596 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑑) ∈
ℝ+) | 
| 13 | 12 | relogcld 26665 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑑)) ∈
ℝ) | 
| 14 | 8 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ+) | 
| 15 | 13, 14 | rerpdivcld 13108 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑑)) / 𝑥) ∈ ℝ) | 
| 16 | 7, 15 | fsumrecl 15770 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ) | 
| 17 | 6, 16 | remulcld 11291 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐶 · Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ ℝ) | 
| 18 |  | dchrvmasum.r | . . . . 5
⊢ (𝜑 → 𝑅 ∈ ℝ) | 
| 19 |  | 3nn 12345 | . . . . . . 7
⊢ 3 ∈
ℕ | 
| 20 |  | nnrp 13046 | . . . . . . 7
⊢ (3 ∈
ℕ → 3 ∈ ℝ+) | 
| 21 |  | relogcl 26617 | . . . . . . 7
⊢ (3 ∈
ℝ+ → (log‘3) ∈ ℝ) | 
| 22 | 19, 20, 21 | mp2b 10 | . . . . . 6
⊢
(log‘3) ∈ ℝ | 
| 23 |  | 1re 11261 | . . . . . 6
⊢ 1 ∈
ℝ | 
| 24 | 22, 23 | readdcli 11276 | . . . . 5
⊢
((log‘3) + 1) ∈ ℝ | 
| 25 |  | remulcl 11240 | . . . . 5
⊢ ((𝑅 ∈ ℝ ∧
((log‘3) + 1) ∈ ℝ) → (𝑅 · ((log‘3) + 1)) ∈
ℝ) | 
| 26 | 18, 24, 25 | sylancl 586 | . . . 4
⊢ (𝜑 → (𝑅 · ((log‘3) + 1)) ∈
ℝ) | 
| 27 | 26 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 · ((log‘3) + 1))
∈ ℝ) | 
| 28 |  | rpssre 13042 | . . . . 5
⊢
ℝ+ ⊆ ℝ | 
| 29 | 5 | recnd 11289 | . . . . 5
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 30 |  | o1const 15656 | . . . . 5
⊢
((ℝ+ ⊆ ℝ ∧ 𝐶 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 𝐶) ∈
𝑂(1)) | 
| 31 | 28, 29, 30 | sylancr 587 | . . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 𝐶) ∈
𝑂(1)) | 
| 32 |  | logfacrlim2 27270 | . . . . 5
⊢ (𝑥 ∈ ℝ+
↦ Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ⇝𝑟
1 | 
| 33 |  | rlimo1 15653 | . . . . 5
⊢ ((𝑥 ∈ ℝ+
↦ Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ⇝𝑟 1 →
(𝑥 ∈
ℝ+ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ 𝑂(1)) | 
| 34 | 32, 33 | mp1i 13 | . . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ 𝑂(1)) | 
| 35 | 6, 16, 31, 34 | o1mul2 15661 | . . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝐶 · Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥))) ∈ 𝑂(1)) | 
| 36 | 26 | recnd 11289 | . . . 4
⊢ (𝜑 → (𝑅 · ((log‘3) + 1)) ∈
ℂ) | 
| 37 |  | o1const 15656 | . . . 4
⊢
((ℝ+ ⊆ ℝ ∧ (𝑅 · ((log‘3) + 1)) ∈
ℂ) → (𝑥 ∈
ℝ+ ↦ (𝑅 · ((log‘3) + 1))) ∈
𝑂(1)) | 
| 38 | 28, 36, 37 | sylancr 587 | . . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑅 · ((log‘3) + 1)))
∈ 𝑂(1)) | 
| 39 | 17, 27, 35, 38 | o1add2 15660 | . 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((𝐶 · Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))) ∈
𝑂(1)) | 
| 40 | 17, 27 | readdcld 11290 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝐶 · Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ∈
ℝ) | 
| 41 |  | dchrvmasum.g | . . . . . . . . 9
⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾) | 
| 42 | 41 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑚 = (𝑥 / 𝑑) → (𝐹 ∈ ℂ ↔ 𝐾 ∈ ℂ)) | 
| 43 |  | dchrvmasum.f | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝐹 ∈
ℂ) | 
| 44 | 43 | ralrimiva 3146 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑚 ∈ ℝ+ 𝐹 ∈ ℂ) | 
| 45 | 44 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ∀𝑚 ∈
ℝ+ 𝐹
∈ ℂ) | 
| 46 | 42, 45, 12 | rspcdva 3623 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝐾 ∈
ℂ) | 
| 47 |  | dchrvmasum.t | . . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ ℂ) | 
| 48 | 47 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑇 ∈
ℂ) | 
| 49 | 46, 48 | subcld 11620 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐾 − 𝑇) ∈
ℂ) | 
| 50 | 49 | abscld 15475 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝐾
− 𝑇)) ∈
ℝ) | 
| 51 | 9 | adantl 481 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℕ) | 
| 52 | 50, 51 | nndivred 12320 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝐾
− 𝑇)) / 𝑑) ∈
ℝ) | 
| 53 | 7, 52 | fsumrecl 15770 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ) | 
| 54 | 53 | recnd 11289 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℂ) | 
| 55 | 51 | nnrpd 13075 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℝ+) | 
| 56 | 49 | absge0d 15483 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘(𝐾
− 𝑇))) | 
| 57 | 50, 55, 56 | divge0d 13117 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((abs‘(𝐾 − 𝑇)) / 𝑑)) | 
| 58 | 7, 52, 57 | fsumge0 15831 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 0 ≤
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) | 
| 59 | 53, 58 | absidd 15461 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) = Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) | 
| 60 | 59, 53 | eqeltrd 2841 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ ℝ) | 
| 61 | 40 | recnd 11289 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝐶 · Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ∈
ℂ) | 
| 62 | 61 | abscld 15475 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘((𝐶 ·
Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1)))) ∈
ℝ) | 
| 63 |  | 3re 12346 | . . . . . . . 8
⊢ 3 ∈
ℝ | 
| 64 | 63 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 3 ∈
ℝ) | 
| 65 |  | 1le3 12478 | . . . . . . 7
⊢ 1 ≤
3 | 
| 66 | 64, 65 | jctir 520 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (3 ∈
ℝ ∧ 1 ≤ 3)) | 
| 67 | 18 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑅 ∈
ℝ) | 
| 68 | 23 | rexri 11319 | . . . . . . . . . 10
⊢ 1 ∈
ℝ* | 
| 69 | 63 | rexri 11319 | . . . . . . . . . 10
⊢ 3 ∈
ℝ* | 
| 70 |  | 1lt3 12439 | . . . . . . . . . 10
⊢ 1 <
3 | 
| 71 |  | lbico1 13441 | . . . . . . . . . 10
⊢ ((1
∈ ℝ* ∧ 3 ∈ ℝ* ∧ 1 < 3)
→ 1 ∈ (1[,)3)) | 
| 72 | 68, 69, 70, 71 | mp3an 1463 | . . . . . . . . 9
⊢ 1 ∈
(1[,)3) | 
| 73 |  | 0red 11264 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ∈
ℝ) | 
| 74 |  | elico2 13451 | . . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ 3 ∈ ℝ*) → (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3))) | 
| 75 | 23, 69, 74 | mp2an 692 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤
𝑚 ∧ 𝑚 < 3)) | 
| 76 | 75 | simp1bi 1146 | . . . . . . . . . . . . 13
⊢ (𝑚 ∈ (1[,)3) → 𝑚 ∈
ℝ) | 
| 77 |  | 0red 11264 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (1[,)3) → 0 ∈
ℝ) | 
| 78 |  | 1red 11262 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (1[,)3) → 1 ∈
ℝ) | 
| 79 |  | 0lt1 11785 | . . . . . . . . . . . . . . 15
⊢ 0 <
1 | 
| 80 | 79 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (1[,)3) → 0 <
1) | 
| 81 | 75 | simp2bi 1147 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (1[,)3) → 1 ≤
𝑚) | 
| 82 | 77, 78, 76, 80, 81 | ltletrd 11421 | . . . . . . . . . . . . 13
⊢ (𝑚 ∈ (1[,)3) → 0 <
𝑚) | 
| 83 | 76, 82 | elrpd 13074 | . . . . . . . . . . . 12
⊢ (𝑚 ∈ (1[,)3) → 𝑚 ∈
ℝ+) | 
| 84 | 47 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝑇 ∈
ℂ) | 
| 85 | 43, 84 | subcld 11620 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → (𝐹 − 𝑇) ∈ ℂ) | 
| 86 | 85 | abscld 15475 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(abs‘(𝐹 − 𝑇)) ∈
ℝ) | 
| 87 | 83, 86 | sylan2 593 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘(𝐹 − 𝑇)) ∈ ℝ) | 
| 88 | 18 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝑅 ∈ ℝ) | 
| 89 | 85 | absge0d 15483 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 0 ≤
(abs‘(𝐹 − 𝑇))) | 
| 90 | 83, 89 | sylan2 593 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ≤
(abs‘(𝐹 − 𝑇))) | 
| 91 |  | dchrvmasum.2 | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅) | 
| 92 | 91 | r19.21bi 3251 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘(𝐹 − 𝑇)) ≤ 𝑅) | 
| 93 | 73, 87, 88, 90, 92 | letrd 11418 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ≤ 𝑅) | 
| 94 | 93 | ralrimiva 3146 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)0 ≤ 𝑅) | 
| 95 |  | biidd 262 | . . . . . . . . . 10
⊢ (𝑚 = 1 → (0 ≤ 𝑅 ↔ 0 ≤ 𝑅)) | 
| 96 | 95 | rspcv 3618 | . . . . . . . . 9
⊢ (1 ∈
(1[,)3) → (∀𝑚
∈ (1[,)3)0 ≤ 𝑅
→ 0 ≤ 𝑅)) | 
| 97 | 72, 94, 96 | mpsyl 68 | . . . . . . . 8
⊢ (𝜑 → 0 ≤ 𝑅) | 
| 98 | 97 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 0 ≤
𝑅) | 
| 99 | 67, 98 | jca 511 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 ∈ ℝ ∧ 0 ≤
𝑅)) | 
| 100 | 50 | recnd 11289 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝐾
− 𝑇)) ∈
ℂ) | 
| 101 | 5 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝐶 ∈
ℝ) | 
| 102 | 101, 15 | remulcld 11291 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 ·
((log‘(𝑥 / 𝑑)) / 𝑥)) ∈ ℝ) | 
| 103 | 4 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 ∈ ℝ
∧ 0 ≤ 𝐶)) | 
| 104 |  | log1 26627 | . . . . . . . . 9
⊢
(log‘1) = 0 | 
| 105 | 51 | nncnd 12282 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℂ) | 
| 106 | 105 | mullidd 11279 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 · 𝑑) =
𝑑) | 
| 107 |  | rpre 13043 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) | 
| 108 | 107 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) | 
| 109 |  | fznnfl 13902 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ → (𝑑 ∈
(1...(⌊‘𝑥))
↔ (𝑑 ∈ ℕ
∧ 𝑑 ≤ 𝑥))) | 
| 110 | 108, 109 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑑 ∈
(1...(⌊‘𝑥))
↔ (𝑑 ∈ ℕ
∧ 𝑑 ≤ 𝑥))) | 
| 111 | 110 | simplbda 499 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ≤ 𝑥) | 
| 112 | 106, 111 | eqbrtrd 5165 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 · 𝑑) ≤
𝑥) | 
| 113 |  | 1red 11262 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) | 
| 114 | 107 | ad2antlr 727 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ) | 
| 115 | 113, 114,
55 | lemuldivd 13126 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((1 · 𝑑) ≤
𝑥 ↔ 1 ≤ (𝑥 / 𝑑))) | 
| 116 | 112, 115 | mpbid 232 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ (𝑥 / 𝑑)) | 
| 117 |  | 1rp 13038 | . . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ | 
| 118 | 117 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ+) | 
| 119 | 118, 12 | logled 26669 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 ≤ (𝑥 / 𝑑) ↔ (log‘1) ≤
(log‘(𝑥 / 𝑑)))) | 
| 120 | 116, 119 | mpbid 232 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (log‘1) ≤ (log‘(𝑥 / 𝑑))) | 
| 121 | 104, 120 | eqbrtrrid 5179 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (log‘(𝑥
/ 𝑑))) | 
| 122 |  | rpregt0 13049 | . . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) | 
| 123 | 122 | ad2antlr 727 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) | 
| 124 |  | divge0 12137 | . . . . . . . 8
⊢
((((log‘(𝑥 /
𝑑)) ∈ ℝ ∧ 0
≤ (log‘(𝑥 / 𝑑))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤
((log‘(𝑥 / 𝑑)) / 𝑥)) | 
| 125 | 13, 121, 123, 124 | syl21anc 838 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((log‘(𝑥 / 𝑑)) / 𝑥)) | 
| 126 |  | mulge0 11781 | . . . . . . 7
⊢ (((𝐶 ∈ ℝ ∧ 0 ≤
𝐶) ∧
(((log‘(𝑥 / 𝑑)) / 𝑥) ∈ ℝ ∧ 0 ≤
((log‘(𝑥 / 𝑑)) / 𝑥))) → 0 ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥))) | 
| 127 | 103, 15, 125, 126 | syl12anc 837 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (𝐶 ·
((log‘(𝑥 / 𝑑)) / 𝑥))) | 
| 128 |  | absidm 15362 | . . . . . . . . 9
⊢ ((𝐾 − 𝑇) ∈ ℂ →
(abs‘(abs‘(𝐾
− 𝑇))) =
(abs‘(𝐾 − 𝑇))) | 
| 129 | 49, 128 | syl 17 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(abs‘(𝐾 − 𝑇))) = (abs‘(𝐾 − 𝑇))) | 
| 130 | 129 | adantr 480 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 3 ≤ (𝑥 / 𝑑)) →
(abs‘(abs‘(𝐾
− 𝑇))) =
(abs‘(𝐾 − 𝑇))) | 
| 131 | 41 | fvoveq1d 7453 | . . . . . . . . . 10
⊢ (𝑚 = (𝑥 / 𝑑) → (abs‘(𝐹 − 𝑇)) = (abs‘(𝐾 − 𝑇))) | 
| 132 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑚 = (𝑥 / 𝑑) → (log‘𝑚) = (log‘(𝑥 / 𝑑))) | 
| 133 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑚 = (𝑥 / 𝑑) → 𝑚 = (𝑥 / 𝑑)) | 
| 134 | 132, 133 | oveq12d 7449 | . . . . . . . . . . 11
⊢ (𝑚 = (𝑥 / 𝑑) → ((log‘𝑚) / 𝑚) = ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) | 
| 135 | 134 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑚 = (𝑥 / 𝑑) → (𝐶 · ((log‘𝑚) / 𝑚)) = (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)))) | 
| 136 | 131, 135 | breq12d 5156 | . . . . . . . . 9
⊢ (𝑚 = (𝑥 / 𝑑) → ((abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)) ↔ (abs‘(𝐾 − 𝑇)) ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))))) | 
| 137 |  | dchrvmasum.1 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚))) | 
| 138 | 137 | ralrimiva 3146 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑚 ∈ (3[,)+∞)(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚))) | 
| 139 | 138 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 3 ≤ (𝑥 / 𝑑)) → ∀𝑚 ∈
(3[,)+∞)(abs‘(𝐹
− 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚))) | 
| 140 |  | nndivre 12307 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ) → (𝑥 / 𝑑) ∈ ℝ) | 
| 141 | 108, 9, 140 | syl2an 596 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑑) ∈
ℝ) | 
| 142 | 141 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 3 ≤ (𝑥 / 𝑑)) → (𝑥 / 𝑑) ∈ ℝ) | 
| 143 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 3 ≤ (𝑥 / 𝑑)) → 3 ≤ (𝑥 / 𝑑)) | 
| 144 |  | elicopnf 13485 | . . . . . . . . . . 11
⊢ (3 ∈
ℝ → ((𝑥 / 𝑑) ∈ (3[,)+∞) ↔
((𝑥 / 𝑑) ∈ ℝ ∧ 3 ≤ (𝑥 / 𝑑)))) | 
| 145 | 63, 144 | ax-mp 5 | . . . . . . . . . 10
⊢ ((𝑥 / 𝑑) ∈ (3[,)+∞) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 3 ≤ (𝑥 / 𝑑))) | 
| 146 | 142, 143,
145 | sylanbrc 583 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 3 ≤ (𝑥 / 𝑑)) → (𝑥 / 𝑑) ∈ (3[,)+∞)) | 
| 147 | 136, 139,
146 | rspcdva 3623 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(𝐾 − 𝑇)) ≤ (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)))) | 
| 148 | 13 | recnd 11289 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑑)) ∈
ℂ) | 
| 149 |  | rpcnne0 13053 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) | 
| 150 | 149 | ad2antlr 727 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) | 
| 151 | 55 | rpcnne0d 13086 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑑 ∈ ℂ
∧ 𝑑 ≠
0)) | 
| 152 |  | divdiv2 11979 | . . . . . . . . . . . . 13
⊢
(((log‘(𝑥 /
𝑑)) ∈ ℂ ∧
(𝑥 ∈ ℂ ∧
𝑥 ≠ 0) ∧ (𝑑 ∈ ℂ ∧ 𝑑 ≠ 0)) →
((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥)) | 
| 153 | 148, 150,
151, 152 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥)) | 
| 154 |  | div23 11941 | . . . . . . . . . . . . 13
⊢
(((log‘(𝑥 /
𝑑)) ∈ ℂ ∧
𝑑 ∈ ℂ ∧
(𝑥 ∈ ℂ ∧
𝑥 ≠ 0)) →
(((log‘(𝑥 / 𝑑)) · 𝑑) / 𝑥) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑)) | 
| 155 | 148, 105,
150, 154 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((log‘(𝑥 /
𝑑)) · 𝑑) / 𝑥) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑)) | 
| 156 | 153, 155 | eqtrd 2777 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑑)) / (𝑥 / 𝑑)) = (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑)) | 
| 157 | 156 | oveq2d 7447 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 ·
((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = (𝐶 · (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))) | 
| 158 | 29 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝐶 ∈
ℂ) | 
| 159 | 15 | recnd 11289 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑑)) / 𝑥) ∈ ℂ) | 
| 160 | 158, 159,
105 | mulassd 11284 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((𝐶 ·
((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑) = (𝐶 · (((log‘(𝑥 / 𝑑)) / 𝑥) · 𝑑))) | 
| 161 | 157, 160 | eqtr4d 2780 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐶 ·
((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑)) | 
| 162 | 161 | adantr 480 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 3 ≤ (𝑥 / 𝑑)) → (𝐶 · ((log‘(𝑥 / 𝑑)) / (𝑥 / 𝑑))) = ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑)) | 
| 163 | 147, 162 | breqtrd 5169 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 3 ≤ (𝑥 / 𝑑)) → (abs‘(𝐾 − 𝑇)) ≤ ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑)) | 
| 164 | 130, 163 | eqbrtrd 5165 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 3 ≤ (𝑥 / 𝑑)) →
(abs‘(abs‘(𝐾
− 𝑇))) ≤ ((𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) · 𝑑)) | 
| 165 | 129 | adantr 480 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑑) < 3) →
(abs‘(abs‘(𝐾
− 𝑇))) =
(abs‘(𝐾 − 𝑇))) | 
| 166 | 131 | breq1d 5153 | . . . . . . . 8
⊢ (𝑚 = (𝑥 / 𝑑) → ((abs‘(𝐹 − 𝑇)) ≤ 𝑅 ↔ (abs‘(𝐾 − 𝑇)) ≤ 𝑅)) | 
| 167 | 91 | ad3antrrr 730 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑑) < 3) → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅) | 
| 168 | 141 | adantr 480 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) ∈ ℝ) | 
| 169 | 116 | adantr 480 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑑) < 3) → 1 ≤ (𝑥 / 𝑑)) | 
| 170 |  | simpr 484 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) < 3) | 
| 171 |  | elico2 13451 | . . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ 3 ∈ ℝ*) → ((𝑥 / 𝑑) ∈ (1[,)3) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑑) ∧ (𝑥 / 𝑑) < 3))) | 
| 172 | 23, 69, 171 | mp2an 692 | . . . . . . . . 9
⊢ ((𝑥 / 𝑑) ∈ (1[,)3) ↔ ((𝑥 / 𝑑) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑑) ∧ (𝑥 / 𝑑) < 3)) | 
| 173 | 168, 169,
170, 172 | syl3anbrc 1344 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑑) < 3) → (𝑥 / 𝑑) ∈ (1[,)3)) | 
| 174 | 166, 167,
173 | rspcdva 3623 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑑) < 3) →
(abs‘(𝐾 − 𝑇)) ≤ 𝑅) | 
| 175 | 165, 174 | eqbrtrd 5165 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑑) < 3) →
(abs‘(abs‘(𝐾
− 𝑇))) ≤ 𝑅) | 
| 176 | 8, 66, 99, 100, 102, 127, 164, 175 | fsumharmonic 27055 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) +
1)))) | 
| 177 | 29 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐶 ∈
ℂ) | 
| 178 | 7, 177, 159 | fsummulc2 15820 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐶 · Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) = Σ𝑑 ∈ (1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥))) | 
| 179 | 178 | oveq1d 7446 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝐶 · Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) =
(Σ𝑑 ∈
(1...(⌊‘𝑥))(𝐶 · ((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) +
1)))) | 
| 180 | 176, 179 | breqtrrd 5171 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ ((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) +
1)))) | 
| 181 | 40 | leabsd 15453 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝐶 · Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) + 1))) ≤
(abs‘((𝐶 ·
Σ𝑑 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) +
1))))) | 
| 182 | 60, 40, 62, 180, 181 | letrd 11418 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) +
1))))) | 
| 183 | 182 | adantrr 717 | . 2
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ≤ (abs‘((𝐶 · Σ𝑑 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑑)) / 𝑥)) + (𝑅 · ((log‘3) +
1))))) | 
| 184 | 1, 39, 40, 54, 183 | o1le 15689 | 1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1)) |