Metamath Proof Explorer

Theorem pntlemb

Description: Lemma for pnt . Unpack all the lower bounds contained in W , in the form they will be used. For comparison with Equation 10.6.27 of Shapiro, p. 434, Z is x. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Hypotheses pntlem1.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
pntlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
pntlem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
pntlem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
pntlem1.d ⊢ 𝐷 = ( 𝐴 + 1 )
pntlem1.f ⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
pntlem1.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
pntlem1.u2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
pntlem1.e ⊢ 𝐸 = ( 𝑈 / 𝐷 )
pntlem1.k ⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
pntlem1.y ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
pntlem1.x ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋 ) )
pntlem1.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
pntlem1.w ⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
pntlem1.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 [,) +∞ ) )
Assertion pntlemb ( 𝜑 → ( 𝑍 ∈ ℝ+ ∧ ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) ∧ ( ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) ∧ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pntlem1.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2 pntlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3 pntlem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
4 pntlem1.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
5 pntlem1.d ⊢ 𝐷 = ( 𝐴 + 1 )
6 pntlem1.f ⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
7 pntlem1.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
8 pntlem1.u2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
9 pntlem1.e ⊢ 𝐸 = ( 𝑈 / 𝐷 )
10 pntlem1.k ⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
11 pntlem1.y ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
12 pntlem1.x ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋 ) )
13 pntlem1.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
14 pntlem1.w ⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
15 pntlem1.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 [,) +∞ ) )
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 pntlema ⊢ ( 𝜑 → 𝑊 ∈ ℝ+ )
17 16 rpred ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
18 pnfxr ⊢ +∞ ∈ ℝ*
19 elico2 ⊢ ( ( 𝑊 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 𝑍 ∈ ( 𝑊 [,) +∞ ) ↔ ( 𝑍 ∈ ℝ ∧ 𝑊 ≤ 𝑍 ∧ 𝑍 < +∞ ) ) )
20 17 18 19 sylancl ⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑊 [,) +∞ ) ↔ ( 𝑍 ∈ ℝ ∧ 𝑊 ≤ 𝑍 ∧ 𝑍 < +∞ ) ) )
21 15 20 mpbid ⊢ ( 𝜑 → ( 𝑍 ∈ ℝ ∧ 𝑊 ≤ 𝑍 ∧ 𝑍 < +∞ ) )
22 21 simp1d ⊢ ( 𝜑 → 𝑍 ∈ ℝ )
23 21 simp2d ⊢ ( 𝜑 → 𝑊 ≤ 𝑍 )
24 22 16 23 rpgecld ⊢ ( 𝜑 → 𝑍 ∈ ℝ+ )
25 1re ⊢ 1 ∈ ℝ
26 25 a1i ⊢ ( 𝜑 → 1 ∈ ℝ )
27 ere ⊢ e ∈ ℝ
28 27 a1i ⊢ ( 𝜑 → e ∈ ℝ )
29 24 rpsqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ∈ ℝ+ )
30 29 rpred ⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ∈ ℝ )
31 1lt2 ⊢ 1 < 2
32 egt2lt3 ⊢ ( 2 < e ∧ e < 3 )
33 32 simpli ⊢ 2 < e
34 2re ⊢ 2 ∈ ℝ
35 25 34 27 lttri ⊢ ( ( 1 < 2 ∧ 2 < e ) → 1 < e )
36 31 33 35 mp2an ⊢ 1 < e
37 36 a1i ⊢ ( 𝜑 → 1 < e )
38 4re ⊢ 4 ∈ ℝ
39 38 a1i ⊢ ( 𝜑 → 4 ∈ ℝ )
40 32 simpri ⊢ e < 3
41 3lt4 ⊢ 3 < 4
42 3re ⊢ 3 ∈ ℝ
43 27 42 38 lttri ⊢ ( ( e < 3 ∧ 3 < 4 ) → e < 4 )
44 40 41 43 mp2an ⊢ e < 4
45 44 a1i ⊢ ( 𝜑 → e < 4 )
46 4nn ⊢ 4 ∈ ℕ
47 nnrp ⊢ ( 4 ∈ ℕ → 4 ∈ ℝ+ )
48 46 47 ax-mp ⊢ 4 ∈ ℝ+
49 1 2 3 4 5 6 pntlemd ⊢ ( 𝜑 → ( 𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ∧ 𝐹 ∈ ℝ+ ) )
50 49 simp1d ⊢ ( 𝜑 → 𝐿 ∈ ℝ+ )
51 1 2 3 4 5 6 7 8 9 10 pntlemc ⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )
52 51 simp1d ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
53 50 52 rpmulcld ⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℝ+ )
54 rpdivcl ⊢ ( ( 4 ∈ ℝ+ ∧ ( 𝐿 · 𝐸 ) ∈ ℝ+ ) → ( 4 / ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
55 48 53 54 sylancr ⊢ ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
56 55 rpred ⊢ ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ∈ ℝ )
57 53 rpred ⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℝ )
58 52 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
59 50 rpred ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
60 eliooord ⊢ ( 𝐿 ∈ ( 0 (,) 1 ) → ( 0 < 𝐿 ∧ 𝐿 < 1 ) )
61 4 60 syl ⊢ ( 𝜑 → ( 0 < 𝐿 ∧ 𝐿 < 1 ) )
62 61 simprd ⊢ ( 𝜑 → 𝐿 < 1 )
63 59 26 52 62 ltmul1dd ⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) < ( 1 · 𝐸 ) )
64 52 rpcnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
65 64 mullidd ⊢ ( 𝜑 → ( 1 · 𝐸 ) = 𝐸 )
66 63 65 breqtrd ⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) < 𝐸 )
67 51 simp3d ⊢ ( 𝜑 → ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
68 67 simp1d ⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
69 eliooord ⊢ ( 𝐸 ∈ ( 0 (,) 1 ) → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
70 68 69 syl ⊢ ( 𝜑 → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
71 70 simprd ⊢ ( 𝜑 → 𝐸 < 1 )
72 57 58 26 66 71 lttrd ⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) < 1 )
73 4pos ⊢ 0 < 4
74 39 73 jctir ⊢ ( 𝜑 → ( 4 ∈ ℝ ∧ 0 < 4 ) )
75 ltmul2 ⊢ ( ( ( 𝐿 · 𝐸 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 4 ∈ ℝ ∧ 0 < 4 ) ) → ( ( 𝐿 · 𝐸 ) < 1 ↔ ( 4 · ( 𝐿 · 𝐸 ) ) < ( 4 · 1 ) ) )
76 57 26 74 75 syl3anc ⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) < 1 ↔ ( 4 · ( 𝐿 · 𝐸 ) ) < ( 4 · 1 ) ) )
77 72 76 mpbid ⊢ ( 𝜑 → ( 4 · ( 𝐿 · 𝐸 ) ) < ( 4 · 1 ) )
78 4cn ⊢ 4 ∈ ℂ
79 78 mulridi ⊢ ( 4 · 1 ) = 4
80 77 79 breqtrdi ⊢ ( 𝜑 → ( 4 · ( 𝐿 · 𝐸 ) ) < 4 )
81 39 39 53 ltmuldivd ⊢ ( 𝜑 → ( ( 4 · ( 𝐿 · 𝐸 ) ) < 4 ↔ 4 < ( 4 / ( 𝐿 · 𝐸 ) ) ) )
82 80 81 mpbid ⊢ ( 𝜑 → 4 < ( 4 / ( 𝐿 · 𝐸 ) ) )
83 11 simpld ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
84 83 55 rpaddcld ⊢ ( 𝜑 → ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ∈ ℝ+ )
85 84 rpred ⊢ ( 𝜑 → ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ∈ ℝ )
86 56 83 ltaddrp2d ⊢ ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) < ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) )
87 85 resqcld ⊢ ( 𝜑 → ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) ∈ ℝ )
88 12 simpld ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
89 51 simp2d ⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
90 2z ⊢ 2 ∈ ℤ
91 rpexpcl ⊢ ( ( 𝐾 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝐾 ↑ 2 ) ∈ ℝ+ )
92 89 90 91 sylancl ⊢ ( 𝜑 → ( 𝐾 ↑ 2 ) ∈ ℝ+ )
93 88 92 rpmulcld ⊢ ( 𝜑 → ( 𝑋 · ( 𝐾 ↑ 2 ) ) ∈ ℝ+ )
94 4z ⊢ 4 ∈ ℤ
95 rpexpcl ⊢ ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ∈ ℝ+ ∧ 4 ∈ ℤ ) → ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) ∈ ℝ+ )
96 93 94 95 sylancl ⊢ ( 𝜑 → ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) ∈ ℝ+ )
97 3nn0 ⊢ 3 ∈ ℕ0
98 2nn ⊢ 2 ∈ ℕ
99 97 98 decnncl ⊢ 3 2 ∈ ℕ
100 nnrp ⊢ ( 3 2 ∈ ℕ → 3 2 ∈ ℝ+ )
101 99 100 ax-mp ⊢ 3 2 ∈ ℝ+
102 rpmulcl ⊢ ( ( 3 2 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 3 2 · 𝐵 ) ∈ ℝ+ )
103 101 3 102 sylancr ⊢ ( 𝜑 → ( 3 2 · 𝐵 ) ∈ ℝ+ )
104 67 simp3d ⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) ∈ ℝ+ )
105 rpexpcl ⊢ ( ( 𝐸 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝐸 ↑ 2 ) ∈ ℝ+ )
106 52 90 105 sylancl ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℝ+ )
107 50 106 rpmulcld ⊢ ( 𝜑 → ( 𝐿 · ( 𝐸 ↑ 2 ) ) ∈ ℝ+ )
108 104 107 rpmulcld ⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ∈ ℝ+ )
109 103 108 rpdivcld ⊢ ( 𝜑 → ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) ∈ ℝ+ )
110 3rp ⊢ 3 ∈ ℝ+
111 rpmulcl ⊢ ( ( 𝑈 ∈ ℝ+ ∧ 3 ∈ ℝ+ ) → ( 𝑈 · 3 ) ∈ ℝ+ )
112 7 110 111 sylancl ⊢ ( 𝜑 → ( 𝑈 · 3 ) ∈ ℝ+ )
113 112 13 rpaddcld ⊢ ( 𝜑 → ( ( 𝑈 · 3 ) + 𝐶 ) ∈ ℝ+ )
114 109 113 rpmulcld ⊢ ( 𝜑 → ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ∈ ℝ+ )
115 114 rpred ⊢ ( 𝜑 → ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ∈ ℝ )
116 115 rpefcld ⊢ ( 𝜑 → ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ∈ ℝ+ )
117 96 116 rpaddcld ⊢ ( 𝜑 → ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) ∈ ℝ+ )
118 87 117 ltaddrpd ⊢ ( 𝜑 → ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) < ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) ) )
119 118 14 breqtrrdi ⊢ ( 𝜑 → ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) < 𝑊 )
120 87 17 22 119 23 ltletrd ⊢ ( 𝜑 → ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) < 𝑍 )
121 24 rprege0d ⊢ ( 𝜑 → ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) )
122 resqrtth ⊢ ( ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) → ( ( √ ‘ 𝑍 ) ↑ 2 ) = 𝑍 )
123 121 122 syl ⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) ↑ 2 ) = 𝑍 )
124 120 123 breqtrrd ⊢ ( 𝜑 → ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) < ( ( √ ‘ 𝑍 ) ↑ 2 ) )
125 84 rprege0d ⊢ ( 𝜑 → ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ) )
126 29 rprege0d ⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑍 ) ) )
127 lt2sq ⊢ ( ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ) ∧ ( ( √ ‘ 𝑍 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑍 ) ) ) → ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) < ( √ ‘ 𝑍 ) ↔ ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) < ( ( √ ‘ 𝑍 ) ↑ 2 ) ) )
128 125 126 127 syl2anc ⊢ ( 𝜑 → ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) < ( √ ‘ 𝑍 ) ↔ ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) < ( ( √ ‘ 𝑍 ) ↑ 2 ) ) )
129 124 128 mpbird ⊢ ( 𝜑 → ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) < ( √ ‘ 𝑍 ) )
130 56 85 30 86 129 lttrd ⊢ ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) < ( √ ‘ 𝑍 ) )
131 39 56 30 82 130 lttrd ⊢ ( 𝜑 → 4 < ( √ ‘ 𝑍 ) )
132 28 39 30 45 131 lttrd ⊢ ( 𝜑 → e < ( √ ‘ 𝑍 ) )
133 26 28 30 37 132 lttrd ⊢ ( 𝜑 → 1 < ( √ ‘ 𝑍 ) )
134 0le1 ⊢ 0 ≤ 1
135 134 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
136 lt2sq ⊢ ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( ( √ ‘ 𝑍 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑍 ) ) ) → ( 1 < ( √ ‘ 𝑍 ) ↔ ( 1 ↑ 2 ) < ( ( √ ‘ 𝑍 ) ↑ 2 ) ) )
137 26 135 126 136 syl21anc ⊢ ( 𝜑 → ( 1 < ( √ ‘ 𝑍 ) ↔ ( 1 ↑ 2 ) < ( ( √ ‘ 𝑍 ) ↑ 2 ) ) )
138 133 137 mpbid ⊢ ( 𝜑 → ( 1 ↑ 2 ) < ( ( √ ‘ 𝑍 ) ↑ 2 ) )
139 sq1 ⊢ ( 1 ↑ 2 ) = 1
140 139 a1i ⊢ ( 𝜑 → ( 1 ↑ 2 ) = 1 )
141 138 140 123 3brtr3d ⊢ ( 𝜑 → 1 < 𝑍 )
142 28 30 132 ltled ⊢ ( 𝜑 → e ≤ ( √ ‘ 𝑍 ) )
143 22 83 rerpdivcld ⊢ ( 𝜑 → ( 𝑍 / 𝑌 ) ∈ ℝ )
144 83 rpred ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
145 144 55 ltaddrpd ⊢ ( 𝜑 → 𝑌 < ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) )
146 144 85 30 145 129 lttrd ⊢ ( 𝜑 → 𝑌 < ( √ ‘ 𝑍 ) )
147 144 30 29 146 ltmul2dd ⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) · 𝑌 ) < ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) )
148 remsqsqrt ⊢ ( ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) → ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) = 𝑍 )
149 121 148 syl ⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) = 𝑍 )
150 147 149 breqtrd ⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) · 𝑌 ) < 𝑍 )
151 30 22 83 ltmuldivd ⊢ ( 𝜑 → ( ( ( √ ‘ 𝑍 ) · 𝑌 ) < 𝑍 ↔ ( √ ‘ 𝑍 ) < ( 𝑍 / 𝑌 ) ) )
152 150 151 mpbid ⊢ ( 𝜑 → ( √ ‘ 𝑍 ) < ( 𝑍 / 𝑌 ) )
153 30 143 152 ltled ⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) )
154 141 142 153 3jca ⊢ ( 𝜑 → ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) )
155 56 30 130 ltled ⊢ ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) )
156 88 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℝ )
157 89 rpred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
158 67 simp2d ⊢ ( 𝜑 → 1 < 𝐾 )
159 157 158 rplogcld ⊢ ( 𝜑 → ( log ‘ 𝐾 ) ∈ ℝ+ )
160 156 159 rerpdivcld ⊢ ( 𝜑 → ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ∈ ℝ )
161 readdcl ⊢ ( ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ∈ ℝ )
162 160 34 161 sylancl ⊢ ( 𝜑 → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ∈ ℝ )
163 24 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℝ )
164 163 159 rerpdivcld ⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℝ )
165 nndivre ⊢ ( ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) ∈ ℝ ∧ 4 ∈ ℕ ) → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∈ ℝ )
166 164 46 165 sylancl ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∈ ℝ )
167 93 relogcld ⊢ ( 𝜑 → ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) ∈ ℝ )
168 nndivre ⊢ ( ( ( log ‘ 𝑍 ) ∈ ℝ ∧ 4 ∈ ℕ ) → ( ( log ‘ 𝑍 ) / 4 ) ∈ ℝ )
169 163 46 168 sylancl ⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) / 4 ) ∈ ℝ )
170 relogexp ⊢ ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ∈ ℝ+ ∧ 4 ∈ ℤ ) → ( log ‘ ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) ) = ( 4 · ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) ) )
171 93 94 170 sylancl ⊢ ( 𝜑 → ( log ‘ ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) ) = ( 4 · ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) ) )
172 96 rpred ⊢ ( 𝜑 → ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) ∈ ℝ )
173 117 rpred ⊢ ( 𝜑 → ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) ∈ ℝ )
174 172 116 ltaddrpd ⊢ ( 𝜑 → ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) < ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
175 rpexpcl ⊢ ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) ∈ ℝ+ )
176 84 90 175 sylancl ⊢ ( 𝜑 → ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) ∈ ℝ+ )
177 173 176 ltaddrpd ⊢ ( 𝜑 → ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) < ( ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) + ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) ) )
178 87 recnd ⊢ ( 𝜑 → ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) ∈ ℂ )
179 117 rpcnd ⊢ ( 𝜑 → ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) ∈ ℂ )
180 178 179 addcomd ⊢ ( 𝜑 → ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) ) = ( ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) + ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) ) )
181 14 180 eqtrid ⊢ ( 𝜑 → 𝑊 = ( ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) + ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) ) )
182 177 181 breqtrrd ⊢ ( 𝜑 → ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) < 𝑊 )
183 173 17 22 182 23 ltletrd ⊢ ( 𝜑 → ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) < 𝑍 )
184 172 173 22 174 183 lttrd ⊢ ( 𝜑 → ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) < 𝑍 )
185 logltb ⊢ ( ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) ∈ ℝ+ ∧ 𝑍 ∈ ℝ+ ) → ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) < 𝑍 ↔ ( log ‘ ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) ) < ( log ‘ 𝑍 ) ) )
186 96 24 185 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) < 𝑍 ↔ ( log ‘ ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) ) < ( log ‘ 𝑍 ) ) )
187 184 186 mpbid ⊢ ( 𝜑 → ( log ‘ ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) ) < ( log ‘ 𝑍 ) )
188 171 187 eqbrtrrd ⊢ ( 𝜑 → ( 4 · ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) ) < ( log ‘ 𝑍 ) )
189 ltmuldiv2 ⊢ ( ( ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) ∈ ℝ ∧ ( log ‘ 𝑍 ) ∈ ℝ ∧ ( 4 ∈ ℝ ∧ 0 < 4 ) ) → ( ( 4 · ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) ) < ( log ‘ 𝑍 ) ↔ ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) < ( ( log ‘ 𝑍 ) / 4 ) ) )
190 167 163 74 189 syl3anc ⊢ ( 𝜑 → ( ( 4 · ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) ) < ( log ‘ 𝑍 ) ↔ ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) < ( ( log ‘ 𝑍 ) / 4 ) ) )
191 188 190 mpbid ⊢ ( 𝜑 → ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) < ( ( log ‘ 𝑍 ) / 4 ) )
192 167 169 159 191 ltdiv1dd ⊢ ( 𝜑 → ( ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) / ( log ‘ 𝐾 ) ) < ( ( ( log ‘ 𝑍 ) / 4 ) / ( log ‘ 𝐾 ) ) )
193 88 92 relogmuld ⊢ ( 𝜑 → ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) = ( ( log ‘ 𝑋 ) + ( log ‘ ( 𝐾 ↑ 2 ) ) ) )
194 relogexp ⊢ ( ( 𝐾 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( log ‘ ( 𝐾 ↑ 2 ) ) = ( 2 · ( log ‘ 𝐾 ) ) )
195 89 90 194 sylancl ⊢ ( 𝜑 → ( log ‘ ( 𝐾 ↑ 2 ) ) = ( 2 · ( log ‘ 𝐾 ) ) )
196 195 oveq2d ⊢ ( 𝜑 → ( ( log ‘ 𝑋 ) + ( log ‘ ( 𝐾 ↑ 2 ) ) ) = ( ( log ‘ 𝑋 ) + ( 2 · ( log ‘ 𝐾 ) ) ) )
197 193 196 eqtrd ⊢ ( 𝜑 → ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) = ( ( log ‘ 𝑋 ) + ( 2 · ( log ‘ 𝐾 ) ) ) )
198 197 oveq1d ⊢ ( 𝜑 → ( ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) / ( log ‘ 𝐾 ) ) = ( ( ( log ‘ 𝑋 ) + ( 2 · ( log ‘ 𝐾 ) ) ) / ( log ‘ 𝐾 ) ) )
199 156 recnd ⊢ ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℂ )
200 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
201 159 rpcnd ⊢ ( 𝜑 → ( log ‘ 𝐾 ) ∈ ℂ )
202 200 201 mulcld ⊢ ( 𝜑 → ( 2 · ( log ‘ 𝐾 ) ) ∈ ℂ )
203 159 rpcnne0d ⊢ ( 𝜑 → ( ( log ‘ 𝐾 ) ∈ ℂ ∧ ( log ‘ 𝐾 ) ≠ 0 ) )
204 divdir ⊢ ( ( ( log ‘ 𝑋 ) ∈ ℂ ∧ ( 2 · ( log ‘ 𝐾 ) ) ∈ ℂ ∧ ( ( log ‘ 𝐾 ) ∈ ℂ ∧ ( log ‘ 𝐾 ) ≠ 0 ) ) → ( ( ( log ‘ 𝑋 ) + ( 2 · ( log ‘ 𝐾 ) ) ) / ( log ‘ 𝐾 ) ) = ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + ( ( 2 · ( log ‘ 𝐾 ) ) / ( log ‘ 𝐾 ) ) ) )
205 199 202 203 204 syl3anc ⊢ ( 𝜑 → ( ( ( log ‘ 𝑋 ) + ( 2 · ( log ‘ 𝐾 ) ) ) / ( log ‘ 𝐾 ) ) = ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + ( ( 2 · ( log ‘ 𝐾 ) ) / ( log ‘ 𝐾 ) ) ) )
206 203 simprd ⊢ ( 𝜑 → ( log ‘ 𝐾 ) ≠ 0 )
207 200 201 206 divcan4d ⊢ ( 𝜑 → ( ( 2 · ( log ‘ 𝐾 ) ) / ( log ‘ 𝐾 ) ) = 2 )
208 207 oveq2d ⊢ ( 𝜑 → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + ( ( 2 · ( log ‘ 𝐾 ) ) / ( log ‘ 𝐾 ) ) ) = ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) )
209 198 205 208 3eqtrd ⊢ ( 𝜑 → ( ( log ‘ ( 𝑋 · ( 𝐾 ↑ 2 ) ) ) / ( log ‘ 𝐾 ) ) = ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) )
210 163 recnd ⊢ ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℂ )
211 rpcnne0 ⊢ ( 4 ∈ ℝ+ → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
212 48 211 mp1i ⊢ ( 𝜑 → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
213 divdiv32 ⊢ ( ( ( log ‘ 𝑍 ) ∈ ℂ ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ∧ ( ( log ‘ 𝐾 ) ∈ ℂ ∧ ( log ‘ 𝐾 ) ≠ 0 ) ) → ( ( ( log ‘ 𝑍 ) / 4 ) / ( log ‘ 𝐾 ) ) = ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) )
214 210 212 203 213 syl3anc ⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) / 4 ) / ( log ‘ 𝐾 ) ) = ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) )
215 192 209 214 3brtr3d ⊢ ( 𝜑 → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) < ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) )
216 162 166 215 ltled ⊢ ( 𝜑 → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) )
217 113 rpred ⊢ ( 𝜑 → ( ( 𝑈 · 3 ) + 𝐶 ) ∈ ℝ )
218 108 103 rpdivcld ⊢ ( 𝜑 → ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) ∈ ℝ+ )
219 218 rpred ⊢ ( 𝜑 → ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) ∈ ℝ )
220 219 163 remulcld ⊢ ( 𝜑 → ( ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) · ( log ‘ 𝑍 ) ) ∈ ℝ )
221 113 rpcnd ⊢ ( 𝜑 → ( ( 𝑈 · 3 ) + 𝐶 ) ∈ ℂ )
222 108 rpcnne0d ⊢ ( 𝜑 → ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ∈ ℂ ∧ ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ≠ 0 ) )
223 103 rpcnne0d ⊢ ( 𝜑 → ( ( 3 2 · 𝐵 ) ∈ ℂ ∧ ( 3 2 · 𝐵 ) ≠ 0 ) )
224 divdiv2 ⊢ ( ( ( ( 𝑈 · 3 ) + 𝐶 ) ∈ ℂ ∧ ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ∈ ℂ ∧ ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ≠ 0 ) ∧ ( ( 3 2 · 𝐵 ) ∈ ℂ ∧ ( 3 2 · 𝐵 ) ≠ 0 ) ) → ( ( ( 𝑈 · 3 ) + 𝐶 ) / ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) ) = ( ( ( ( 𝑈 · 3 ) + 𝐶 ) · ( 3 2 · 𝐵 ) ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) )
225 221 222 223 224 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑈 · 3 ) + 𝐶 ) / ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) ) = ( ( ( ( 𝑈 · 3 ) + 𝐶 ) · ( 3 2 · 𝐵 ) ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) )
226 103 rpcnd ⊢ ( 𝜑 → ( 3 2 · 𝐵 ) ∈ ℂ )
227 221 226 mulcomd ⊢ ( 𝜑 → ( ( ( 𝑈 · 3 ) + 𝐶 ) · ( 3 2 · 𝐵 ) ) = ( ( 3 2 · 𝐵 ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) )
228 227 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑈 · 3 ) + 𝐶 ) · ( 3 2 · 𝐵 ) ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) = ( ( ( 3 2 · 𝐵 ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) )
229 div23 ⊢ ( ( ( 3 2 · 𝐵 ) ∈ ℂ ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ∈ ℂ ∧ ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ∈ ℂ ∧ ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ≠ 0 ) ) → ( ( ( 3 2 · 𝐵 ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) = ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) )
230 226 221 222 229 syl3anc ⊢ ( 𝜑 → ( ( ( 3 2 · 𝐵 ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) = ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) )
231 225 228 230 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑈 · 3 ) + 𝐶 ) / ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) ) = ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) )
232 115 reefcld ⊢ ( 𝜑 → ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ∈ ℝ )
233 232 96 ltaddrp2d ⊢ ( 𝜑 → ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) < ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
234 232 173 22 233 183 lttrd ⊢ ( 𝜑 → ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) < 𝑍 )
235 24 reeflogd ⊢ ( 𝜑 → ( exp ‘ ( log ‘ 𝑍 ) ) = 𝑍 )
236 234 235 breqtrrd ⊢ ( 𝜑 → ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) < ( exp ‘ ( log ‘ 𝑍 ) ) )
237 eflt ⊢ ( ( ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ∈ ℝ ∧ ( log ‘ 𝑍 ) ∈ ℝ ) → ( ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) < ( log ‘ 𝑍 ) ↔ ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) < ( exp ‘ ( log ‘ 𝑍 ) ) ) )
238 115 163 237 syl2anc ⊢ ( 𝜑 → ( ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) < ( log ‘ 𝑍 ) ↔ ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) < ( exp ‘ ( log ‘ 𝑍 ) ) ) )
239 236 238 mpbird ⊢ ( 𝜑 → ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) < ( log ‘ 𝑍 ) )
240 231 239 eqbrtrd ⊢ ( 𝜑 → ( ( ( 𝑈 · 3 ) + 𝐶 ) / ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) ) < ( log ‘ 𝑍 ) )
241 217 163 218 ltdivmuld ⊢ ( 𝜑 → ( ( ( ( 𝑈 · 3 ) + 𝐶 ) / ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) ) < ( log ‘ 𝑍 ) ↔ ( ( 𝑈 · 3 ) + 𝐶 ) < ( ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) · ( log ‘ 𝑍 ) ) ) )
242 240 241 mpbid ⊢ ( 𝜑 → ( ( 𝑈 · 3 ) + 𝐶 ) < ( ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) · ( log ‘ 𝑍 ) ) )
243 217 220 242 ltled ⊢ ( 𝜑 → ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) · ( log ‘ 𝑍 ) ) )
244 104 rpcnd ⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) ∈ ℂ )
245 107 rpcnd ⊢ ( 𝜑 → ( 𝐿 · ( 𝐸 ↑ 2 ) ) ∈ ℂ )
246 divass ⊢ ( ( ( 𝑈 − 𝐸 ) ∈ ℂ ∧ ( 𝐿 · ( 𝐸 ↑ 2 ) ) ∈ ℂ ∧ ( ( 3 2 · 𝐵 ) ∈ ℂ ∧ ( 3 2 · 𝐵 ) ≠ 0 ) ) → ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) = ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ) )
247 244 245 223 246 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) = ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ) )
248 247 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) / ( 3 2 · 𝐵 ) ) · ( log ‘ 𝑍 ) ) = ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) )
249 243 248 breqtrd ⊢ ( 𝜑 → ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) )
250 155 216 249 3jca ⊢ ( 𝜑 → ( ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) ∧ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) )
251 24 154 250 3jca ⊢ ( 𝜑 → ( 𝑍 ∈ ℝ+ ∧ ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) ∧ ( ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) ∧ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) )