Proof of Theorem pntlemk
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2re 12340 | . . . . 5
⊢ 2 ∈
ℝ | 
| 2 |  | fzfid 14014 | . . . . . 6
⊢ (𝜑 → (1...(⌊‘(𝑍 / 𝑌))) ∈ Fin) | 
| 3 |  | elfznn 13593 | . . . . . . . . . 10
⊢ (𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌))) → 𝑛 ∈
ℕ) | 
| 4 | 3 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℕ) | 
| 5 | 4 | nnrpd 13075 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℝ+) | 
| 6 | 5 | relogcld 26665 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℝ) | 
| 7 | 6, 4 | nndivred 12320 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((log‘𝑛) / 𝑛) ∈ ℝ) | 
| 8 | 2, 7 | fsumrecl 15770 | . . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((log‘𝑛) / 𝑛) ∈ ℝ) | 
| 9 |  | remulcl 11240 | . . . . 5
⊢ ((2
∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((log‘𝑛) / 𝑛) ∈ ℝ) → (2 ·
Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛)) ∈ ℝ) | 
| 10 | 1, 8, 9 | sylancr 587 | . . . 4
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛)) ∈ ℝ) | 
| 11 |  | pntlem1.r | . . . . . . . . 9
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) | 
| 12 |  | pntlem1.a | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
ℝ+) | 
| 13 |  | pntlem1.b | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈
ℝ+) | 
| 14 |  | pntlem1.l | . . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ (0(,)1)) | 
| 15 |  | pntlem1.d | . . . . . . . . 9
⊢ 𝐷 = (𝐴 + 1) | 
| 16 |  | pntlem1.f | . . . . . . . . 9
⊢ 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) | 
| 17 |  | pntlem1.u | . . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈
ℝ+) | 
| 18 |  | pntlem1.u2 | . . . . . . . . 9
⊢ (𝜑 → 𝑈 ≤ 𝐴) | 
| 19 |  | pntlem1.e | . . . . . . . . 9
⊢ 𝐸 = (𝑈 / 𝐷) | 
| 20 |  | pntlem1.k | . . . . . . . . 9
⊢ 𝐾 = (exp‘(𝐵 / 𝐸)) | 
| 21 |  | pntlem1.y | . . . . . . . . 9
⊢ (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤
𝑌)) | 
| 22 |  | pntlem1.x | . . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋)) | 
| 23 |  | pntlem1.c | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈
ℝ+) | 
| 24 |  | pntlem1.w | . . . . . . . . 9
⊢ 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) | 
| 25 |  | pntlem1.z | . . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ (𝑊[,)+∞)) | 
| 26 | 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25 | pntlemb 27641 | . . . . . . . 8
⊢ (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 <
𝑍 ∧ e ≤
(√‘𝑍) ∧
(√‘𝑍) ≤
(𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) | 
| 27 | 26 | simp1d 1143 | . . . . . . 7
⊢ (𝜑 → 𝑍 ∈
ℝ+) | 
| 28 | 27 | relogcld 26665 | . . . . . 6
⊢ (𝜑 → (log‘𝑍) ∈
ℝ) | 
| 29 |  | peano2re 11434 | . . . . . 6
⊢
((log‘𝑍)
∈ ℝ → ((log‘𝑍) + 1) ∈ ℝ) | 
| 30 | 28, 29 | syl 17 | . . . . 5
⊢ (𝜑 → ((log‘𝑍) + 1) ∈
ℝ) | 
| 31 | 30 | resqcld 14165 | . . . 4
⊢ (𝜑 → (((log‘𝑍) + 1)↑2) ∈
ℝ) | 
| 32 |  | 3re 12346 | . . . . . 6
⊢ 3 ∈
ℝ | 
| 33 |  | readdcl 11238 | . . . . . 6
⊢
(((log‘𝑍)
∈ ℝ ∧ 3 ∈ ℝ) → ((log‘𝑍) + 3) ∈ ℝ) | 
| 34 | 28, 32, 33 | sylancl 586 | . . . . 5
⊢ (𝜑 → ((log‘𝑍) + 3) ∈
ℝ) | 
| 35 | 34, 28 | remulcld 11291 | . . . 4
⊢ (𝜑 → (((log‘𝑍) + 3) · (log‘𝑍)) ∈
ℝ) | 
| 36 | 27 | rpred 13077 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑍 ∈ ℝ) | 
| 37 | 21 | simpld 494 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈
ℝ+) | 
| 38 | 36, 37 | rerpdivcld 13108 | . . . . . . . . . 10
⊢ (𝜑 → (𝑍 / 𝑌) ∈ ℝ) | 
| 39 |  | 1red 11262 | . . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℝ) | 
| 40 | 27 | rpsqrtcld 15450 | . . . . . . . . . . . 12
⊢ (𝜑 → (√‘𝑍) ∈
ℝ+) | 
| 41 | 40 | rpred 13077 | . . . . . . . . . . 11
⊢ (𝜑 → (√‘𝑍) ∈
ℝ) | 
| 42 |  | ere 16125 | . . . . . . . . . . . . 13
⊢ e ∈
ℝ | 
| 43 | 42 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → e ∈
ℝ) | 
| 44 |  | 1re 11261 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ | 
| 45 |  | 1lt2 12437 | . . . . . . . . . . . . . . 15
⊢ 1 <
2 | 
| 46 |  | egt2lt3 16242 | . . . . . . . . . . . . . . . 16
⊢ (2 < e
∧ e < 3) | 
| 47 | 46 | simpli 483 | . . . . . . . . . . . . . . 15
⊢ 2 <
e | 
| 48 | 44, 1, 42 | lttri 11387 | . . . . . . . . . . . . . . 15
⊢ ((1 <
2 ∧ 2 < e) → 1 < e) | 
| 49 | 45, 47, 48 | mp2an 692 | . . . . . . . . . . . . . 14
⊢ 1 <
e | 
| 50 | 44, 42, 49 | ltleii 11384 | . . . . . . . . . . . . 13
⊢ 1 ≤
e | 
| 51 | 50 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 1 ≤ e) | 
| 52 | 26 | simp2d 1144 | . . . . . . . . . . . . 13
⊢ (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌))) | 
| 53 | 52 | simp2d 1144 | . . . . . . . . . . . 12
⊢ (𝜑 → e ≤
(√‘𝑍)) | 
| 54 | 39, 43, 41, 51, 53 | letrd 11418 | . . . . . . . . . . 11
⊢ (𝜑 → 1 ≤
(√‘𝑍)) | 
| 55 | 52 | simp3d 1145 | . . . . . . . . . . 11
⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / 𝑌)) | 
| 56 | 39, 41, 38, 54, 55 | letrd 11418 | . . . . . . . . . 10
⊢ (𝜑 → 1 ≤ (𝑍 / 𝑌)) | 
| 57 |  | flge1nn 13861 | . . . . . . . . . 10
⊢ (((𝑍 / 𝑌) ∈ ℝ ∧ 1 ≤ (𝑍 / 𝑌)) → (⌊‘(𝑍 / 𝑌)) ∈ ℕ) | 
| 58 | 38, 56, 57 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (⌊‘(𝑍 / 𝑌)) ∈ ℕ) | 
| 59 | 58 | nnrpd 13075 | . . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑍 / 𝑌)) ∈
ℝ+) | 
| 60 | 59 | relogcld 26665 | . . . . . . 7
⊢ (𝜑 →
(log‘(⌊‘(𝑍 / 𝑌))) ∈ ℝ) | 
| 61 | 60, 39 | readdcld 11290 | . . . . . 6
⊢ (𝜑 →
((log‘(⌊‘(𝑍 / 𝑌))) + 1) ∈ ℝ) | 
| 62 | 61 | resqcld 14165 | . . . . 5
⊢ (𝜑 →
(((log‘(⌊‘(𝑍 / 𝑌))) + 1)↑2) ∈
ℝ) | 
| 63 |  | logdivbnd 27600 | . . . . . . 7
⊢
((⌊‘(𝑍 /
𝑌)) ∈ ℕ →
Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛) ≤ ((((log‘(⌊‘(𝑍 / 𝑌))) + 1)↑2) / 2)) | 
| 64 | 58, 63 | syl 17 | . . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((log‘𝑛) / 𝑛) ≤ ((((log‘(⌊‘(𝑍 / 𝑌))) + 1)↑2) / 2)) | 
| 65 | 1 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 2 ∈
ℝ) | 
| 66 |  | 2pos 12369 | . . . . . . . 8
⊢ 0 <
2 | 
| 67 | 66 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 0 < 2) | 
| 68 |  | lemuldiv2 12149 | . . . . . . 7
⊢
((Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛) ∈ ℝ ∧
(((log‘(⌊‘(𝑍 / 𝑌))) + 1)↑2) ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((log‘𝑛) / 𝑛)) ≤ (((log‘(⌊‘(𝑍 / 𝑌))) + 1)↑2) ↔ Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛) ≤ ((((log‘(⌊‘(𝑍 / 𝑌))) + 1)↑2) / 2))) | 
| 69 | 8, 62, 65, 67, 68 | syl112anc 1376 | . . . . . 6
⊢ (𝜑 → ((2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛)) ≤ (((log‘(⌊‘(𝑍 / 𝑌))) + 1)↑2) ↔ Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛) ≤ ((((log‘(⌊‘(𝑍 / 𝑌))) + 1)↑2) / 2))) | 
| 70 | 64, 69 | mpbird 257 | . . . . 5
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛)) ≤ (((log‘(⌊‘(𝑍 / 𝑌))) + 1)↑2)) | 
| 71 |  | reflcl 13836 | . . . . . . . . . 10
⊢ ((𝑍 / 𝑌) ∈ ℝ →
(⌊‘(𝑍 / 𝑌)) ∈
ℝ) | 
| 72 | 38, 71 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (⌊‘(𝑍 / 𝑌)) ∈ ℝ) | 
| 73 |  | flle 13839 | . . . . . . . . . 10
⊢ ((𝑍 / 𝑌) ∈ ℝ →
(⌊‘(𝑍 / 𝑌)) ≤ (𝑍 / 𝑌)) | 
| 74 | 38, 73 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (⌊‘(𝑍 / 𝑌)) ≤ (𝑍 / 𝑌)) | 
| 75 | 21 | simprd 495 | . . . . . . . . . . 11
⊢ (𝜑 → 1 ≤ 𝑌) | 
| 76 |  | 1rp 13038 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℝ+ | 
| 77 | 76 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ+) | 
| 78 | 77, 37, 27 | lediv2d 13101 | . . . . . . . . . . 11
⊢ (𝜑 → (1 ≤ 𝑌 ↔ (𝑍 / 𝑌) ≤ (𝑍 / 1))) | 
| 79 | 75, 78 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → (𝑍 / 𝑌) ≤ (𝑍 / 1)) | 
| 80 | 36 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑍 ∈ ℂ) | 
| 81 | 80 | div1d 12035 | . . . . . . . . . 10
⊢ (𝜑 → (𝑍 / 1) = 𝑍) | 
| 82 | 79, 81 | breqtrd 5169 | . . . . . . . . 9
⊢ (𝜑 → (𝑍 / 𝑌) ≤ 𝑍) | 
| 83 | 72, 38, 36, 74, 82 | letrd 11418 | . . . . . . . 8
⊢ (𝜑 → (⌊‘(𝑍 / 𝑌)) ≤ 𝑍) | 
| 84 | 59, 27 | logled 26669 | . . . . . . . 8
⊢ (𝜑 → ((⌊‘(𝑍 / 𝑌)) ≤ 𝑍 ↔ (log‘(⌊‘(𝑍 / 𝑌))) ≤ (log‘𝑍))) | 
| 85 | 83, 84 | mpbid 232 | . . . . . . 7
⊢ (𝜑 →
(log‘(⌊‘(𝑍 / 𝑌))) ≤ (log‘𝑍)) | 
| 86 | 60, 28, 39, 85 | leadd1dd 11877 | . . . . . 6
⊢ (𝜑 →
((log‘(⌊‘(𝑍 / 𝑌))) + 1) ≤ ((log‘𝑍) + 1)) | 
| 87 |  | 0red 11264 | . . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) | 
| 88 |  | log1 26627 | . . . . . . . . 9
⊢
(log‘1) = 0 | 
| 89 | 58 | nnge1d 12314 | . . . . . . . . . 10
⊢ (𝜑 → 1 ≤
(⌊‘(𝑍 / 𝑌))) | 
| 90 |  | logleb 26645 | . . . . . . . . . . 11
⊢ ((1
∈ ℝ+ ∧ (⌊‘(𝑍 / 𝑌)) ∈ ℝ+) → (1
≤ (⌊‘(𝑍 /
𝑌)) ↔ (log‘1)
≤ (log‘(⌊‘(𝑍 / 𝑌))))) | 
| 91 | 76, 59, 90 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (1 ≤
(⌊‘(𝑍 / 𝑌)) ↔ (log‘1) ≤
(log‘(⌊‘(𝑍 / 𝑌))))) | 
| 92 | 89, 91 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → (log‘1) ≤
(log‘(⌊‘(𝑍 / 𝑌)))) | 
| 93 | 88, 92 | eqbrtrrid 5179 | . . . . . . . 8
⊢ (𝜑 → 0 ≤
(log‘(⌊‘(𝑍 / 𝑌)))) | 
| 94 | 60 | lep1d 12199 | . . . . . . . 8
⊢ (𝜑 →
(log‘(⌊‘(𝑍 / 𝑌))) ≤ ((log‘(⌊‘(𝑍 / 𝑌))) + 1)) | 
| 95 | 87, 60, 61, 93, 94 | letrd 11418 | . . . . . . 7
⊢ (𝜑 → 0 ≤
((log‘(⌊‘(𝑍 / 𝑌))) + 1)) | 
| 96 | 87, 61, 30, 95, 86 | letrd 11418 | . . . . . . 7
⊢ (𝜑 → 0 ≤ ((log‘𝑍) + 1)) | 
| 97 | 61, 30, 95, 96 | le2sqd 14296 | . . . . . 6
⊢ (𝜑 →
(((log‘(⌊‘(𝑍 / 𝑌))) + 1) ≤ ((log‘𝑍) + 1) ↔
(((log‘(⌊‘(𝑍 / 𝑌))) + 1)↑2) ≤ (((log‘𝑍) +
1)↑2))) | 
| 98 | 86, 97 | mpbid 232 | . . . . 5
⊢ (𝜑 →
(((log‘(⌊‘(𝑍 / 𝑌))) + 1)↑2) ≤ (((log‘𝑍) + 1)↑2)) | 
| 99 | 10, 62, 31, 70, 98 | letrd 11418 | . . . 4
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛)) ≤ (((log‘𝑍) + 1)↑2)) | 
| 100 | 28 | resqcld 14165 | . . . . . . 7
⊢ (𝜑 → ((log‘𝑍)↑2) ∈
ℝ) | 
| 101 | 65, 28 | remulcld 11291 | . . . . . . 7
⊢ (𝜑 → (2 ·
(log‘𝑍)) ∈
ℝ) | 
| 102 | 100, 101 | readdcld 11290 | . . . . . 6
⊢ (𝜑 → (((log‘𝑍)↑2) + (2 ·
(log‘𝑍))) ∈
ℝ) | 
| 103 |  | loge 26628 | . . . . . . 7
⊢
(log‘e) = 1 | 
| 104 | 40 | rpge0d 13081 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ≤
(√‘𝑍)) | 
| 105 | 41, 41, 104, 54 | lemulge12d 12206 | . . . . . . . . . 10
⊢ (𝜑 → (√‘𝑍) ≤ ((√‘𝑍) · (√‘𝑍))) | 
| 106 | 27 | rprege0d 13084 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍)) | 
| 107 |  | remsqsqrt 15295 | . . . . . . . . . . 11
⊢ ((𝑍 ∈ ℝ ∧ 0 ≤
𝑍) →
((√‘𝑍) ·
(√‘𝑍)) = 𝑍) | 
| 108 | 106, 107 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍) | 
| 109 | 105, 108 | breqtrd 5169 | . . . . . . . . 9
⊢ (𝜑 → (√‘𝑍) ≤ 𝑍) | 
| 110 | 43, 41, 36, 53, 109 | letrd 11418 | . . . . . . . 8
⊢ (𝜑 → e ≤ 𝑍) | 
| 111 |  | epr 16244 | . . . . . . . . 9
⊢ e ∈
ℝ+ | 
| 112 |  | logleb 26645 | . . . . . . . . 9
⊢ ((e
∈ ℝ+ ∧ 𝑍 ∈ ℝ+) → (e ≤
𝑍 ↔ (log‘e) ≤
(log‘𝑍))) | 
| 113 | 111, 27, 112 | sylancr 587 | . . . . . . . 8
⊢ (𝜑 → (e ≤ 𝑍 ↔ (log‘e) ≤ (log‘𝑍))) | 
| 114 | 110, 113 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → (log‘e) ≤
(log‘𝑍)) | 
| 115 | 103, 114 | eqbrtrrid 5179 | . . . . . 6
⊢ (𝜑 → 1 ≤ (log‘𝑍)) | 
| 116 | 39, 28, 102, 115 | leadd2dd 11878 | . . . . 5
⊢ (𝜑 → ((((log‘𝑍)↑2) + (2 ·
(log‘𝑍))) + 1) ≤
((((log‘𝑍)↑2) +
(2 · (log‘𝑍)))
+ (log‘𝑍))) | 
| 117 | 28 | recnd 11289 | . . . . . 6
⊢ (𝜑 → (log‘𝑍) ∈
ℂ) | 
| 118 |  | binom21 14258 | . . . . . 6
⊢
((log‘𝑍)
∈ ℂ → (((log‘𝑍) + 1)↑2) = ((((log‘𝑍)↑2) + (2 ·
(log‘𝑍))) +
1)) | 
| 119 | 117, 118 | syl 17 | . . . . 5
⊢ (𝜑 → (((log‘𝑍) + 1)↑2) =
((((log‘𝑍)↑2) +
(2 · (log‘𝑍)))
+ 1)) | 
| 120 | 117 | sqvald 14183 | . . . . . . 7
⊢ (𝜑 → ((log‘𝑍)↑2) = ((log‘𝑍) · (log‘𝑍))) | 
| 121 |  | df-3 12330 | . . . . . . . . . 10
⊢ 3 = (2 +
1) | 
| 122 | 121 | oveq1i 7441 | . . . . . . . . 9
⊢ (3
· (log‘𝑍)) =
((2 + 1) · (log‘𝑍)) | 
| 123 |  | 2cnd 12344 | . . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℂ) | 
| 124 |  | 1cnd 11256 | . . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) | 
| 125 | 123, 124,
117 | adddird 11286 | . . . . . . . . 9
⊢ (𝜑 → ((2 + 1) ·
(log‘𝑍)) = ((2
· (log‘𝑍)) +
(1 · (log‘𝑍)))) | 
| 126 | 122, 125 | eqtrid 2789 | . . . . . . . 8
⊢ (𝜑 → (3 ·
(log‘𝑍)) = ((2
· (log‘𝑍)) +
(1 · (log‘𝑍)))) | 
| 127 | 117 | mullidd 11279 | . . . . . . . . 9
⊢ (𝜑 → (1 ·
(log‘𝑍)) =
(log‘𝑍)) | 
| 128 | 127 | oveq2d 7447 | . . . . . . . 8
⊢ (𝜑 → ((2 ·
(log‘𝑍)) + (1
· (log‘𝑍))) =
((2 · (log‘𝑍))
+ (log‘𝑍))) | 
| 129 | 126, 128 | eqtr2d 2778 | . . . . . . 7
⊢ (𝜑 → ((2 ·
(log‘𝑍)) +
(log‘𝑍)) = (3
· (log‘𝑍))) | 
| 130 | 120, 129 | oveq12d 7449 | . . . . . 6
⊢ (𝜑 → (((log‘𝑍)↑2) + ((2 ·
(log‘𝑍)) +
(log‘𝑍))) =
(((log‘𝑍) ·
(log‘𝑍)) + (3
· (log‘𝑍)))) | 
| 131 | 117 | sqcld 14184 | . . . . . . 7
⊢ (𝜑 → ((log‘𝑍)↑2) ∈
ℂ) | 
| 132 |  | 2cn 12341 | . . . . . . . 8
⊢ 2 ∈
ℂ | 
| 133 |  | mulcl 11239 | . . . . . . . 8
⊢ ((2
∈ ℂ ∧ (log‘𝑍) ∈ ℂ) → (2 ·
(log‘𝑍)) ∈
ℂ) | 
| 134 | 132, 117,
133 | sylancr 587 | . . . . . . 7
⊢ (𝜑 → (2 ·
(log‘𝑍)) ∈
ℂ) | 
| 135 | 131, 134,
117 | addassd 11283 | . . . . . 6
⊢ (𝜑 → ((((log‘𝑍)↑2) + (2 ·
(log‘𝑍))) +
(log‘𝑍)) =
(((log‘𝑍)↑2) +
((2 · (log‘𝑍))
+ (log‘𝑍)))) | 
| 136 |  | 3cn 12347 | . . . . . . . 8
⊢ 3 ∈
ℂ | 
| 137 | 136 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 3 ∈
ℂ) | 
| 138 | 117, 137,
117 | adddird 11286 | . . . . . 6
⊢ (𝜑 → (((log‘𝑍) + 3) · (log‘𝑍)) = (((log‘𝑍) · (log‘𝑍)) + (3 ·
(log‘𝑍)))) | 
| 139 | 130, 135,
138 | 3eqtr4rd 2788 | . . . . 5
⊢ (𝜑 → (((log‘𝑍) + 3) · (log‘𝑍)) = ((((log‘𝑍)↑2) + (2 ·
(log‘𝑍))) +
(log‘𝑍))) | 
| 140 | 116, 119,
139 | 3brtr4d 5175 | . . . 4
⊢ (𝜑 → (((log‘𝑍) + 1)↑2) ≤
(((log‘𝑍) + 3)
· (log‘𝑍))) | 
| 141 | 10, 31, 35, 99, 140 | letrd 11418 | . . 3
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛)) ≤ (((log‘𝑍) + 3) · (log‘𝑍))) | 
| 142 | 10, 35, 17 | lemul2d 13121 | . . 3
⊢ (𝜑 → ((2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛)) ≤ (((log‘𝑍) + 3) · (log‘𝑍)) ↔ (𝑈 · (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛))) ≤ (𝑈 · (((log‘𝑍) + 3) · (log‘𝑍))))) | 
| 143 | 141, 142 | mpbid 232 | . 2
⊢ (𝜑 → (𝑈 · (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛))) ≤ (𝑈 · (((log‘𝑍) + 3) · (log‘𝑍)))) | 
| 144 | 17 | rpred 13077 | . . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ ℝ) | 
| 145 | 144 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑈 ∈ ℝ) | 
| 146 | 145 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑈 ∈ ℂ) | 
| 147 | 6 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℂ) | 
| 148 | 5 | rpcnne0d 13086 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) | 
| 149 |  | div23 11941 | . . . . . . . 8
⊢ ((𝑈 ∈ ℂ ∧
(log‘𝑛) ∈
ℂ ∧ (𝑛 ∈
ℂ ∧ 𝑛 ≠ 0))
→ ((𝑈 ·
(log‘𝑛)) / 𝑛) = ((𝑈 / 𝑛) · (log‘𝑛))) | 
| 150 |  | divass 11940 | . . . . . . . 8
⊢ ((𝑈 ∈ ℂ ∧
(log‘𝑛) ∈
ℂ ∧ (𝑛 ∈
ℂ ∧ 𝑛 ≠ 0))
→ ((𝑈 ·
(log‘𝑛)) / 𝑛) = (𝑈 · ((log‘𝑛) / 𝑛))) | 
| 151 | 149, 150 | eqtr3d 2779 | . . . . . . 7
⊢ ((𝑈 ∈ ℂ ∧
(log‘𝑛) ∈
ℂ ∧ (𝑛 ∈
ℂ ∧ 𝑛 ≠ 0))
→ ((𝑈 / 𝑛) · (log‘𝑛)) = (𝑈 · ((log‘𝑛) / 𝑛))) | 
| 152 | 146, 147,
148, 151 | syl3anc 1373 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) · (log‘𝑛)) = (𝑈 · ((log‘𝑛) / 𝑛))) | 
| 153 | 152 | sumeq2dv 15738 | . . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(𝑈 · ((log‘𝑛) / 𝑛))) | 
| 154 | 144 | recnd 11289 | . . . . . 6
⊢ (𝜑 → 𝑈 ∈ ℂ) | 
| 155 | 7 | recnd 11289 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((log‘𝑛) / 𝑛) ∈ ℂ) | 
| 156 | 2, 154, 155 | fsummulc2 15820 | . . . . 5
⊢ (𝜑 → (𝑈 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((log‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(𝑈 · ((log‘𝑛) / 𝑛))) | 
| 157 | 153, 156 | eqtr4d 2780 | . . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) = (𝑈 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((log‘𝑛) / 𝑛))) | 
| 158 | 157 | oveq2d 7447 | . . 3
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) = (2 · (𝑈 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((log‘𝑛) / 𝑛)))) | 
| 159 | 8 | recnd 11289 | . . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((log‘𝑛) / 𝑛) ∈ ℂ) | 
| 160 | 123, 154,
159 | mul12d 11470 | . . 3
⊢ (𝜑 → (2 · (𝑈 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛))) = (𝑈 · (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛)))) | 
| 161 | 158, 160 | eqtrd 2777 | . 2
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) = (𝑈 · (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((log‘𝑛) / 𝑛)))) | 
| 162 | 34 | recnd 11289 | . . 3
⊢ (𝜑 → ((log‘𝑍) + 3) ∈
ℂ) | 
| 163 | 154, 162,
117 | mulassd 11284 | . 2
⊢ (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) = (𝑈 · (((log‘𝑍) + 3) · (log‘𝑍)))) | 
| 164 | 143, 161,
163 | 3brtr4d 5175 | 1
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) ≤ ((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍))) |