Proof of Theorem pntlemb
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pntlem1.z | . . . . 5
⊢ (𝜑 → 𝑍 ∈ (𝑊[,)+∞)) | 
| 2 |  | pntlem1.r | . . . . . . . 8
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) | 
| 3 |  | pntlem1.a | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ+) | 
| 4 |  | pntlem1.b | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ+) | 
| 5 |  | pntlem1.l | . . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (0(,)1)) | 
| 6 |  | pntlem1.d | . . . . . . . 8
⊢ 𝐷 = (𝐴 + 1) | 
| 7 |  | pntlem1.f | . . . . . . . 8
⊢ 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (;32 · 𝐵)) / (𝐷↑2))) | 
| 8 |  | pntlem1.u | . . . . . . . 8
⊢ (𝜑 → 𝑈 ∈
ℝ+) | 
| 9 |  | pntlem1.u2 | . . . . . . . 8
⊢ (𝜑 → 𝑈 ≤ 𝐴) | 
| 10 |  | pntlem1.e | . . . . . . . 8
⊢ 𝐸 = (𝑈 / 𝐷) | 
| 11 |  | pntlem1.k | . . . . . . . 8
⊢ 𝐾 = (exp‘(𝐵 / 𝐸)) | 
| 12 |  | pntlem1.y | . . . . . . . 8
⊢ (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤
𝑌)) | 
| 13 |  | pntlem1.x | . . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋)) | 
| 14 |  | pntlem1.c | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈
ℝ+) | 
| 15 |  | pntlem1.w | . . . . . . . 8
⊢ 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) | 
| 16 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 | pntlema 27640 | . . . . . . 7
⊢ (𝜑 → 𝑊 ∈
ℝ+) | 
| 17 | 16 | rpred 13077 | . . . . . 6
⊢ (𝜑 → 𝑊 ∈ ℝ) | 
| 18 |  | pnfxr 11315 | . . . . . 6
⊢ +∞
∈ ℝ* | 
| 19 |  | elico2 13451 | . . . . . 6
⊢ ((𝑊 ∈ ℝ ∧ +∞
∈ ℝ*) → (𝑍 ∈ (𝑊[,)+∞) ↔ (𝑍 ∈ ℝ ∧ 𝑊 ≤ 𝑍 ∧ 𝑍 < +∞))) | 
| 20 | 17, 18, 19 | sylancl 586 | . . . . 5
⊢ (𝜑 → (𝑍 ∈ (𝑊[,)+∞) ↔ (𝑍 ∈ ℝ ∧ 𝑊 ≤ 𝑍 ∧ 𝑍 < +∞))) | 
| 21 | 1, 20 | mpbid 232 | . . . 4
⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 𝑊 ≤ 𝑍 ∧ 𝑍 < +∞)) | 
| 22 | 21 | simp1d 1143 | . . 3
⊢ (𝜑 → 𝑍 ∈ ℝ) | 
| 23 | 21 | simp2d 1144 | . . 3
⊢ (𝜑 → 𝑊 ≤ 𝑍) | 
| 24 | 22, 16, 23 | rpgecld 13116 | . 2
⊢ (𝜑 → 𝑍 ∈
ℝ+) | 
| 25 |  | 1re 11261 | . . . . . . 7
⊢ 1 ∈
ℝ | 
| 26 | 25 | a1i 11 | . . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) | 
| 27 |  | ere 16125 | . . . . . . 7
⊢ e ∈
ℝ | 
| 28 | 27 | a1i 11 | . . . . . 6
⊢ (𝜑 → e ∈
ℝ) | 
| 29 | 24 | rpsqrtcld 15450 | . . . . . . 7
⊢ (𝜑 → (√‘𝑍) ∈
ℝ+) | 
| 30 | 29 | rpred 13077 | . . . . . 6
⊢ (𝜑 → (√‘𝑍) ∈
ℝ) | 
| 31 |  | 1lt2 12437 | . . . . . . . 8
⊢ 1 <
2 | 
| 32 |  | egt2lt3 16242 | . . . . . . . . 9
⊢ (2 < e
∧ e < 3) | 
| 33 | 32 | simpli 483 | . . . . . . . 8
⊢ 2 <
e | 
| 34 |  | 2re 12340 | . . . . . . . . 9
⊢ 2 ∈
ℝ | 
| 35 | 25, 34, 27 | lttri 11387 | . . . . . . . 8
⊢ ((1 <
2 ∧ 2 < e) → 1 < e) | 
| 36 | 31, 33, 35 | mp2an 692 | . . . . . . 7
⊢ 1 <
e | 
| 37 | 36 | a1i 11 | . . . . . 6
⊢ (𝜑 → 1 < e) | 
| 38 |  | 4re 12350 | . . . . . . . 8
⊢ 4 ∈
ℝ | 
| 39 | 38 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 4 ∈
ℝ) | 
| 40 | 32 | simpri 485 | . . . . . . . . 9
⊢ e <
3 | 
| 41 |  | 3lt4 12440 | . . . . . . . . 9
⊢ 3 <
4 | 
| 42 |  | 3re 12346 | . . . . . . . . . 10
⊢ 3 ∈
ℝ | 
| 43 | 27, 42, 38 | lttri 11387 | . . . . . . . . 9
⊢ ((e <
3 ∧ 3 < 4) → e < 4) | 
| 44 | 40, 41, 43 | mp2an 692 | . . . . . . . 8
⊢ e <
4 | 
| 45 | 44 | a1i 11 | . . . . . . 7
⊢ (𝜑 → e < 4) | 
| 46 |  | 4nn 12349 | . . . . . . . . . . 11
⊢ 4 ∈
ℕ | 
| 47 |  | nnrp 13046 | . . . . . . . . . . 11
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) | 
| 48 | 46, 47 | ax-mp 5 | . . . . . . . . . 10
⊢ 4 ∈
ℝ+ | 
| 49 | 2, 3, 4, 5, 6, 7 | pntlemd 27638 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+
∧ 𝐹 ∈
ℝ+)) | 
| 50 | 49 | simp1d 1143 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈
ℝ+) | 
| 51 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | pntlemc 27639 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+
∧ (𝐸 ∈ (0(,)1)
∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+))) | 
| 52 | 51 | simp1d 1143 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) | 
| 53 | 50, 52 | rpmulcld 13093 | . . . . . . . . . 10
⊢ (𝜑 → (𝐿 · 𝐸) ∈
ℝ+) | 
| 54 |  | rpdivcl 13060 | . . . . . . . . . 10
⊢ ((4
∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (4 /
(𝐿 · 𝐸)) ∈
ℝ+) | 
| 55 | 48, 53, 54 | sylancr 587 | . . . . . . . . 9
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈
ℝ+) | 
| 56 | 55 | rpred 13077 | . . . . . . . 8
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ) | 
| 57 | 53 | rpred 13077 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ) | 
| 58 | 52 | rpred 13077 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 59 | 50 | rpred 13077 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ ℝ) | 
| 60 |  | eliooord 13446 | . . . . . . . . . . . . . . . 16
⊢ (𝐿 ∈ (0(,)1) → (0 <
𝐿 ∧ 𝐿 < 1)) | 
| 61 | 5, 60 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (0 < 𝐿 ∧ 𝐿 < 1)) | 
| 62 | 61 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 < 1) | 
| 63 | 59, 26, 52, 62 | ltmul1dd 13132 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 · 𝐸) < (1 · 𝐸)) | 
| 64 | 52 | rpcnd 13079 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ ℂ) | 
| 65 | 64 | mullidd 11279 | . . . . . . . . . . . . 13
⊢ (𝜑 → (1 · 𝐸) = 𝐸) | 
| 66 | 63, 65 | breqtrd 5169 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 · 𝐸) < 𝐸) | 
| 67 | 51 | simp3d 1145 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈
ℝ+)) | 
| 68 | 67 | simp1d 1143 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) | 
| 69 |  | eliooord 13446 | . . . . . . . . . . . . . 14
⊢ (𝐸 ∈ (0(,)1) → (0 <
𝐸 ∧ 𝐸 < 1)) | 
| 70 | 68, 69 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1)) | 
| 71 | 70 | simprd 495 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 < 1) | 
| 72 | 57, 58, 26, 66, 71 | lttrd 11422 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐿 · 𝐸) < 1) | 
| 73 |  | 4pos 12373 | . . . . . . . . . . . . 13
⊢ 0 <
4 | 
| 74 | 39, 73 | jctir 520 | . . . . . . . . . . . 12
⊢ (𝜑 → (4 ∈ ℝ ∧ 0
< 4)) | 
| 75 |  | ltmul2 12118 | . . . . . . . . . . . 12
⊢ (((𝐿 · 𝐸) ∈ ℝ ∧ 1 ∈ ℝ
∧ (4 ∈ ℝ ∧ 0 < 4)) → ((𝐿 · 𝐸) < 1 ↔ (4 · (𝐿 · 𝐸)) < (4 · 1))) | 
| 76 | 57, 26, 74, 75 | syl3anc 1373 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 · 𝐸) < 1 ↔ (4 · (𝐿 · 𝐸)) < (4 · 1))) | 
| 77 | 72, 76 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → (4 · (𝐿 · 𝐸)) < (4 · 1)) | 
| 78 |  | 4cn 12351 | . . . . . . . . . . 11
⊢ 4 ∈
ℂ | 
| 79 | 78 | mulridi 11265 | . . . . . . . . . 10
⊢ (4
· 1) = 4 | 
| 80 | 77, 79 | breqtrdi 5184 | . . . . . . . . 9
⊢ (𝜑 → (4 · (𝐿 · 𝐸)) < 4) | 
| 81 | 39, 39, 53 | ltmuldivd 13124 | . . . . . . . . 9
⊢ (𝜑 → ((4 · (𝐿 · 𝐸)) < 4 ↔ 4 < (4 / (𝐿 · 𝐸)))) | 
| 82 | 80, 81 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → 4 < (4 / (𝐿 · 𝐸))) | 
| 83 | 12 | simpld 494 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈
ℝ+) | 
| 84 | 83, 55 | rpaddcld 13092 | . . . . . . . . . 10
⊢ (𝜑 → (𝑌 + (4 / (𝐿 · 𝐸))) ∈
ℝ+) | 
| 85 | 84 | rpred 13077 | . . . . . . . . 9
⊢ (𝜑 → (𝑌 + (4 / (𝐿 · 𝐸))) ∈ ℝ) | 
| 86 | 56, 83 | ltaddrp2d 13111 | . . . . . . . . 9
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) < (𝑌 + (4 / (𝐿 · 𝐸)))) | 
| 87 | 85 | resqcld 14165 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) ∈ ℝ) | 
| 88 | 13 | simpld 494 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ∈
ℝ+) | 
| 89 | 51 | simp2d 1144 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐾 ∈
ℝ+) | 
| 90 |  | 2z 12649 | . . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℤ | 
| 91 |  | rpexpcl 14121 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝐾↑2) ∈
ℝ+) | 
| 92 | 89, 90, 91 | sylancl 586 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐾↑2) ∈
ℝ+) | 
| 93 | 88, 92 | rpmulcld 13093 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋 · (𝐾↑2)) ∈
ℝ+) | 
| 94 |  | 4z 12651 | . . . . . . . . . . . . . . . 16
⊢ 4 ∈
ℤ | 
| 95 |  | rpexpcl 14121 | . . . . . . . . . . . . . . . 16
⊢ (((𝑋 · (𝐾↑2)) ∈ ℝ+ ∧ 4
∈ ℤ) → ((𝑋
· (𝐾↑2))↑4) ∈
ℝ+) | 
| 96 | 93, 94, 95 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑋 · (𝐾↑2))↑4) ∈
ℝ+) | 
| 97 |  | 3nn0 12544 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 3 ∈
ℕ0 | 
| 98 |  | 2nn 12339 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℕ | 
| 99 | 97, 98 | decnncl 12753 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ;32 ∈ ℕ | 
| 100 |  | nnrp 13046 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (;32 ∈ ℕ → ;32 ∈
ℝ+) | 
| 101 | 99, 100 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . 20
⊢ ;32 ∈
ℝ+ | 
| 102 |  | rpmulcl 13058 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((;32 ∈ ℝ+ ∧
𝐵 ∈
ℝ+) → (;32
· 𝐵) ∈
ℝ+) | 
| 103 | 101, 4, 102 | sylancr 587 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (;32 · 𝐵) ∈
ℝ+) | 
| 104 | 67 | simp3d 1145 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑈 − 𝐸) ∈
ℝ+) | 
| 105 |  | rpexpcl 14121 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐸 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝐸↑2) ∈
ℝ+) | 
| 106 | 52, 90, 105 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐸↑2) ∈
ℝ+) | 
| 107 | 50, 106 | rpmulcld 13093 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐿 · (𝐸↑2)) ∈
ℝ+) | 
| 108 | 104, 107 | rpmulcld 13093 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ∈
ℝ+) | 
| 109 | 103, 108 | rpdivcld 13094 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) ∈
ℝ+) | 
| 110 |  | 3rp 13040 | . . . . . . . . . . . . . . . . . . . 20
⊢ 3 ∈
ℝ+ | 
| 111 |  | rpmulcl 13058 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 ∈ ℝ+
∧ 3 ∈ ℝ+) → (𝑈 · 3) ∈
ℝ+) | 
| 112 | 8, 110, 111 | sylancl 586 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑈 · 3) ∈
ℝ+) | 
| 113 | 112, 14 | rpaddcld 13092 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) ∈
ℝ+) | 
| 114 | 109, 113 | rpmulcld 13093 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)) ∈
ℝ+) | 
| 115 | 114 | rpred 13077 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)) ∈ ℝ) | 
| 116 | 115 | rpefcld 16141 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) ∈
ℝ+) | 
| 117 | 96, 116 | rpaddcld 13092 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) ∈
ℝ+) | 
| 118 | 87, 117 | ltaddrpd 13110 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) < (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))) | 
| 119 | 118, 15 | breqtrrdi 5185 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) < 𝑊) | 
| 120 | 87, 17, 22, 119, 23 | ltletrd 11421 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) < 𝑍) | 
| 121 | 24 | rprege0d 13084 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍)) | 
| 122 |  | resqrtth 15294 | . . . . . . . . . . . 12
⊢ ((𝑍 ∈ ℝ ∧ 0 ≤
𝑍) →
((√‘𝑍)↑2)
= 𝑍) | 
| 123 | 121, 122 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ((√‘𝑍)↑2) = 𝑍) | 
| 124 | 120, 123 | breqtrrd 5171 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) < ((√‘𝑍)↑2)) | 
| 125 | 84 | rprege0d 13084 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸))) ∈ ℝ ∧ 0 ≤ (𝑌 + (4 / (𝐿 · 𝐸))))) | 
| 126 | 29 | rprege0d 13084 | . . . . . . . . . . 11
⊢ (𝜑 → ((√‘𝑍) ∈ ℝ ∧ 0 ≤
(√‘𝑍))) | 
| 127 |  | lt2sq 14173 | . . . . . . . . . . 11
⊢ ((((𝑌 + (4 / (𝐿 · 𝐸))) ∈ ℝ ∧ 0 ≤ (𝑌 + (4 / (𝐿 · 𝐸)))) ∧ ((√‘𝑍) ∈ ℝ ∧ 0 ≤
(√‘𝑍))) →
((𝑌 + (4 / (𝐿 · 𝐸))) < (√‘𝑍) ↔ ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) < ((√‘𝑍)↑2))) | 
| 128 | 125, 126,
127 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸))) < (√‘𝑍) ↔ ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) < ((√‘𝑍)↑2))) | 
| 129 | 124, 128 | mpbird 257 | . . . . . . . . 9
⊢ (𝜑 → (𝑌 + (4 / (𝐿 · 𝐸))) < (√‘𝑍)) | 
| 130 | 56, 85, 30, 86, 129 | lttrd 11422 | . . . . . . . 8
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) < (√‘𝑍)) | 
| 131 | 39, 56, 30, 82, 130 | lttrd 11422 | . . . . . . 7
⊢ (𝜑 → 4 <
(√‘𝑍)) | 
| 132 | 28, 39, 30, 45, 131 | lttrd 11422 | . . . . . 6
⊢ (𝜑 → e <
(√‘𝑍)) | 
| 133 | 26, 28, 30, 37, 132 | lttrd 11422 | . . . . 5
⊢ (𝜑 → 1 <
(√‘𝑍)) | 
| 134 |  | 0le1 11786 | . . . . . . 7
⊢ 0 ≤
1 | 
| 135 | 134 | a1i 11 | . . . . . 6
⊢ (𝜑 → 0 ≤ 1) | 
| 136 |  | lt2sq 14173 | . . . . . 6
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ ((√‘𝑍) ∈ ℝ ∧ 0 ≤
(√‘𝑍))) →
(1 < (√‘𝑍)
↔ (1↑2) < ((√‘𝑍)↑2))) | 
| 137 | 26, 135, 126, 136 | syl21anc 838 | . . . . 5
⊢ (𝜑 → (1 <
(√‘𝑍) ↔
(1↑2) < ((√‘𝑍)↑2))) | 
| 138 | 133, 137 | mpbid 232 | . . . 4
⊢ (𝜑 → (1↑2) <
((√‘𝑍)↑2)) | 
| 139 |  | sq1 14234 | . . . . 5
⊢
(1↑2) = 1 | 
| 140 | 139 | a1i 11 | . . . 4
⊢ (𝜑 → (1↑2) =
1) | 
| 141 | 138, 140,
123 | 3brtr3d 5174 | . . 3
⊢ (𝜑 → 1 < 𝑍) | 
| 142 | 28, 30, 132 | ltled 11409 | . . 3
⊢ (𝜑 → e ≤
(√‘𝑍)) | 
| 143 | 22, 83 | rerpdivcld 13108 | . . . 4
⊢ (𝜑 → (𝑍 / 𝑌) ∈ ℝ) | 
| 144 | 83 | rpred 13077 | . . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 145 | 144, 55 | ltaddrpd 13110 | . . . . . . . 8
⊢ (𝜑 → 𝑌 < (𝑌 + (4 / (𝐿 · 𝐸)))) | 
| 146 | 144, 85, 30, 145, 129 | lttrd 11422 | . . . . . . 7
⊢ (𝜑 → 𝑌 < (√‘𝑍)) | 
| 147 | 144, 30, 29, 146 | ltmul2dd 13133 | . . . . . 6
⊢ (𝜑 → ((√‘𝑍) · 𝑌) < ((√‘𝑍) · (√‘𝑍))) | 
| 148 |  | remsqsqrt 15295 | . . . . . . 7
⊢ ((𝑍 ∈ ℝ ∧ 0 ≤
𝑍) →
((√‘𝑍) ·
(√‘𝑍)) = 𝑍) | 
| 149 | 121, 148 | syl 17 | . . . . . 6
⊢ (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍) | 
| 150 | 147, 149 | breqtrd 5169 | . . . . 5
⊢ (𝜑 → ((√‘𝑍) · 𝑌) < 𝑍) | 
| 151 | 30, 22, 83 | ltmuldivd 13124 | . . . . 5
⊢ (𝜑 → (((√‘𝑍) · 𝑌) < 𝑍 ↔ (√‘𝑍) < (𝑍 / 𝑌))) | 
| 152 | 150, 151 | mpbid 232 | . . . 4
⊢ (𝜑 → (√‘𝑍) < (𝑍 / 𝑌)) | 
| 153 | 30, 143, 152 | ltled 11409 | . . 3
⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / 𝑌)) | 
| 154 | 141, 142,
153 | 3jca 1129 | . 2
⊢ (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌))) | 
| 155 | 56, 30, 130 | ltled 11409 | . . 3
⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (√‘𝑍)) | 
| 156 | 88 | relogcld 26665 | . . . . . 6
⊢ (𝜑 → (log‘𝑋) ∈
ℝ) | 
| 157 | 89 | rpred 13077 | . . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℝ) | 
| 158 | 67 | simp2d 1144 | . . . . . . 7
⊢ (𝜑 → 1 < 𝐾) | 
| 159 | 157, 158 | rplogcld 26671 | . . . . . 6
⊢ (𝜑 → (log‘𝐾) ∈
ℝ+) | 
| 160 | 156, 159 | rerpdivcld 13108 | . . . . 5
⊢ (𝜑 → ((log‘𝑋) / (log‘𝐾)) ∈ ℝ) | 
| 161 |  | readdcl 11238 | . . . . 5
⊢
((((log‘𝑋) /
(log‘𝐾)) ∈
ℝ ∧ 2 ∈ ℝ) → (((log‘𝑋) / (log‘𝐾)) + 2) ∈ ℝ) | 
| 162 | 160, 34, 161 | sylancl 586 | . . . 4
⊢ (𝜑 → (((log‘𝑋) / (log‘𝐾)) + 2) ∈ ℝ) | 
| 163 | 24 | relogcld 26665 | . . . . . 6
⊢ (𝜑 → (log‘𝑍) ∈
ℝ) | 
| 164 | 163, 159 | rerpdivcld 13108 | . . . . 5
⊢ (𝜑 → ((log‘𝑍) / (log‘𝐾)) ∈ ℝ) | 
| 165 |  | nndivre 12307 | . . . . 5
⊢
((((log‘𝑍) /
(log‘𝐾)) ∈
ℝ ∧ 4 ∈ ℕ) → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℝ) | 
| 166 | 164, 46, 165 | sylancl 586 | . . . 4
⊢ (𝜑 → (((log‘𝑍) / (log‘𝐾)) / 4) ∈ ℝ) | 
| 167 | 93 | relogcld 26665 | . . . . . 6
⊢ (𝜑 → (log‘(𝑋 · (𝐾↑2))) ∈ ℝ) | 
| 168 |  | nndivre 12307 | . . . . . . 7
⊢
(((log‘𝑍)
∈ ℝ ∧ 4 ∈ ℕ) → ((log‘𝑍) / 4) ∈ ℝ) | 
| 169 | 163, 46, 168 | sylancl 586 | . . . . . 6
⊢ (𝜑 → ((log‘𝑍) / 4) ∈
ℝ) | 
| 170 |  | relogexp 26638 | . . . . . . . . 9
⊢ (((𝑋 · (𝐾↑2)) ∈ ℝ+ ∧ 4
∈ ℤ) → (log‘((𝑋 · (𝐾↑2))↑4)) = (4 ·
(log‘(𝑋 ·
(𝐾↑2))))) | 
| 171 | 93, 94, 170 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → (log‘((𝑋 · (𝐾↑2))↑4)) = (4 ·
(log‘(𝑋 ·
(𝐾↑2))))) | 
| 172 | 96 | rpred 13077 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑋 · (𝐾↑2))↑4) ∈
ℝ) | 
| 173 | 117 | rpred 13077 | . . . . . . . . . 10
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) ∈ ℝ) | 
| 174 | 172, 116 | ltaddrpd 13110 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑋 · (𝐾↑2))↑4) < (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) | 
| 175 |  | rpexpcl 14121 | . . . . . . . . . . . . . 14
⊢ (((𝑌 + (4 / (𝐿 · 𝐸))) ∈ ℝ+ ∧ 2
∈ ℤ) → ((𝑌
+ (4 / (𝐿 · 𝐸)))↑2) ∈
ℝ+) | 
| 176 | 84, 90, 175 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) ∈
ℝ+) | 
| 177 | 173, 176 | ltaddrpd 13110 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) < ((((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) + ((𝑌 + (4 / (𝐿 · 𝐸)))↑2))) | 
| 178 | 87 | recnd 11289 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 + (4 / (𝐿 · 𝐸)))↑2) ∈ ℂ) | 
| 179 | 117 | rpcnd 13079 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) ∈ ℂ) | 
| 180 | 178, 179 | addcomd 11463 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) = ((((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) + ((𝑌 + (4 / (𝐿 · 𝐸)))↑2))) | 
| 181 | 15, 180 | eqtrid 2789 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 = ((((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) + ((𝑌 + (4 / (𝐿 · 𝐸)))↑2))) | 
| 182 | 177, 181 | breqtrrd 5171 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) < 𝑊) | 
| 183 | 173, 17, 22, 182, 23 | ltletrd 11421 | . . . . . . . . . 10
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))) < 𝑍) | 
| 184 | 172, 173,
22, 174, 183 | lttrd 11422 | . . . . . . . . 9
⊢ (𝜑 → ((𝑋 · (𝐾↑2))↑4) < 𝑍) | 
| 185 |  | logltb 26642 | . . . . . . . . . 10
⊢ ((((𝑋 · (𝐾↑2))↑4) ∈ ℝ+
∧ 𝑍 ∈
ℝ+) → (((𝑋 · (𝐾↑2))↑4) < 𝑍 ↔ (log‘((𝑋 · (𝐾↑2))↑4)) < (log‘𝑍))) | 
| 186 | 96, 24, 185 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (((𝑋 · (𝐾↑2))↑4) < 𝑍 ↔ (log‘((𝑋 · (𝐾↑2))↑4)) < (log‘𝑍))) | 
| 187 | 184, 186 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → (log‘((𝑋 · (𝐾↑2))↑4)) < (log‘𝑍)) | 
| 188 | 171, 187 | eqbrtrrd 5167 | . . . . . . 7
⊢ (𝜑 → (4 ·
(log‘(𝑋 ·
(𝐾↑2)))) <
(log‘𝑍)) | 
| 189 |  | ltmuldiv2 12142 | . . . . . . . 8
⊢
(((log‘(𝑋
· (𝐾↑2)))
∈ ℝ ∧ (log‘𝑍) ∈ ℝ ∧ (4 ∈ ℝ
∧ 0 < 4)) → ((4 · (log‘(𝑋 · (𝐾↑2)))) < (log‘𝑍) ↔ (log‘(𝑋 · (𝐾↑2))) < ((log‘𝑍) / 4))) | 
| 190 | 167, 163,
74, 189 | syl3anc 1373 | . . . . . . 7
⊢ (𝜑 → ((4 ·
(log‘(𝑋 ·
(𝐾↑2)))) <
(log‘𝑍) ↔
(log‘(𝑋 ·
(𝐾↑2))) <
((log‘𝑍) /
4))) | 
| 191 | 188, 190 | mpbid 232 | . . . . . 6
⊢ (𝜑 → (log‘(𝑋 · (𝐾↑2))) < ((log‘𝑍) / 4)) | 
| 192 | 167, 169,
159, 191 | ltdiv1dd 13134 | . . . . 5
⊢ (𝜑 → ((log‘(𝑋 · (𝐾↑2))) / (log‘𝐾)) < (((log‘𝑍) / 4) / (log‘𝐾))) | 
| 193 | 88, 92 | relogmuld 26667 | . . . . . . . 8
⊢ (𝜑 → (log‘(𝑋 · (𝐾↑2))) = ((log‘𝑋) + (log‘(𝐾↑2)))) | 
| 194 |  | relogexp 26638 | . . . . . . . . . 10
⊢ ((𝐾 ∈ ℝ+
∧ 2 ∈ ℤ) → (log‘(𝐾↑2)) = (2 · (log‘𝐾))) | 
| 195 | 89, 90, 194 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → (log‘(𝐾↑2)) = (2 ·
(log‘𝐾))) | 
| 196 | 195 | oveq2d 7447 | . . . . . . . 8
⊢ (𝜑 → ((log‘𝑋) + (log‘(𝐾↑2))) = ((log‘𝑋) + (2 · (log‘𝐾)))) | 
| 197 | 193, 196 | eqtrd 2777 | . . . . . . 7
⊢ (𝜑 → (log‘(𝑋 · (𝐾↑2))) = ((log‘𝑋) + (2 · (log‘𝐾)))) | 
| 198 | 197 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 → ((log‘(𝑋 · (𝐾↑2))) / (log‘𝐾)) = (((log‘𝑋) + (2 · (log‘𝐾))) / (log‘𝐾))) | 
| 199 | 156 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → (log‘𝑋) ∈
ℂ) | 
| 200 |  | 2cnd 12344 | . . . . . . . 8
⊢ (𝜑 → 2 ∈
ℂ) | 
| 201 | 159 | rpcnd 13079 | . . . . . . . 8
⊢ (𝜑 → (log‘𝐾) ∈
ℂ) | 
| 202 | 200, 201 | mulcld 11281 | . . . . . . 7
⊢ (𝜑 → (2 ·
(log‘𝐾)) ∈
ℂ) | 
| 203 | 159 | rpcnne0d 13086 | . . . . . . 7
⊢ (𝜑 → ((log‘𝐾) ∈ ℂ ∧
(log‘𝐾) ≠
0)) | 
| 204 |  | divdir 11947 | . . . . . . 7
⊢
(((log‘𝑋)
∈ ℂ ∧ (2 · (log‘𝐾)) ∈ ℂ ∧ ((log‘𝐾) ∈ ℂ ∧
(log‘𝐾) ≠ 0))
→ (((log‘𝑋) + (2
· (log‘𝐾))) /
(log‘𝐾)) =
(((log‘𝑋) /
(log‘𝐾)) + ((2
· (log‘𝐾)) /
(log‘𝐾)))) | 
| 205 | 199, 202,
203, 204 | syl3anc 1373 | . . . . . 6
⊢ (𝜑 → (((log‘𝑋) + (2 · (log‘𝐾))) / (log‘𝐾)) = (((log‘𝑋) / (log‘𝐾)) + ((2 · (log‘𝐾)) / (log‘𝐾)))) | 
| 206 | 203 | simprd 495 | . . . . . . . 8
⊢ (𝜑 → (log‘𝐾) ≠ 0) | 
| 207 | 200, 201,
206 | divcan4d 12049 | . . . . . . 7
⊢ (𝜑 → ((2 ·
(log‘𝐾)) /
(log‘𝐾)) =
2) | 
| 208 | 207 | oveq2d 7447 | . . . . . 6
⊢ (𝜑 → (((log‘𝑋) / (log‘𝐾)) + ((2 · (log‘𝐾)) / (log‘𝐾))) = (((log‘𝑋) / (log‘𝐾)) + 2)) | 
| 209 | 198, 205,
208 | 3eqtrd 2781 | . . . . 5
⊢ (𝜑 → ((log‘(𝑋 · (𝐾↑2))) / (log‘𝐾)) = (((log‘𝑋) / (log‘𝐾)) + 2)) | 
| 210 | 163 | recnd 11289 | . . . . . 6
⊢ (𝜑 → (log‘𝑍) ∈
ℂ) | 
| 211 |  | rpcnne0 13053 | . . . . . . 7
⊢ (4 ∈
ℝ+ → (4 ∈ ℂ ∧ 4 ≠ 0)) | 
| 212 | 48, 211 | mp1i 13 | . . . . . 6
⊢ (𝜑 → (4 ∈ ℂ ∧ 4
≠ 0)) | 
| 213 |  | divdiv32 11975 | . . . . . 6
⊢
(((log‘𝑍)
∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ ((log‘𝐾) ∈ ℂ ∧
(log‘𝐾) ≠ 0))
→ (((log‘𝑍) / 4)
/ (log‘𝐾)) =
(((log‘𝑍) /
(log‘𝐾)) /
4)) | 
| 214 | 210, 212,
203, 213 | syl3anc 1373 | . . . . 5
⊢ (𝜑 → (((log‘𝑍) / 4) / (log‘𝐾)) = (((log‘𝑍) / (log‘𝐾)) / 4)) | 
| 215 | 192, 209,
214 | 3brtr3d 5174 | . . . 4
⊢ (𝜑 → (((log‘𝑋) / (log‘𝐾)) + 2) < (((log‘𝑍) / (log‘𝐾)) / 4)) | 
| 216 | 162, 166,
215 | ltled 11409 | . . 3
⊢ (𝜑 → (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4)) | 
| 217 | 113 | rpred 13077 | . . . . 5
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) ∈ ℝ) | 
| 218 | 108, 103 | rpdivcld 13094 | . . . . . . 7
⊢ (𝜑 → (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) ∈
ℝ+) | 
| 219 | 218 | rpred 13077 | . . . . . 6
⊢ (𝜑 → (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) ∈ ℝ) | 
| 220 | 219, 163 | remulcld 11291 | . . . . 5
⊢ (𝜑 → ((((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) · (log‘𝑍)) ∈ ℝ) | 
| 221 | 113 | rpcnd 13079 | . . . . . . . . 9
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) ∈ ℂ) | 
| 222 | 108 | rpcnne0d 13086 | . . . . . . . . 9
⊢ (𝜑 → (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ∈ ℂ ∧ ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ≠ 0)) | 
| 223 | 103 | rpcnne0d 13086 | . . . . . . . . 9
⊢ (𝜑 → ((;32 · 𝐵) ∈ ℂ ∧ (;32 · 𝐵) ≠ 0)) | 
| 224 |  | divdiv2 11979 | . . . . . . . . 9
⊢ ((((𝑈 · 3) + 𝐶) ∈ ℂ ∧ (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ∈ ℂ ∧ ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ≠ 0) ∧ ((;32 · 𝐵) ∈ ℂ ∧ (;32 · 𝐵) ≠ 0)) → (((𝑈 · 3) + 𝐶) / (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵))) = ((((𝑈 · 3) + 𝐶) · (;32 · 𝐵)) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))))) | 
| 225 | 221, 222,
223, 224 | syl3anc 1373 | . . . . . . . 8
⊢ (𝜑 → (((𝑈 · 3) + 𝐶) / (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵))) = ((((𝑈 · 3) + 𝐶) · (;32 · 𝐵)) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))))) | 
| 226 | 103 | rpcnd 13079 | . . . . . . . . . 10
⊢ (𝜑 → (;32 · 𝐵) ∈ ℂ) | 
| 227 | 221, 226 | mulcomd 11282 | . . . . . . . . 9
⊢ (𝜑 → (((𝑈 · 3) + 𝐶) · (;32 · 𝐵)) = ((;32 · 𝐵) · ((𝑈 · 3) + 𝐶))) | 
| 228 | 227 | oveq1d 7446 | . . . . . . . 8
⊢ (𝜑 → ((((𝑈 · 3) + 𝐶) · (;32 · 𝐵)) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) = (((;32 · 𝐵) · ((𝑈 · 3) + 𝐶)) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))))) | 
| 229 |  | div23 11941 | . . . . . . . . 9
⊢ (((;32 · 𝐵) ∈ ℂ ∧ ((𝑈 · 3) + 𝐶) ∈ ℂ ∧ (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ∈ ℂ ∧ ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) ≠ 0)) → (((;32 · 𝐵) · ((𝑈 · 3) + 𝐶)) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) = (((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) | 
| 230 | 226, 221,
222, 229 | syl3anc 1373 | . . . . . . . 8
⊢ (𝜑 → (((;32 · 𝐵) · ((𝑈 · 3) + 𝐶)) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) = (((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) | 
| 231 | 225, 228,
230 | 3eqtrd 2781 | . . . . . . 7
⊢ (𝜑 → (((𝑈 · 3) + 𝐶) / (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵))) = (((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) | 
| 232 | 115 | reefcld 16124 | . . . . . . . . . 10
⊢ (𝜑 → (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) ∈ ℝ) | 
| 233 | 232, 96 | ltaddrp2d 13111 | . . . . . . . . . 10
⊢ (𝜑 → (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) < (((𝑋 · (𝐾↑2))↑4) + (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))))) | 
| 234 | 232, 173,
22, 233, 183 | lttrd 11422 | . . . . . . . . 9
⊢ (𝜑 → (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) < 𝑍) | 
| 235 | 24 | reeflogd 26666 | . . . . . . . . 9
⊢ (𝜑 →
(exp‘(log‘𝑍)) =
𝑍) | 
| 236 | 234, 235 | breqtrrd 5171 | . . . . . . . 8
⊢ (𝜑 → (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) < (exp‘(log‘𝑍))) | 
| 237 |  | eflt 16153 | . . . . . . . . 9
⊢
(((((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)) ∈ ℝ ∧ (log‘𝑍) ∈ ℝ) →
((((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)) < (log‘𝑍) ↔ (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) < (exp‘(log‘𝑍)))) | 
| 238 | 115, 163,
237 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → ((((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)) < (log‘𝑍) ↔ (exp‘(((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶))) < (exp‘(log‘𝑍)))) | 
| 239 | 236, 238 | mpbird 257 | . . . . . . 7
⊢ (𝜑 → (((;32 · 𝐵) / ((𝑈 − 𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)) < (log‘𝑍)) | 
| 240 | 231, 239 | eqbrtrd 5165 | . . . . . 6
⊢ (𝜑 → (((𝑈 · 3) + 𝐶) / (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵))) < (log‘𝑍)) | 
| 241 | 217, 163,
218 | ltdivmuld 13128 | . . . . . 6
⊢ (𝜑 → ((((𝑈 · 3) + 𝐶) / (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵))) < (log‘𝑍) ↔ ((𝑈 · 3) + 𝐶) < ((((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) · (log‘𝑍)))) | 
| 242 | 240, 241 | mpbid 232 | . . . . 5
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) < ((((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) · (log‘𝑍))) | 
| 243 | 217, 220,
242 | ltled 11409 | . . . 4
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) ≤ ((((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) · (log‘𝑍))) | 
| 244 | 104 | rpcnd 13079 | . . . . . 6
⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℂ) | 
| 245 | 107 | rpcnd 13079 | . . . . . 6
⊢ (𝜑 → (𝐿 · (𝐸↑2)) ∈ ℂ) | 
| 246 |  | divass 11940 | . . . . . 6
⊢ (((𝑈 − 𝐸) ∈ ℂ ∧ (𝐿 · (𝐸↑2)) ∈ ℂ ∧ ((;32 · 𝐵) ∈ ℂ ∧ (;32 · 𝐵) ≠ 0)) → (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) = ((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)))) | 
| 247 | 244, 245,
223, 246 | syl3anc 1373 | . . . . 5
⊢ (𝜑 → (((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) = ((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵)))) | 
| 248 | 247 | oveq1d 7446 | . . . 4
⊢ (𝜑 → ((((𝑈 − 𝐸) · (𝐿 · (𝐸↑2))) / (;32 · 𝐵)) · (log‘𝑍)) = (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) | 
| 249 | 243, 248 | breqtrd 5169 | . . 3
⊢ (𝜑 → ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))) | 
| 250 | 155, 216,
249 | 3jca 1129 | . 2
⊢ (𝜑 → ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))) | 
| 251 | 24, 154, 250 | 3jca 1129 | 1
⊢ (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 <
𝑍 ∧ e ≤
(√‘𝑍) ∧
(√‘𝑍) ≤
(𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))) |