| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pntlem1.r | . . . . . . . . . 10
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) | 
| 2 |  | pntlem1.a | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℝ+) | 
| 3 |  | pntlem1.b | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈
ℝ+) | 
| 4 |  | pntlem1.l | . . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ (0(,)1)) | 
| 5 |  | pntlem1.d | . . . . . . . . . 10
⊢ 𝐷 = (𝐴 + 1) | 
| 6 |  | pntlem1.f | . . . . . . . . . 10
⊢ 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) | 
| 7 |  | pntlem1.u | . . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈
ℝ+) | 
| 8 |  | pntlem1.u2 | . . . . . . . . . 10
⊢ (𝜑 → 𝑈 ≤ 𝐴) | 
| 9 |  | pntlem1.e | . . . . . . . . . 10
⊢ 𝐸 = (𝑈 / 𝐷) | 
| 10 |  | pntlem1.k | . . . . . . . . . 10
⊢ 𝐾 = (exp‘(𝐵 / 𝐸)) | 
| 11 |  | pntlem1.y | . . . . . . . . . 10
⊢ (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤
𝑌)) | 
| 12 |  | pntlem1.x | . . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋)) | 
| 13 |  | pntlem1.c | . . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈
ℝ+) | 
| 14 |  | pntlem1.w | . . . . . . . . . 10
⊢ 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) | 
| 15 |  | pntlem1.z | . . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝑊[,)+∞)) | 
| 16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | pntlemb 27641 | . . . . . . . . 9
⊢ (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 <
𝑍 ∧ e ≤
(√‘𝑍) ∧
(√‘𝑍) ≤
(𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) | 
| 17 | 16 | simp1d 1143 | . . . . . . . 8
⊢ (𝜑 → 𝑍 ∈
ℝ+) | 
| 18 | 1 | pntrf 27607 | . . . . . . . . 9
⊢ 𝑅:ℝ+⟶ℝ | 
| 19 | 18 | ffvelcdmi 7103 | . . . . . . . 8
⊢ (𝑍 ∈ ℝ+
→ (𝑅‘𝑍) ∈
ℝ) | 
| 20 | 17, 19 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝑅‘𝑍) ∈ ℝ) | 
| 21 | 20, 17 | rerpdivcld 13108 | . . . . . 6
⊢ (𝜑 → ((𝑅‘𝑍) / 𝑍) ∈ ℝ) | 
| 22 | 21 | recnd 11289 | . . . . 5
⊢ (𝜑 → ((𝑅‘𝑍) / 𝑍) ∈ ℂ) | 
| 23 | 22 | abscld 15475 | . . . 4
⊢ (𝜑 → (abs‘((𝑅‘𝑍) / 𝑍)) ∈ ℝ) | 
| 24 | 17 | relogcld 26665 | . . . 4
⊢ (𝜑 → (log‘𝑍) ∈
ℝ) | 
| 25 | 23, 24 | remulcld 11291 | . . 3
⊢ (𝜑 → ((abs‘((𝑅‘𝑍) / 𝑍)) · (log‘𝑍)) ∈ ℝ) | 
| 26 | 7 | rpred 13077 | . . . . . 6
⊢ (𝜑 → 𝑈 ∈ ℝ) | 
| 27 |  | 3re 12346 | . . . . . . . 8
⊢ 3 ∈
ℝ | 
| 28 | 27 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 3 ∈
ℝ) | 
| 29 | 24, 28 | readdcld 11290 | . . . . . 6
⊢ (𝜑 → ((log‘𝑍) + 3) ∈
ℝ) | 
| 30 | 26, 29 | remulcld 11291 | . . . . 5
⊢ (𝜑 → (𝑈 · ((log‘𝑍) + 3)) ∈ ℝ) | 
| 31 |  | 2re 12340 | . . . . . . 7
⊢ 2 ∈
ℝ | 
| 32 | 31 | a1i 11 | . . . . . 6
⊢ (𝜑 → 2 ∈
ℝ) | 
| 33 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | pntlemc 27639 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+
∧ (𝐸 ∈ (0(,)1)
∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+))) | 
| 34 | 33 | simp3d 1145 | . . . . . . . . . 10
⊢ (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+)) | 
| 35 | 34 | simp3d 1145 | . . . . . . . . 9
⊢ (𝜑 → (𝑈 − 𝐸) ∈
ℝ+) | 
| 36 | 35 | rpred 13077 | . . . . . . . 8
⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℝ) | 
| 37 | 1, 2, 3, 4, 5, 6 | pntlemd 27638 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+
∧ 𝐹 ∈
ℝ+)) | 
| 38 | 37 | simp1d 1143 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈
ℝ+) | 
| 39 | 33 | simp1d 1143 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈
ℝ+) | 
| 40 |  | 2z 12649 | . . . . . . . . . . . 12
⊢ 2 ∈
ℤ | 
| 41 |  | rpexpcl 14121 | . . . . . . . . . . . 12
⊢ ((𝐸 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝐸↑2) ∈
ℝ+) | 
| 42 | 39, 40, 41 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐸↑2) ∈
ℝ+) | 
| 43 | 38, 42 | rpmulcld 13093 | . . . . . . . . . 10
⊢ (𝜑 → (𝐿 · (𝐸↑2)) ∈
ℝ+) | 
| 44 |  | 3nn0 12544 | . . . . . . . . . . . . 13
⊢ 3 ∈
ℕ0 | 
| 45 |  | 2nn 12339 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℕ | 
| 46 | 44, 45 | decnncl 12753 | . . . . . . . . . . . 12
⊢ ;32 ∈ ℕ | 
| 47 |  | nnrp 13046 | . . . . . . . . . . . 12
⊢ (;32 ∈ ℕ → ;32 ∈
ℝ+) | 
| 48 | 46, 47 | ax-mp 5 | . . . . . . . . . . 11
⊢ ;32 ∈
ℝ+ | 
| 49 |  | rpmulcl 13058 | . . . . . . . . . . 11
⊢ ((;32 ∈ ℝ+ ∧
𝐵 ∈
ℝ+) → (;32
· 𝐵) ∈
ℝ+) | 
| 50 | 48, 3, 49 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (;32 · 𝐵) ∈
ℝ+) | 
| 51 | 43, 50 | rpdivcld 13094 | . . . . . . . . 9
⊢ (𝜑 → ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) ∈
ℝ+) | 
| 52 | 51 | rpred 13077 | . . . . . . . 8
⊢ (𝜑 → ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) ∈ ℝ) | 
| 53 | 36, 52 | remulcld 11291 | . . . . . . 7
⊢ (𝜑 → ((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) ∈ ℝ) | 
| 54 | 53, 24 | remulcld 11291 | . . . . . 6
⊢ (𝜑 → (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)) ∈ ℝ) | 
| 55 | 32, 54 | remulcld 11291 | . . . . 5
⊢ (𝜑 → (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) ∈ ℝ) | 
| 56 | 30, 55 | resubcld 11691 | . . . 4
⊢ (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) ∈ ℝ) | 
| 57 | 13 | rpred 13077 | . . . 4
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 58 | 56, 57 | readdcld 11290 | . . 3
⊢ (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) + 𝐶) ∈ ℝ) | 
| 59 | 7 | rpcnd 13079 | . . . . . 6
⊢ (𝜑 → 𝑈 ∈ ℂ) | 
| 60 | 53 | recnd 11289 | . . . . . 6
⊢ (𝜑 → ((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) ∈ ℂ) | 
| 61 | 24 | recnd 11289 | . . . . . 6
⊢ (𝜑 → (log‘𝑍) ∈
ℂ) | 
| 62 | 59, 60, 61 | subdird 11720 | . . . . 5
⊢ (𝜑 → ((𝑈 − ((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)))) · (log‘𝑍)) = ((𝑈 · (log‘𝑍)) − (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) | 
| 63 | 38 | rpcnd 13079 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈ ℂ) | 
| 64 | 42 | rpcnd 13079 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) | 
| 65 | 50 | rpcnne0d 13086 | . . . . . . . . . . 11
⊢ (𝜑 → ((;32 · 𝐵) ∈ ℂ ∧ (;32 · 𝐵) ≠ 0)) | 
| 66 |  | div23 11941 | . . . . . . . . . . 11
⊢ ((𝐿 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧
((;32 · 𝐵) ∈ ℂ ∧ (;32 · 𝐵) ≠ 0)) → ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) = ((𝐿 / (;32 · 𝐵)) · (𝐸↑2))) | 
| 67 | 63, 64, 65, 66 | syl3anc 1373 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) = ((𝐿 / (;32 · 𝐵)) · (𝐸↑2))) | 
| 68 | 9 | oveq1i 7441 | . . . . . . . . . . . 12
⊢ (𝐸↑2) = ((𝑈 / 𝐷)↑2) | 
| 69 | 37 | simp2d 1144 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ∈
ℝ+) | 
| 70 | 69 | rpcnd 13079 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ∈ ℂ) | 
| 71 | 69 | rpne0d 13082 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ≠ 0) | 
| 72 | 59, 70, 71 | sqdivd 14199 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑈 / 𝐷)↑2) = ((𝑈↑2) / (𝐷↑2))) | 
| 73 | 68, 72 | eqtrid 2789 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐸↑2) = ((𝑈↑2) / (𝐷↑2))) | 
| 74 | 73 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐿 / (;32 · 𝐵)) · (𝐸↑2)) = ((𝐿 / (;32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2)))) | 
| 75 | 38, 50 | rpdivcld 13094 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 / (;32 · 𝐵)) ∈
ℝ+) | 
| 76 | 75 | rpcnd 13079 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐿 / (;32 · 𝐵)) ∈ ℂ) | 
| 77 | 59 | sqcld 14184 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑈↑2) ∈ ℂ) | 
| 78 |  | rpexpcl 14121 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝐷↑2) ∈
ℝ+) | 
| 79 | 69, 40, 78 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐷↑2) ∈
ℝ+) | 
| 80 | 79 | rpcnne0d 13086 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐷↑2) ∈ ℂ ∧ (𝐷↑2) ≠
0)) | 
| 81 |  | divass 11940 | . . . . . . . . . . . 12
⊢ (((𝐿 / (;32 · 𝐵)) ∈ ℂ ∧ (𝑈↑2) ∈ ℂ ∧ ((𝐷↑2) ∈ ℂ ∧
(𝐷↑2) ≠ 0)) →
(((𝐿 / (;32 · 𝐵)) · (𝑈↑2)) / (𝐷↑2)) = ((𝐿 / (;32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2)))) | 
| 82 |  | div23 11941 | . . . . . . . . . . . 12
⊢ (((𝐿 / (;32 · 𝐵)) ∈ ℂ ∧ (𝑈↑2) ∈ ℂ ∧ ((𝐷↑2) ∈ ℂ ∧
(𝐷↑2) ≠ 0)) →
(((𝐿 / (;32 · 𝐵)) · (𝑈↑2)) / (𝐷↑2)) = (((𝐿 / (;32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))) | 
| 83 | 81, 82 | eqtr3d 2779 | . . . . . . . . . . 11
⊢ (((𝐿 / (;32 · 𝐵)) ∈ ℂ ∧ (𝑈↑2) ∈ ℂ ∧ ((𝐷↑2) ∈ ℂ ∧
(𝐷↑2) ≠ 0)) →
((𝐿 / (;32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2))) = (((𝐿 / (;32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))) | 
| 84 | 76, 77, 80, 83 | syl3anc 1373 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐿 / (;32 · 𝐵)) · ((𝑈↑2) / (𝐷↑2))) = (((𝐿 / (;32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))) | 
| 85 | 67, 74, 84 | 3eqtrd 2781 | . . . . . . . . 9
⊢ (𝜑 → ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) = (((𝐿 / (;32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2))) | 
| 86 | 85 | oveq2d 7447 | . . . . . . . 8
⊢ (𝜑 → ((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) = ((𝑈 − 𝐸) · (((𝐿 / (;32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))) | 
| 87 |  | df-3 12330 | . . . . . . . . . . . . 13
⊢ 3 = (2 +
1) | 
| 88 | 87 | oveq2i 7442 | . . . . . . . . . . . 12
⊢ (𝑈↑3) = (𝑈↑(2 + 1)) | 
| 89 |  | 2nn0 12543 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 | 
| 90 |  | expp1 14109 | . . . . . . . . . . . . 13
⊢ ((𝑈 ∈ ℂ ∧ 2 ∈
ℕ0) → (𝑈↑(2 + 1)) = ((𝑈↑2) · 𝑈)) | 
| 91 | 59, 89, 90 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑈↑(2 + 1)) = ((𝑈↑2) · 𝑈)) | 
| 92 | 88, 91 | eqtrid 2789 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑈↑3) = ((𝑈↑2) · 𝑈)) | 
| 93 | 77, 59 | mulcomd 11282 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑈↑2) · 𝑈) = (𝑈 · (𝑈↑2))) | 
| 94 | 92, 93 | eqtrd 2777 | . . . . . . . . . 10
⊢ (𝜑 → (𝑈↑3) = (𝑈 · (𝑈↑2))) | 
| 95 | 94 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝜑 → (𝐹 · (𝑈↑3)) = (𝐹 · (𝑈 · (𝑈↑2)))) | 
| 96 | 37 | simp3d 1145 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈
ℝ+) | 
| 97 | 96 | rpcnd 13079 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ℂ) | 
| 98 | 97, 59, 77 | mulassd 11284 | . . . . . . . . 9
⊢ (𝜑 → ((𝐹 · 𝑈) · (𝑈↑2)) = (𝐹 · (𝑈 · (𝑈↑2)))) | 
| 99 |  | 1cnd 11256 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℂ) | 
| 100 | 69 | rpreccld 13087 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 / 𝐷) ∈
ℝ+) | 
| 101 | 100 | rpcnd 13079 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 / 𝐷) ∈ ℂ) | 
| 102 | 99, 101, 59 | subdird 11720 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((1 − (1 / 𝐷)) · 𝑈) = ((1 · 𝑈) − ((1 / 𝐷) · 𝑈))) | 
| 103 | 59 | mullidd 11279 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 · 𝑈) = 𝑈) | 
| 104 | 59, 70, 71 | divrec2d 12047 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑈 / 𝐷) = ((1 / 𝐷) · 𝑈)) | 
| 105 | 9, 104 | eqtr2id 2790 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1 / 𝐷) · 𝑈) = 𝐸) | 
| 106 | 103, 105 | oveq12d 7449 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((1 · 𝑈) − ((1 / 𝐷) · 𝑈)) = (𝑈 − 𝐸)) | 
| 107 | 102, 106 | eqtr2d 2778 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑈 − 𝐸) = ((1 − (1 / 𝐷)) · 𝑈)) | 
| 108 | 107 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑈 − 𝐸) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) = (((1 − (1 / 𝐷)) · 𝑈) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2)))) | 
| 109 | 6 | oveq1i 7441 | . . . . . . . . . . . . 13
⊢ (𝐹 · 𝑈) = (((1 − (1 / 𝐷)) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) · 𝑈) | 
| 110 | 99, 101 | subcld 11620 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (1 − (1 / 𝐷)) ∈
ℂ) | 
| 111 | 75, 79 | rpdivcld 13094 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐿 / (;32 · 𝐵)) / (𝐷↑2)) ∈
ℝ+) | 
| 112 | 111 | rpcnd 13079 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐿 / (;32 · 𝐵)) / (𝐷↑2)) ∈ ℂ) | 
| 113 | 110, 112,
59 | mul32d 11471 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((1 − (1 / 𝐷)) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) · 𝑈) = (((1 − (1 / 𝐷)) · 𝑈) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2)))) | 
| 114 | 109, 113 | eqtrid 2789 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 · 𝑈) = (((1 − (1 / 𝐷)) · 𝑈) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2)))) | 
| 115 | 108, 114 | eqtr4d 2780 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑈 − 𝐸) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) = (𝐹 · 𝑈)) | 
| 116 | 115 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝜑 → (((𝑈 − 𝐸) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) · (𝑈↑2)) = ((𝐹 · 𝑈) · (𝑈↑2))) | 
| 117 | 35 | rpcnd 13079 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℂ) | 
| 118 | 117, 112,
77 | mulassd 11284 | . . . . . . . . . 10
⊢ (𝜑 → (((𝑈 − 𝐸) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) · (𝑈↑2)) = ((𝑈 − 𝐸) · (((𝐿 / (;32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))) | 
| 119 | 116, 118 | eqtr3d 2779 | . . . . . . . . 9
⊢ (𝜑 → ((𝐹 · 𝑈) · (𝑈↑2)) = ((𝑈 − 𝐸) · (((𝐿 / (;32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))) | 
| 120 | 95, 98, 119 | 3eqtr2d 2783 | . . . . . . . 8
⊢ (𝜑 → (𝐹 · (𝑈↑3)) = ((𝑈 − 𝐸) · (((𝐿 / (;32 · 𝐵)) / (𝐷↑2)) · (𝑈↑2)))) | 
| 121 | 86, 120 | eqtr4d 2780 | . . . . . . 7
⊢ (𝜑 → ((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) = (𝐹 · (𝑈↑3))) | 
| 122 | 121 | oveq2d 7447 | . . . . . 6
⊢ (𝜑 → (𝑈 − ((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)))) = (𝑈 − (𝐹 · (𝑈↑3)))) | 
| 123 | 122 | oveq1d 7446 | . . . . 5
⊢ (𝜑 → ((𝑈 − ((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)))) · (log‘𝑍)) = ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍))) | 
| 124 | 62, 123 | eqtr3d 2779 | . . . 4
⊢ (𝜑 → ((𝑈 · (log‘𝑍)) − (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) = ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍))) | 
| 125 | 26, 24 | remulcld 11291 | . . . . 5
⊢ (𝜑 → (𝑈 · (log‘𝑍)) ∈ ℝ) | 
| 126 | 125, 54 | resubcld 11691 | . . . 4
⊢ (𝜑 → ((𝑈 · (log‘𝑍)) − (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) ∈ ℝ) | 
| 127 | 124, 126 | eqeltrrd 2842 | . . 3
⊢ (𝜑 → ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)) ∈
ℝ) | 
| 128 | 17 | rpred 13077 | . . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ ℝ) | 
| 129 | 16 | simp2d 1144 | . . . . . . . . 9
⊢ (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌))) | 
| 130 | 129 | simp1d 1143 | . . . . . . . 8
⊢ (𝜑 → 1 < 𝑍) | 
| 131 | 128, 130 | rplogcld 26671 | . . . . . . 7
⊢ (𝜑 → (log‘𝑍) ∈
ℝ+) | 
| 132 | 32, 131 | rerpdivcld 13108 | . . . . . 6
⊢ (𝜑 → (2 / (log‘𝑍)) ∈
ℝ) | 
| 133 |  | fzfid 14014 | . . . . . . 7
⊢ (𝜑 → (1...(⌊‘(𝑍 / 𝑌))) ∈ Fin) | 
| 134 | 17 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ∈
ℝ+) | 
| 135 |  | elfznn 13593 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌))) → 𝑛 ∈
ℕ) | 
| 136 | 135 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℕ) | 
| 137 | 136 | nnrpd 13075 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑛 ∈ ℝ+) | 
| 138 | 134, 137 | rpdivcld 13094 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑍 / 𝑛) ∈
ℝ+) | 
| 139 | 18 | ffvelcdmi 7103 | . . . . . . . . . . . 12
⊢ ((𝑍 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ) | 
| 140 | 138, 139 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑍 / 𝑛)) ∈ ℝ) | 
| 141 | 140, 134 | rerpdivcld 13108 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℝ) | 
| 142 | 141 | recnd 11289 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑅‘(𝑍 / 𝑛)) / 𝑍) ∈ ℂ) | 
| 143 | 142 | abscld 15475 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℝ) | 
| 144 | 137 | relogcld 26665 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℝ) | 
| 145 | 143, 144 | remulcld 11291 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℝ) | 
| 146 | 133, 145 | fsumrecl 15770 | . . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℝ) | 
| 147 | 132, 146 | remulcld 11291 | . . . . 5
⊢ (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ∈ ℝ) | 
| 148 | 147, 57 | readdcld 11290 | . . . 4
⊢ (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶) ∈ ℝ) | 
| 149 | 20 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑅‘𝑍) ∈ ℂ) | 
| 150 | 149 | abscld 15475 | . . . . . . . . . 10
⊢ (𝜑 → (abs‘(𝑅‘𝑍)) ∈ ℝ) | 
| 151 | 150 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → (abs‘(𝑅‘𝑍)) ∈ ℂ) | 
| 152 | 151, 61 | mulcld 11281 | . . . . . . . 8
⊢ (𝜑 → ((abs‘(𝑅‘𝑍)) · (log‘𝑍)) ∈ ℂ) | 
| 153 | 132 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → (2 / (log‘𝑍)) ∈
ℂ) | 
| 154 | 140 | recnd 11289 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑍 / 𝑛)) ∈ ℂ) | 
| 155 | 154 | abscld 15475 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘(𝑅‘(𝑍 / 𝑛))) ∈ ℝ) | 
| 156 | 155, 144 | remulcld 11291 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℝ) | 
| 157 | 133, 156 | fsumrecl 15770 | . . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℝ) | 
| 158 | 157 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℂ) | 
| 159 | 153, 158 | mulcld 11281 | . . . . . . . 8
⊢ (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) ∈ ℂ) | 
| 160 | 17 | rpcnd 13079 | . . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ ℂ) | 
| 161 | 17 | rpne0d 13082 | . . . . . . . 8
⊢ (𝜑 → 𝑍 ≠ 0) | 
| 162 | 152, 159,
160, 161 | divsubdird 12082 | . . . . . . 7
⊢ (𝜑 → ((((abs‘(𝑅‘𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) = ((((abs‘(𝑅‘𝑍)) · (log‘𝑍)) / 𝑍) − (((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍))) | 
| 163 | 151, 61, 160, 161 | div23d 12080 | . . . . . . . . 9
⊢ (𝜑 → (((abs‘(𝑅‘𝑍)) · (log‘𝑍)) / 𝑍) = (((abs‘(𝑅‘𝑍)) / 𝑍) · (log‘𝑍))) | 
| 164 | 149, 160,
161 | absdivd 15494 | . . . . . . . . . . 11
⊢ (𝜑 → (abs‘((𝑅‘𝑍) / 𝑍)) = ((abs‘(𝑅‘𝑍)) / (abs‘𝑍))) | 
| 165 | 17 | rprege0d 13084 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍)) | 
| 166 |  | absid 15335 | . . . . . . . . . . . . 13
⊢ ((𝑍 ∈ ℝ ∧ 0 ≤
𝑍) → (abs‘𝑍) = 𝑍) | 
| 167 | 165, 166 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (abs‘𝑍) = 𝑍) | 
| 168 | 167 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → ((abs‘(𝑅‘𝑍)) / (abs‘𝑍)) = ((abs‘(𝑅‘𝑍)) / 𝑍)) | 
| 169 | 164, 168 | eqtrd 2777 | . . . . . . . . . 10
⊢ (𝜑 → (abs‘((𝑅‘𝑍) / 𝑍)) = ((abs‘(𝑅‘𝑍)) / 𝑍)) | 
| 170 | 169 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝜑 → ((abs‘((𝑅‘𝑍) / 𝑍)) · (log‘𝑍)) = (((abs‘(𝑅‘𝑍)) / 𝑍) · (log‘𝑍))) | 
| 171 | 163, 170 | eqtr4d 2780 | . . . . . . . 8
⊢ (𝜑 → (((abs‘(𝑅‘𝑍)) · (log‘𝑍)) / 𝑍) = ((abs‘((𝑅‘𝑍) / 𝑍)) · (log‘𝑍))) | 
| 172 | 153, 158,
160, 161 | divassd 12078 | . . . . . . . . 9
⊢ (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍) = ((2 / (log‘𝑍)) · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))) | 
| 173 | 160 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ∈ ℂ) | 
| 174 | 161 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑍 ≠ 0) | 
| 175 | 154, 173,
174 | absdivd 15494 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) / (abs‘𝑍))) | 
| 176 | 167 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘𝑍) = 𝑍) | 
| 177 | 176 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑍 / 𝑛))) / (abs‘𝑍)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍)) | 
| 178 | 175, 177 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍)) | 
| 179 | 178 | oveq1d 7446 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = (((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍) · (log‘𝑛))) | 
| 180 | 155 | recnd 11289 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘(𝑅‘(𝑍 / 𝑛))) ∈ ℂ) | 
| 181 | 144 | recnd 11289 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (log‘𝑛) ∈ ℂ) | 
| 182 | 17 | rpcnne0d 13086 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0)) | 
| 183 | 182 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0)) | 
| 184 |  | div23 11941 | . . . . . . . . . . . . . 14
⊢
(((abs‘(𝑅‘(𝑍 / 𝑛))) ∈ ℂ ∧ (log‘𝑛) ∈ ℂ ∧ (𝑍 ∈ ℂ ∧ 𝑍 ≠ 0)) →
(((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍) = (((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍) · (log‘𝑛))) | 
| 185 | 180, 181,
183, 184 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍) = (((abs‘(𝑅‘(𝑍 / 𝑛))) / 𝑍) · (log‘𝑛))) | 
| 186 | 179, 185 | eqtr4d 2780 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = (((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍)) | 
| 187 | 186 | sumeq2dv 15738 | . . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍)) | 
| 188 | 156 | recnd 11289 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) ∈ ℂ) | 
| 189 | 133, 160,
188, 161 | fsumdivc 15822 | . . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍)) | 
| 190 | 187, 189 | eqtr4d 2780 | . . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) = (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍)) | 
| 191 | 190 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) = ((2 / (log‘𝑍)) · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)) / 𝑍))) | 
| 192 | 172, 191 | eqtr4d 2780 | . . . . . . . 8
⊢ (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍) = ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) | 
| 193 | 171, 192 | oveq12d 7449 | . . . . . . 7
⊢ (𝜑 → ((((abs‘(𝑅‘𝑍)) · (log‘𝑍)) / 𝑍) − (((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) / 𝑍)) = (((abs‘((𝑅‘𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))) | 
| 194 | 162, 193 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → ((((abs‘(𝑅‘𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) = (((abs‘((𝑅‘𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))) | 
| 195 |  | 2fveq3 6911 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑍 → (abs‘(𝑅‘𝑧)) = (abs‘(𝑅‘𝑍))) | 
| 196 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑍 → (log‘𝑧) = (log‘𝑍)) | 
| 197 | 195, 196 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑧 = 𝑍 → ((abs‘(𝑅‘𝑧)) · (log‘𝑧)) = ((abs‘(𝑅‘𝑍)) · (log‘𝑍))) | 
| 198 | 196 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑍 → (2 / (log‘𝑧)) = (2 / (log‘𝑍))) | 
| 199 |  | oveq2 7439 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑛 → (𝑧 / 𝑖) = (𝑧 / 𝑛)) | 
| 200 | 199 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑛 → (𝑅‘(𝑧 / 𝑖)) = (𝑅‘(𝑧 / 𝑛))) | 
| 201 | 200 | fveq2d 6910 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (abs‘(𝑅‘(𝑧 / 𝑖))) = (abs‘(𝑅‘(𝑧 / 𝑛)))) | 
| 202 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (log‘𝑖) = (log‘𝑛)) | 
| 203 | 201, 202 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑛 → ((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)) = ((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛))) | 
| 204 | 203 | cbvsumv 15732 | . . . . . . . . . . . 12
⊢
Σ𝑖 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)) = Σ𝑛 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)) | 
| 205 |  | fvoveq1 7454 | . . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑍 → (⌊‘(𝑧 / 𝑌)) = (⌊‘(𝑍 / 𝑌))) | 
| 206 | 205 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ (𝑧 = 𝑍 → (1...(⌊‘(𝑧 / 𝑌))) = (1...(⌊‘(𝑍 / 𝑌)))) | 
| 207 |  | simpl 482 | . . . . . . . . . . . . . . . 16
⊢ ((𝑧 = 𝑍 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑧 = 𝑍) | 
| 208 | 207 | fvoveq1d 7453 | . . . . . . . . . . . . . . 15
⊢ ((𝑧 = 𝑍 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑅‘(𝑧 / 𝑛)) = (𝑅‘(𝑍 / 𝑛))) | 
| 209 | 208 | fveq2d 6910 | . . . . . . . . . . . . . 14
⊢ ((𝑧 = 𝑍 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘(𝑅‘(𝑧 / 𝑛))) = (abs‘(𝑅‘(𝑍 / 𝑛)))) | 
| 210 | 209 | oveq1d 7446 | . . . . . . . . . . . . 13
⊢ ((𝑧 = 𝑍 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)) = ((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) | 
| 211 | 206, 210 | sumeq12rdv 15743 | . . . . . . . . . . . 12
⊢ (𝑧 = 𝑍 → Σ𝑛 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑛))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) | 
| 212 | 204, 211 | eqtrid 2789 | . . . . . . . . . . 11
⊢ (𝑧 = 𝑍 → Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))) | 
| 213 | 198, 212 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑧 = 𝑍 → ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖))) = ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) | 
| 214 | 197, 213 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑧 = 𝑍 → (((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) = (((abs‘(𝑅‘𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛))))) | 
| 215 |  | id 22 | . . . . . . . . 9
⊢ (𝑧 = 𝑍 → 𝑧 = 𝑍) | 
| 216 | 214, 215 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑧 = 𝑍 → ((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) / 𝑧) = ((((abs‘(𝑅‘𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍)) | 
| 217 | 216 | breq1d 5153 | . . . . . . 7
⊢ (𝑧 = 𝑍 → (((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) / 𝑧) ≤ 𝐶 ↔ ((((abs‘(𝑅‘𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) ≤ 𝐶)) | 
| 218 |  | pntlem1.C | . . . . . . 7
⊢ (𝜑 → ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅‘𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈
(1...(⌊‘(𝑧 /
𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) / 𝑧) ≤ 𝐶) | 
| 219 |  | 1re 11261 | . . . . . . . . 9
⊢ 1 ∈
ℝ | 
| 220 |  | rexr 11307 | . . . . . . . . 9
⊢ (1 ∈
ℝ → 1 ∈ ℝ*) | 
| 221 |  | elioopnf 13483 | . . . . . . . . 9
⊢ (1 ∈
ℝ* → (𝑍 ∈ (1(,)+∞) ↔ (𝑍 ∈ ℝ ∧ 1 <
𝑍))) | 
| 222 | 219, 220,
221 | mp2b 10 | . . . . . . . 8
⊢ (𝑍 ∈ (1(,)+∞) ↔
(𝑍 ∈ ℝ ∧ 1
< 𝑍)) | 
| 223 | 128, 130,
222 | sylanbrc 583 | . . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (1(,)+∞)) | 
| 224 | 217, 218,
223 | rspcdva 3623 | . . . . . 6
⊢ (𝜑 → ((((abs‘(𝑅‘𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘(𝑅‘(𝑍 / 𝑛))) · (log‘𝑛)))) / 𝑍) ≤ 𝐶) | 
| 225 | 194, 224 | eqbrtrrd 5167 | . . . . 5
⊢ (𝜑 → (((abs‘((𝑅‘𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ≤ 𝐶) | 
| 226 | 25, 147, 57 | lesubadd2d 11862 | . . . . 5
⊢ (𝜑 → ((((abs‘((𝑅‘𝑍) / 𝑍)) · (log‘𝑍)) − ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ≤ 𝐶 ↔ ((abs‘((𝑅‘𝑍) / 𝑍)) · (log‘𝑍)) ≤ (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶))) | 
| 227 | 225, 226 | mpbid 232 | . . . 4
⊢ (𝜑 → ((abs‘((𝑅‘𝑍) / 𝑍)) · (log‘𝑍)) ≤ (((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶)) | 
| 228 |  | 2cnd 12344 | . . . . . . 7
⊢ (𝜑 → 2 ∈
ℂ) | 
| 229 | 143 | recnd 11289 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) ∈ ℂ) | 
| 230 | 229, 181 | mulcld 11281 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℂ) | 
| 231 | 133, 230 | fsumcl 15769 | . . . . . . 7
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℂ) | 
| 232 | 131 | rpne0d 13082 | . . . . . . 7
⊢ (𝜑 → (log‘𝑍) ≠ 0) | 
| 233 | 228, 231,
61, 232 | div23d 12080 | . . . . . 6
⊢ (𝜑 → ((2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) / (log‘𝑍)) = ((2 / (log‘𝑍)) · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) | 
| 234 | 24 | resqcld 14165 | . . . . . . . . . . . 12
⊢ (𝜑 → ((log‘𝑍)↑2) ∈
ℝ) | 
| 235 | 52, 234 | remulcld 11291 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)) ∈ ℝ) | 
| 236 | 36, 235 | remulcld 11291 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ) | 
| 237 |  | remulcl 11240 | . . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ ((𝑈
− 𝐸) ·
(((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ) → (2
· ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)))) ∈
ℝ) | 
| 238 | 31, 236, 237 | sylancr 587 | . . . . . . . . 9
⊢ (𝜑 → (2 · ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)))) ∈
ℝ) | 
| 239 | 30, 24 | remulcld 11291 | . . . . . . . . 9
⊢ (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) ∈
ℝ) | 
| 240 |  | remulcl 11240 | . . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)) ∈ ℝ) → (2 ·
Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ∈ ℝ) | 
| 241 | 31, 146, 240 | sylancr 587 | . . . . . . . . 9
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ∈ ℝ) | 
| 242 | 26 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → 𝑈 ∈ ℝ) | 
| 243 | 242, 136 | nndivred 12320 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑈 / 𝑛) ∈ ℝ) | 
| 244 | 243, 143 | resubcld 11691 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) ∈ ℝ) | 
| 245 | 244, 144 | remulcld 11291 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) | 
| 246 | 133, 245 | fsumrecl 15770 | . . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ) | 
| 247 | 32, 246 | remulcld 11291 | . . . . . . . . . 10
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ∈ ℝ) | 
| 248 | 239, 241 | resubcld 11691 | . . . . . . . . . 10
⊢ (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 ·
Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ∈ ℝ) | 
| 249 |  | pntlem1.m | . . . . . . . . . . . 12
⊢ 𝑀 =
((⌊‘((log‘𝑋) / (log‘𝐾))) + 1) | 
| 250 |  | pntlem1.n | . . . . . . . . . . . 12
⊢ 𝑁 =
(⌊‘(((log‘𝑍) / (log‘𝐾)) / 2)) | 
| 251 |  | pntlem1.U | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑈) | 
| 252 |  | pntlem1.K | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸)) | 
| 253 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 249, 250, 251, 252 | pntlemf 27649 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) | 
| 254 |  | 2pos 12369 | . . . . . . . . . . . . 13
⊢ 0 <
2 | 
| 255 | 254 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 < 2) | 
| 256 |  | lemul2 12120 | . . . . . . . . . . . 12
⊢ ((((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))) ∈ ℝ ∧
Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → (((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (2 · ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)))) ≤ (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))) | 
| 257 | 236, 246,
32, 255, 256 | syl112anc 1376 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) ↔ (2 · ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)))) ≤ (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))))) | 
| 258 | 253, 257 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → (2 · ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)))) ≤ (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))) | 
| 259 | 243 | recnd 11289 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (𝑈 / 𝑛) ∈ ℂ) | 
| 260 | 259, 229,
181 | subdird 11720 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = (((𝑈 / 𝑛) · (log‘𝑛)) − ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) | 
| 261 | 260 | sumeq2dv 15738 | . . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) · (log‘𝑛)) − ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) | 
| 262 | 243, 144 | remulcld 11291 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℝ) | 
| 263 | 262 | recnd 11289 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))) → ((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℂ) | 
| 264 | 133, 263,
230 | fsumsub 15824 | . . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) · (log‘𝑛)) − ((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) | 
| 265 | 261, 264 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)) = (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) | 
| 266 | 265 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) = (2 · (Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))) | 
| 267 | 133, 262 | fsumrecl 15770 | . . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℝ) | 
| 268 | 267 | recnd 11289 | . . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℂ) | 
| 269 | 228, 268,
231 | subdid 11719 | . . . . . . . . . . . 12
⊢ (𝜑 → (2 · (Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) = ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) − (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))) | 
| 270 | 266, 269 | eqtrd 2777 | . . . . . . . . . . 11
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) = ((2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) − (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))) | 
| 271 |  | remulcl 11240 | . . . . . . . . . . . . 13
⊢ ((2
∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛)) ∈ ℝ) → (2 ·
Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) ∈ ℝ) | 
| 272 | 31, 267, 271 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) ∈ ℝ) | 
| 273 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 249, 250, 251, 252 | pntlemk 27650 | . . . . . . . . . . . 12
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) ≤ ((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍))) | 
| 274 | 272, 239,
241, 273 | lesub1dd 11879 | . . . . . . . . . . 11
⊢ (𝜑 → ((2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) − (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛)))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 ·
Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))) | 
| 275 | 270, 274 | eqbrtrd 5165 | . . . . . . . . . 10
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 ·
Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))) | 
| 276 | 238, 247,
248, 258, 275 | letrd 11418 | . . . . . . . . 9
⊢ (𝜑 → (2 · ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 ·
Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))))) | 
| 277 | 238, 239,
241, 276 | lesubd 11867 | . . . . . . . 8
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)))))) | 
| 278 | 30 | recnd 11289 | . . . . . . . . . 10
⊢ (𝜑 → (𝑈 · ((log‘𝑍) + 3)) ∈ ℂ) | 
| 279 | 55 | recnd 11289 | . . . . . . . . . 10
⊢ (𝜑 → (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) ∈ ℂ) | 
| 280 | 278, 279,
61 | subdird 11720 | . . . . . . . . 9
⊢ (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍)) = (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − ((2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍)))) | 
| 281 | 54 | recnd 11289 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)) ∈ ℂ) | 
| 282 | 228, 281,
61 | mulassd 11284 | . . . . . . . . . . 11
⊢ (𝜑 → ((2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍)) = (2 · ((((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍)))) | 
| 283 | 60, 61, 61 | mulassd 11284 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍)) = (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · ((log‘𝑍) · (log‘𝑍)))) | 
| 284 | 61 | sqvald 14183 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((log‘𝑍)↑2) = ((log‘𝑍) · (log‘𝑍))) | 
| 285 | 284 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · ((log‘𝑍)↑2)) = (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · ((log‘𝑍) · (log‘𝑍)))) | 
| 286 | 51 | rpcnd 13079 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) ∈ ℂ) | 
| 287 | 234 | recnd 11289 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((log‘𝑍)↑2) ∈
ℂ) | 
| 288 | 117, 286,
287 | mulassd 11284 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · ((log‘𝑍)↑2)) = ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)))) | 
| 289 | 283, 285,
288 | 3eqtr2d 2783 | . . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍)) = ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)))) | 
| 290 | 289 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → (2 · ((((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)) · (log‘𝑍))) = (2 · ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))))) | 
| 291 | 282, 290 | eqtrd 2777 | . . . . . . . . . 10
⊢ (𝜑 → ((2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍)) = (2 · ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2))))) | 
| 292 | 291 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − ((2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) · (log‘𝑍))) = (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)))))) | 
| 293 | 280, 292 | eqtrd 2777 | . . . . . . . 8
⊢ (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍)) = (((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)) − (2 · ((𝑈 − 𝐸) · (((𝐿 · (𝐸↑2)) / (;32 · 𝐵)) · ((log‘𝑍)↑2)))))) | 
| 294 | 277, 293 | breqtrrd 5171 | . . . . . . 7
⊢ (𝜑 → (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍))) | 
| 295 | 241, 56, 131 | ledivmul2d 13131 | . . . . . . 7
⊢ (𝜑 → (((2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) / (log‘𝑍)) ≤ ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) ↔ (2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) · (log‘𝑍)))) | 
| 296 | 294, 295 | mpbird 257 | . . . . . 6
⊢ (𝜑 → ((2 · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) / (log‘𝑍)) ≤ ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) | 
| 297 | 233, 296 | eqbrtrrd 5167 | . . . . 5
⊢ (𝜑 → ((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) ≤ ((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) | 
| 298 | 147, 56, 57, 297 | leadd1dd 11877 | . . . 4
⊢ (𝜑 → (((2 / (log‘𝑍)) · Σ𝑛 ∈
(1...(⌊‘(𝑍 /
𝑌)))((abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍)) · (log‘𝑛))) + 𝐶) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) + 𝐶)) | 
| 299 | 25, 148, 58, 227, 298 | letrd 11418 | . . 3
⊢ (𝜑 → ((abs‘((𝑅‘𝑍) / 𝑍)) · (log‘𝑍)) ≤ (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) + 𝐶)) | 
| 300 |  | remulcl 11240 | . . . . . . . . 9
⊢ ((𝑈 ∈ ℝ ∧ 3 ∈
ℝ) → (𝑈 ·
3) ∈ ℝ) | 
| 301 | 26, 27, 300 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → (𝑈 · 3) ∈
ℝ) | 
| 302 | 301, 57 | readdcld 11290 | . . . . . . 7
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) ∈ ℝ) | 
| 303 | 16 | simp3d 1145 | . . . . . . . 8
⊢ (𝜑 → ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) | 
| 304 | 303 | simp3d 1145 | . . . . . . 7
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) | 
| 305 | 302, 54, 125, 304 | leadd2dd 11878 | . . . . . 6
⊢ (𝜑 → ((𝑈 · (log‘𝑍)) + ((𝑈 · 3) + 𝐶)) ≤ ((𝑈 · (log‘𝑍)) + (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) | 
| 306 | 28 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → 3 ∈
ℂ) | 
| 307 | 59, 61, 306 | adddid 11285 | . . . . . . . 8
⊢ (𝜑 → (𝑈 · ((log‘𝑍) + 3)) = ((𝑈 · (log‘𝑍)) + (𝑈 · 3))) | 
| 308 | 307 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) = (((𝑈 · (log‘𝑍)) + (𝑈 · 3)) + 𝐶)) | 
| 309 | 125 | recnd 11289 | . . . . . . . 8
⊢ (𝜑 → (𝑈 · (log‘𝑍)) ∈ ℂ) | 
| 310 | 59, 306 | mulcld 11281 | . . . . . . . 8
⊢ (𝜑 → (𝑈 · 3) ∈
ℂ) | 
| 311 | 13 | rpcnd 13079 | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 312 | 309, 310,
311 | addassd 11283 | . . . . . . 7
⊢ (𝜑 → (((𝑈 · (log‘𝑍)) + (𝑈 · 3)) + 𝐶) = ((𝑈 · (log‘𝑍)) + ((𝑈 · 3) + 𝐶))) | 
| 313 | 308, 312 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) = ((𝑈 · (log‘𝑍)) + ((𝑈 · 3) + 𝐶))) | 
| 314 | 281 | 2timesd 12509 | . . . . . . . 8
⊢ (𝜑 → (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) = ((((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)) + (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) | 
| 315 | 314 | oveq2d 7447 | . . . . . . 7
⊢ (𝜑 → (((𝑈 · (log‘𝑍)) − (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) = (((𝑈 · (log‘𝑍)) − (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) + ((((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)) + (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) | 
| 316 | 309, 281,
281 | nppcan3d 11647 | . . . . . . 7
⊢ (𝜑 → (((𝑈 · (log‘𝑍)) − (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) + ((((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)) + (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) = ((𝑈 · (log‘𝑍)) + (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) | 
| 317 | 315, 316 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → (((𝑈 · (log‘𝑍)) − (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) = ((𝑈 · (log‘𝑍)) + (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) | 
| 318 | 305, 313,
317 | 3brtr4d 5175 | . . . . 5
⊢ (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) ≤ (((𝑈 · (log‘𝑍)) − (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) | 
| 319 | 30, 57 | readdcld 11290 | . . . . . 6
⊢ (𝜑 → ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) ∈ ℝ) | 
| 320 | 319, 55, 126 | lesubaddd 11860 | . . . . 5
⊢ (𝜑 → ((((𝑈 · ((log‘𝑍) + 3)) + 𝐶) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) ≤ ((𝑈 · (log‘𝑍)) − (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) ↔ ((𝑈 · ((log‘𝑍) + 3)) + 𝐶) ≤ (((𝑈 · (log‘𝑍)) − (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) + (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))))) | 
| 321 | 318, 320 | mpbird 257 | . . . 4
⊢ (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) + 𝐶) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) ≤ ((𝑈 · (log‘𝑍)) − (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) | 
| 322 | 278, 311,
279 | addsubd 11641 | . . . 4
⊢ (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) + 𝐶) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) = (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) + 𝐶)) | 
| 323 | 321, 322,
124 | 3brtr3d 5174 | . . 3
⊢ (𝜑 → (((𝑈 · ((log‘𝑍) + 3)) − (2 · (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) + 𝐶) ≤ ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍))) | 
| 324 | 25, 58, 127, 299, 323 | letrd 11418 | . 2
⊢ (𝜑 → ((abs‘((𝑅‘𝑍) / 𝑍)) · (log‘𝑍)) ≤ ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍))) | 
| 325 |  | 3z 12650 | . . . . . . 7
⊢ 3 ∈
ℤ | 
| 326 |  | rpexpcl 14121 | . . . . . . 7
⊢ ((𝑈 ∈ ℝ+
∧ 3 ∈ ℤ) → (𝑈↑3) ∈
ℝ+) | 
| 327 | 7, 325, 326 | sylancl 586 | . . . . . 6
⊢ (𝜑 → (𝑈↑3) ∈
ℝ+) | 
| 328 | 96, 327 | rpmulcld 13093 | . . . . 5
⊢ (𝜑 → (𝐹 · (𝑈↑3)) ∈
ℝ+) | 
| 329 | 328 | rpred 13077 | . . . 4
⊢ (𝜑 → (𝐹 · (𝑈↑3)) ∈ ℝ) | 
| 330 | 26, 329 | resubcld 11691 | . . 3
⊢ (𝜑 → (𝑈 − (𝐹 · (𝑈↑3))) ∈ ℝ) | 
| 331 | 23, 330, 131 | lemul1d 13120 | . 2
⊢ (𝜑 → ((abs‘((𝑅‘𝑍) / 𝑍)) ≤ (𝑈 − (𝐹 · (𝑈↑3))) ↔ ((abs‘((𝑅‘𝑍) / 𝑍)) · (log‘𝑍)) ≤ ((𝑈 − (𝐹 · (𝑈↑3))) · (log‘𝑍)))) | 
| 332 | 324, 331 | mpbird 257 | 1
⊢ (𝜑 → (abs‘((𝑅‘𝑍) / 𝑍)) ≤ (𝑈 − (𝐹 · (𝑈↑3)))) |