Metamath Proof Explorer


Theorem pntlemr

Description: Lemma for pntlemj . (Contributed by Mario Carneiro, 7-Jun-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 ( 𝜑𝑍 ∈ ( 𝑊 [,) +∞ ) )
pntlem1.m 𝑀 = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 )
pntlem1.n 𝑁 = ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
pntlem1.U ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
pntlem1.K ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
pntlem1.o 𝑂 = ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝐽 ) ) ) )
pntlem1.v ( 𝜑𝑉 ∈ ℝ+ )
pntlem1.V ( 𝜑 → ( ( ( 𝐾𝐽 ) < 𝑉 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 · ( 𝐾𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑉 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ( abs ‘ ( ( 𝑅𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
pntlem1.j ( 𝜑𝐽 ∈ ( 𝑀 ..^ 𝑁 ) )
pntlem1.i 𝐼 = ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) )
Assertion pntlemr ( 𝜑 → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ ( ( ♯ ‘ 𝐼 ) · ( ( 𝑈𝐸 ) · ( ( 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 pntlem1.m 𝑀 = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 )
17 pntlem1.n 𝑁 = ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
18 pntlem1.U ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
19 pntlem1.K ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
20 pntlem1.o 𝑂 = ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾𝐽 ) ) ) )
21 pntlem1.v ( 𝜑𝑉 ∈ ℝ+ )
22 pntlem1.V ( 𝜑 → ( ( ( 𝐾𝐽 ) < 𝑉 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 · ( 𝐾𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑉 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ( abs ‘ ( ( 𝑅𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
23 pntlem1.j ( 𝜑𝐽 ∈ ( 𝑀 ..^ 𝑁 ) )
24 pntlem1.i 𝐼 = ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) )
25 1 2 3 4 5 6 pntlemd ( 𝜑 → ( 𝐿 ∈ ℝ+𝐷 ∈ ℝ+𝐹 ∈ ℝ+ ) )
26 25 simp1d ( 𝜑𝐿 ∈ ℝ+ )
27 1 2 3 4 5 6 7 8 9 10 pntlemc ( 𝜑 → ( 𝐸 ∈ ℝ+𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈𝐸 ) ∈ ℝ+ ) ) )
28 27 simp1d ( 𝜑𝐸 ∈ ℝ+ )
29 26 28 rpmulcld ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℝ+ )
30 4re 4 ∈ ℝ
31 4pos 0 < 4
32 30 31 elrpii 4 ∈ ℝ+
33 rpdivcl ( ( ( 𝐿 · 𝐸 ) ∈ ℝ+ ∧ 4 ∈ ℝ+ ) → ( ( 𝐿 · 𝐸 ) / 4 ) ∈ ℝ+ )
34 29 32 33 sylancl ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 4 ) ∈ ℝ+ )
35 34 rpred ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 4 ) ∈ ℝ )
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 pntlemb ( 𝜑 → ( 𝑍 ∈ ℝ+ ∧ ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) ∧ ( ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) ∧ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) )
37 36 simp1d ( 𝜑𝑍 ∈ ℝ+ )
38 37 21 rpdivcld ( 𝜑 → ( 𝑍 / 𝑉 ) ∈ ℝ+ )
39 38 rpred ( 𝜑 → ( 𝑍 / 𝑉 ) ∈ ℝ )
40 35 39 remulcld ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) ∈ ℝ )
41 fzfid ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) ∈ Fin )
42 24 41 eqeltrid ( 𝜑𝐼 ∈ Fin )
43 hashcl ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
44 42 43 syl ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
45 44 nn0red ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℝ )
46 40 recnd ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) ∈ ℂ )
47 1rp 1 ∈ ℝ+
48 rpaddcl ( ( 1 ∈ ℝ+ ∧ ( 𝐿 · 𝐸 ) ∈ ℝ+ ) → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
49 47 29 48 sylancr ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
50 49 21 rpmulcld ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ∈ ℝ+ )
51 37 50 rpdivcld ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ+ )
52 51 rpred ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ )
53 reflcl ( ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℝ )
54 52 53 syl ( 𝜑 → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℝ )
55 54 recnd ( 𝜑 → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℂ )
56 1cnd ( 𝜑 → 1 ∈ ℂ )
57 46 55 56 add32d ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) + 1 ) = ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) )
58 peano2re ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) ∈ ℝ → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ℝ )
59 40 58 syl ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ℝ )
60 59 54 readdcld ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) ∈ ℝ )
61 reflcl ( ( 𝑍 / 𝑉 ) ∈ ℝ → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℝ )
62 39 61 syl ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℝ )
63 peano2re ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ℝ )
64 62 63 syl ( 𝜑 → ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ℝ )
65 29 rphalfcld ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 2 ) ∈ ℝ+ )
66 65 38 rpmulcld ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) ∈ ℝ+ )
67 66 rpred ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) ∈ ℝ )
68 67 52 readdcld ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℝ )
69 rpdivcl ( ( 4 ∈ ℝ+ ∧ ( 𝐿 · 𝐸 ) ∈ ℝ+ ) → ( 4 / ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
70 32 29 69 sylancr ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
71 70 rpred ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ∈ ℝ )
72 37 rpsqrtcld ( 𝜑 → ( √ ‘ 𝑍 ) ∈ ℝ+ )
73 72 rpred ( 𝜑 → ( √ ‘ 𝑍 ) ∈ ℝ )
74 36 simp3d ( 𝜑 → ( ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) ∧ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) )
75 74 simp1d ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) )
76 50 rpred ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ∈ ℝ )
77 27 simp2d ( 𝜑𝐾 ∈ ℝ+ )
78 elfzoelz ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
79 23 78 syl ( 𝜑𝐽 ∈ ℤ )
80 79 peano2zd ( 𝜑 → ( 𝐽 + 1 ) ∈ ℤ )
81 77 80 rpexpcld ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∈ ℝ+ )
82 81 rpred ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∈ ℝ )
83 22 simplrd ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 · ( 𝐾𝐽 ) ) )
84 77 rpcnd ( 𝜑𝐾 ∈ ℂ )
85 77 79 rpexpcld ( 𝜑 → ( 𝐾𝐽 ) ∈ ℝ+ )
86 85 rpcnd ( 𝜑 → ( 𝐾𝐽 ) ∈ ℂ )
87 84 86 mulcomd ( 𝜑 → ( 𝐾 · ( 𝐾𝐽 ) ) = ( ( 𝐾𝐽 ) · 𝐾 ) )
88 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemg ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ𝑀 ) ∧ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ≤ ( 𝑁𝑀 ) ) )
89 88 simp1d ( 𝜑𝑀 ∈ ℕ )
90 elfzouz ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐽 ∈ ( ℤ𝑀 ) )
91 23 90 syl ( 𝜑𝐽 ∈ ( ℤ𝑀 ) )
92 eluznn ( ( 𝑀 ∈ ℕ ∧ 𝐽 ∈ ( ℤ𝑀 ) ) → 𝐽 ∈ ℕ )
93 89 91 92 syl2anc ( 𝜑𝐽 ∈ ℕ )
94 93 nnnn0d ( 𝜑𝐽 ∈ ℕ0 )
95 84 94 expp1d ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) = ( ( 𝐾𝐽 ) · 𝐾 ) )
96 87 95 eqtr4d ( 𝜑 → ( 𝐾 · ( 𝐾𝐽 ) ) = ( 𝐾 ↑ ( 𝐽 + 1 ) ) )
97 83 96 breqtrd ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 ↑ ( 𝐽 + 1 ) ) )
98 76 82 97 ltled ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ≤ ( 𝐾 ↑ ( 𝐽 + 1 ) ) )
99 fzofzp1 ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐽 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
100 23 99 syl ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
101 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemh ( ( 𝜑 ∧ ( 𝐽 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑋 < ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∧ ( 𝐾 ↑ ( 𝐽 + 1 ) ) ≤ ( √ ‘ 𝑍 ) ) )
102 100 101 mpdan ( 𝜑 → ( 𝑋 < ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∧ ( 𝐾 ↑ ( 𝐽 + 1 ) ) ≤ ( √ ‘ 𝑍 ) ) )
103 102 simprd ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) ≤ ( √ ‘ 𝑍 ) )
104 76 82 73 98 103 letrd ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ≤ ( √ ‘ 𝑍 ) )
105 76 73 72 lemul2d ( 𝜑 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ≤ ( √ ‘ 𝑍 ) ↔ ( ( √ ‘ 𝑍 ) · ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) ) )
106 104 105 mpbid ( 𝜑 → ( ( √ ‘ 𝑍 ) · ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) )
107 37 rprege0d ( 𝜑 → ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) )
108 remsqsqrt ( ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) → ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) = 𝑍 )
109 107 108 syl ( 𝜑 → ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) = 𝑍 )
110 106 109 breqtrd ( 𝜑 → ( ( √ ‘ 𝑍 ) · ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ 𝑍 )
111 37 rpred ( 𝜑𝑍 ∈ ℝ )
112 73 111 50 lemuldivd ( 𝜑 → ( ( ( √ ‘ 𝑍 ) · ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ 𝑍 ↔ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) )
113 110 112 mpbid ( 𝜑 → ( √ ‘ 𝑍 ) ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
114 21 rpcnd ( 𝜑𝑉 ∈ ℂ )
115 114 mulid2d ( 𝜑 → ( 1 · 𝑉 ) = 𝑉 )
116 1red ( 𝜑 → 1 ∈ ℝ )
117 49 rpred ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ )
118 1re 1 ∈ ℝ
119 ltaddrp ( ( 1 ∈ ℝ ∧ ( 𝐿 · 𝐸 ) ∈ ℝ+ ) → 1 < ( 1 + ( 𝐿 · 𝐸 ) ) )
120 118 29 119 sylancr ( 𝜑 → 1 < ( 1 + ( 𝐿 · 𝐸 ) ) )
121 116 117 21 120 ltmul1dd ( 𝜑 → ( 1 · 𝑉 ) < ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) )
122 115 121 eqbrtrrd ( 𝜑𝑉 < ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) )
123 21 50 37 ltdiv2d ( 𝜑 → ( 𝑉 < ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ↔ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) < ( 𝑍 / 𝑉 ) ) )
124 122 123 mpbid ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) < ( 𝑍 / 𝑉 ) )
125 52 39 124 ltled ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ ( 𝑍 / 𝑉 ) )
126 73 52 39 113 125 letrd ( 𝜑 → ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑉 ) )
127 71 73 39 75 126 letrd ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( 𝑍 / 𝑉 ) )
128 71 39 39 127 leadd2dd ( 𝜑 → ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ≤ ( ( 𝑍 / 𝑉 ) + ( 𝑍 / 𝑉 ) ) )
129 38 rpcnd ( 𝜑 → ( 𝑍 / 𝑉 ) ∈ ℂ )
130 129 2timesd ( 𝜑 → ( 2 · ( 𝑍 / 𝑉 ) ) = ( ( 𝑍 / 𝑉 ) + ( 𝑍 / 𝑉 ) ) )
131 128 130 breqtrrd ( 𝜑 → ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ≤ ( 2 · ( 𝑍 / 𝑉 ) ) )
132 39 71 readdcld ( 𝜑 → ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ∈ ℝ )
133 2re 2 ∈ ℝ
134 remulcl ( ( 2 ∈ ℝ ∧ ( 𝑍 / 𝑉 ) ∈ ℝ ) → ( 2 · ( 𝑍 / 𝑉 ) ) ∈ ℝ )
135 133 39 134 sylancr ( 𝜑 → ( 2 · ( 𝑍 / 𝑉 ) ) ∈ ℝ )
136 132 135 34 lemul2d ( 𝜑 → ( ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ≤ ( 2 · ( 𝑍 / 𝑉 ) ) ↔ ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ) ≤ ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 2 · ( 𝑍 / 𝑉 ) ) ) ) )
137 131 136 mpbid ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ) ≤ ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 2 · ( 𝑍 / 𝑉 ) ) ) )
138 34 rpcnd ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 4 ) ∈ ℂ )
139 70 rpcnd ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ∈ ℂ )
140 138 129 139 adddid ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ) = ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 4 / ( 𝐿 · 𝐸 ) ) ) ) )
141 29 rpcnne0d ( 𝜑 → ( ( 𝐿 · 𝐸 ) ∈ ℂ ∧ ( 𝐿 · 𝐸 ) ≠ 0 ) )
142 rpcnne0 ( 4 ∈ ℝ+ → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
143 32 142 mp1i ( 𝜑 → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
144 divcan6 ( ( ( ( 𝐿 · 𝐸 ) ∈ ℂ ∧ ( 𝐿 · 𝐸 ) ≠ 0 ) ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 4 / ( 𝐿 · 𝐸 ) ) ) = 1 )
145 141 143 144 syl2anc ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 4 / ( 𝐿 · 𝐸 ) ) ) = 1 )
146 145 oveq2d ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 4 / ( 𝐿 · 𝐸 ) ) ) ) = ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) )
147 140 146 eqtrd ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ) = ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) )
148 2cnd ( 𝜑 → 2 ∈ ℂ )
149 138 148 129 mulassd ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · 2 ) · ( 𝑍 / 𝑉 ) ) = ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 2 · ( 𝑍 / 𝑉 ) ) ) )
150 29 rpcnd ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℂ )
151 2rp 2 ∈ ℝ+
152 rpcnne0 ( 2 ∈ ℝ+ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
153 151 152 mp1i ( 𝜑 → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
154 divdiv1 ( ( ( 𝐿 · 𝐸 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 𝐿 · 𝐸 ) / 2 ) / 2 ) = ( ( 𝐿 · 𝐸 ) / ( 2 · 2 ) ) )
155 150 153 153 154 syl3anc ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 2 ) / 2 ) = ( ( 𝐿 · 𝐸 ) / ( 2 · 2 ) ) )
156 2t2e4 ( 2 · 2 ) = 4
157 156 oveq2i ( ( 𝐿 · 𝐸 ) / ( 2 · 2 ) ) = ( ( 𝐿 · 𝐸 ) / 4 )
158 155 157 eqtr2di ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 4 ) = ( ( ( 𝐿 · 𝐸 ) / 2 ) / 2 ) )
159 158 oveq1d ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · 2 ) = ( ( ( ( 𝐿 · 𝐸 ) / 2 ) / 2 ) · 2 ) )
160 150 halfcld ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 2 ) ∈ ℂ )
161 153 simprd ( 𝜑 → 2 ≠ 0 )
162 160 148 161 divcan1d ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) / 2 ) · 2 ) = ( ( 𝐿 · 𝐸 ) / 2 ) )
163 159 162 eqtrd ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · 2 ) = ( ( 𝐿 · 𝐸 ) / 2 ) )
164 163 oveq1d ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · 2 ) · ( 𝑍 / 𝑉 ) ) = ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) )
165 149 164 eqtr3d ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 2 · ( 𝑍 / 𝑉 ) ) ) = ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) )
166 137 147 165 3brtr3d ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) ≤ ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) )
167 flle ( ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
168 52 167 syl ( 𝜑 → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
169 59 54 67 52 166 168 le2addd ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) ≤ ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) )
170 65 rpred ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 2 ) ∈ ℝ )
171 49 rprecred ( 𝜑 → ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ∈ ℝ )
172 170 171 readdcld ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 2 ) + ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) ∈ ℝ )
173 29 rpred ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℝ )
174 28 rpred ( 𝜑𝐸 ∈ ℝ )
175 26 rpred ( 𝜑𝐿 ∈ ℝ )
176 eliooord ( 𝐿 ∈ ( 0 (,) 1 ) → ( 0 < 𝐿𝐿 < 1 ) )
177 4 176 syl ( 𝜑 → ( 0 < 𝐿𝐿 < 1 ) )
178 177 simprd ( 𝜑𝐿 < 1 )
179 175 116 28 178 ltmul1dd ( 𝜑 → ( 𝐿 · 𝐸 ) < ( 1 · 𝐸 ) )
180 28 rpcnd ( 𝜑𝐸 ∈ ℂ )
181 180 mulid2d ( 𝜑 → ( 1 · 𝐸 ) = 𝐸 )
182 179 181 breqtrd ( 𝜑 → ( 𝐿 · 𝐸 ) < 𝐸 )
183 27 simp3d ( 𝜑 → ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈𝐸 ) ∈ ℝ+ ) )
184 183 simp1d ( 𝜑𝐸 ∈ ( 0 (,) 1 ) )
185 eliooord ( 𝐸 ∈ ( 0 (,) 1 ) → ( 0 < 𝐸𝐸 < 1 ) )
186 184 185 syl ( 𝜑 → ( 0 < 𝐸𝐸 < 1 ) )
187 186 simprd ( 𝜑𝐸 < 1 )
188 173 174 116 182 187 lttrd ( 𝜑 → ( 𝐿 · 𝐸 ) < 1 )
189 173 116 116 188 ltadd2dd ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) < ( 1 + 1 ) )
190 df-2 2 = ( 1 + 1 )
191 189 190 breqtrrdi ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) < 2 )
192 49 rpregt0d ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ ∧ 0 < ( 1 + ( 𝐿 · 𝐸 ) ) ) )
193 133 a1i ( 𝜑 → 2 ∈ ℝ )
194 2pos 0 < 2
195 194 a1i ( 𝜑 → 0 < 2 )
196 29 rpregt0d ( 𝜑 → ( ( 𝐿 · 𝐸 ) ∈ ℝ ∧ 0 < ( 𝐿 · 𝐸 ) ) )
197 ltdiv2 ( ( ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ ∧ 0 < ( 1 + ( 𝐿 · 𝐸 ) ) ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ∧ ( ( 𝐿 · 𝐸 ) ∈ ℝ ∧ 0 < ( 𝐿 · 𝐸 ) ) ) → ( ( 1 + ( 𝐿 · 𝐸 ) ) < 2 ↔ ( ( 𝐿 · 𝐸 ) / 2 ) < ( ( 𝐿 · 𝐸 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
198 192 193 195 196 197 syl121anc ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) < 2 ↔ ( ( 𝐿 · 𝐸 ) / 2 ) < ( ( 𝐿 · 𝐸 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
199 191 198 mpbid ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 2 ) < ( ( 𝐿 · 𝐸 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) )
200 49 rpcnd ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ )
201 49 rpcnne0d ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ ∧ ( 1 + ( 𝐿 · 𝐸 ) ) ≠ 0 ) )
202 divsubdir ( ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ ∧ ( 1 + ( 𝐿 · 𝐸 ) ) ≠ 0 ) ) → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) − 1 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( ( ( 1 + ( 𝐿 · 𝐸 ) ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
203 200 56 201 202 syl3anc ( 𝜑 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) − 1 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( ( ( 1 + ( 𝐿 · 𝐸 ) ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
204 ax-1cn 1 ∈ ℂ
205 pncan2 ( ( 1 ∈ ℂ ∧ ( 𝐿 · 𝐸 ) ∈ ℂ ) → ( ( 1 + ( 𝐿 · 𝐸 ) ) − 1 ) = ( 𝐿 · 𝐸 ) )
206 204 150 205 sylancr ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) − 1 ) = ( 𝐿 · 𝐸 ) )
207 206 oveq1d ( 𝜑 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) − 1 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( ( 𝐿 · 𝐸 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) )
208 divid ( ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ ∧ ( 1 + ( 𝐿 · 𝐸 ) ) ≠ 0 ) → ( ( 1 + ( 𝐿 · 𝐸 ) ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = 1 )
209 201 208 syl ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = 1 )
210 209 oveq1d ( 𝜑 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) = ( 1 − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
211 203 207 210 3eqtr3d ( 𝜑 → ( ( 𝐿 · 𝐸 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( 1 − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
212 199 211 breqtrd ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 2 ) < ( 1 − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
213 170 171 116 ltaddsubd ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) + ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) < 1 ↔ ( ( 𝐿 · 𝐸 ) / 2 ) < ( 1 − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) ) )
214 212 213 mpbird ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 2 ) + ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) < 1 )
215 172 116 38 214 ltmul1dd ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) + ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) · ( 𝑍 / 𝑉 ) ) < ( 1 · ( 𝑍 / 𝑉 ) ) )
216 reccl ( ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ ∧ ( 1 + ( 𝐿 · 𝐸 ) ) ≠ 0 ) → ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ∈ ℂ )
217 201 216 syl ( 𝜑 → ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ∈ ℂ )
218 160 217 129 adddird ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) + ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) · ( 𝑍 / 𝑉 ) ) = ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) · ( 𝑍 / 𝑉 ) ) ) )
219 200 114 mulcomd ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) = ( 𝑉 · ( 1 + ( 𝐿 · 𝐸 ) ) ) )
220 219 oveq2d ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) = ( 𝑍 / ( 𝑉 · ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
221 37 rpcnd ( 𝜑𝑍 ∈ ℂ )
222 21 rpcnne0d ( 𝜑 → ( 𝑉 ∈ ℂ ∧ 𝑉 ≠ 0 ) )
223 divdiv1 ( ( 𝑍 ∈ ℂ ∧ ( 𝑉 ∈ ℂ ∧ 𝑉 ≠ 0 ) ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ ∧ ( 1 + ( 𝐿 · 𝐸 ) ) ≠ 0 ) ) → ( ( 𝑍 / 𝑉 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( 𝑍 / ( 𝑉 · ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
224 221 222 201 223 syl3anc ( 𝜑 → ( ( 𝑍 / 𝑉 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( 𝑍 / ( 𝑉 · ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
225 49 rpne0d ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) ≠ 0 )
226 129 200 225 divrec2d ( 𝜑 → ( ( 𝑍 / 𝑉 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) · ( 𝑍 / 𝑉 ) ) )
227 220 224 226 3eqtr2d ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) = ( ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) · ( 𝑍 / 𝑉 ) ) )
228 227 oveq2d ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) = ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) · ( 𝑍 / 𝑉 ) ) ) )
229 218 228 eqtr4d ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) + ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) · ( 𝑍 / 𝑉 ) ) = ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) )
230 129 mulid2d ( 𝜑 → ( 1 · ( 𝑍 / 𝑉 ) ) = ( 𝑍 / 𝑉 ) )
231 215 229 230 3brtr3d ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) < ( 𝑍 / 𝑉 ) )
232 60 68 39 169 231 lelttrd ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) < ( 𝑍 / 𝑉 ) )
233 fllep1 ( ( 𝑍 / 𝑉 ) ∈ ℝ → ( 𝑍 / 𝑉 ) ≤ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) )
234 39 233 syl ( 𝜑 → ( 𝑍 / 𝑉 ) ≤ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) )
235 60 39 64 232 234 ltletrd ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) < ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) )
236 57 235 eqbrtrd ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) + 1 ) < ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) )
237 40 54 readdcld ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) ∈ ℝ )
238 237 62 116 ltadd1d ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) < ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ↔ ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) + 1 ) < ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) )
239 236 238 mpbird ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) < ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) )
240 40 54 62 ltaddsubd ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) < ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ↔ ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) < ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) − ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) ) )
241 239 240 mpbid ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) < ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) − ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) )
242 39 flcld ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℤ )
243 fzval3 ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℤ → ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ..^ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) )
244 242 243 syl ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ..^ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) )
245 24 244 eqtrid ( 𝜑𝐼 = ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ..^ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) )
246 245 fveq2d ( 𝜑 → ( ♯ ‘ 𝐼 ) = ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ..^ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) ) )
247 flword2 ( ( ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ ∧ ( 𝑍 / 𝑉 ) ∈ ℝ ∧ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ ( 𝑍 / 𝑉 ) ) → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ( ℤ ‘ ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) )
248 52 39 125 247 syl3anc ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ( ℤ ‘ ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) )
249 eluzp1p1 ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ( ℤ ‘ ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) → ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ( ℤ ‘ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) )
250 248 249 syl ( 𝜑 → ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ( ℤ ‘ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) )
251 hashfzo ( ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ( ℤ ‘ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) → ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ..^ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) − ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) )
252 250 251 syl ( 𝜑 → ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ..^ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) − ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) )
253 62 recnd ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℂ )
254 253 55 56 pnpcan2d ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) − ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) = ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) − ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) )
255 246 252 254 3eqtrd ( 𝜑 → ( ♯ ‘ 𝐼 ) = ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) − ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) )
256 241 255 breqtrrd ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) < ( ♯ ‘ 𝐼 ) )
257 40 45 256 ltled ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) ≤ ( ♯ ‘ 𝐼 ) )
258 35 45 38 lemuldivd ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) ≤ ( ♯ ‘ 𝐼 ) ↔ ( ( 𝐿 · 𝐸 ) / 4 ) ≤ ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) ) )
259 257 258 mpbid ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 4 ) ≤ ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) )
260 21 rpred ( 𝜑𝑉 ∈ ℝ )
261 76 82 73 97 103 ltletrd ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( √ ‘ 𝑍 ) )
262 260 76 73 122 261 lttrd ( 𝜑𝑉 < ( √ ‘ 𝑍 ) )
263 260 73 262 ltled ( 𝜑𝑉 ≤ ( √ ‘ 𝑍 ) )
264 21 rprege0d ( 𝜑 → ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) )
265 72 rprege0d ( 𝜑 → ( ( √ ‘ 𝑍 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑍 ) ) )
266 le2sq ( ( ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ∧ ( ( √ ‘ 𝑍 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑍 ) ) ) → ( 𝑉 ≤ ( √ ‘ 𝑍 ) ↔ ( 𝑉 ↑ 2 ) ≤ ( ( √ ‘ 𝑍 ) ↑ 2 ) ) )
267 264 265 266 syl2anc ( 𝜑 → ( 𝑉 ≤ ( √ ‘ 𝑍 ) ↔ ( 𝑉 ↑ 2 ) ≤ ( ( √ ‘ 𝑍 ) ↑ 2 ) ) )
268 263 267 mpbid ( 𝜑 → ( 𝑉 ↑ 2 ) ≤ ( ( √ ‘ 𝑍 ) ↑ 2 ) )
269 resqrtth ( ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) → ( ( √ ‘ 𝑍 ) ↑ 2 ) = 𝑍 )
270 107 269 syl ( 𝜑 → ( ( √ ‘ 𝑍 ) ↑ 2 ) = 𝑍 )
271 268 270 breqtrd ( 𝜑 → ( 𝑉 ↑ 2 ) ≤ 𝑍 )
272 2z 2 ∈ ℤ
273 rpexpcl ( ( 𝑉 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝑉 ↑ 2 ) ∈ ℝ+ )
274 21 272 273 sylancl ( 𝜑 → ( 𝑉 ↑ 2 ) ∈ ℝ+ )
275 274 rpred ( 𝜑 → ( 𝑉 ↑ 2 ) ∈ ℝ )
276 275 111 37 lemul2d ( 𝜑 → ( ( 𝑉 ↑ 2 ) ≤ 𝑍 ↔ ( 𝑍 · ( 𝑉 ↑ 2 ) ) ≤ ( 𝑍 · 𝑍 ) ) )
277 271 276 mpbid ( 𝜑 → ( 𝑍 · ( 𝑉 ↑ 2 ) ) ≤ ( 𝑍 · 𝑍 ) )
278 221 sqvald ( 𝜑 → ( 𝑍 ↑ 2 ) = ( 𝑍 · 𝑍 ) )
279 277 278 breqtrrd ( 𝜑 → ( 𝑍 · ( 𝑉 ↑ 2 ) ) ≤ ( 𝑍 ↑ 2 ) )
280 111 resqcld ( 𝜑 → ( 𝑍 ↑ 2 ) ∈ ℝ )
281 111 280 274 lemuldivd ( 𝜑 → ( ( 𝑍 · ( 𝑉 ↑ 2 ) ) ≤ ( 𝑍 ↑ 2 ) ↔ 𝑍 ≤ ( ( 𝑍 ↑ 2 ) / ( 𝑉 ↑ 2 ) ) ) )
282 279 281 mpbid ( 𝜑𝑍 ≤ ( ( 𝑍 ↑ 2 ) / ( 𝑉 ↑ 2 ) ) )
283 21 rpne0d ( 𝜑𝑉 ≠ 0 )
284 221 114 283 sqdivd ( 𝜑 → ( ( 𝑍 / 𝑉 ) ↑ 2 ) = ( ( 𝑍 ↑ 2 ) / ( 𝑉 ↑ 2 ) ) )
285 282 284 breqtrrd ( 𝜑𝑍 ≤ ( ( 𝑍 / 𝑉 ) ↑ 2 ) )
286 rpexpcl ( ( ( 𝑍 / 𝑉 ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( 𝑍 / 𝑉 ) ↑ 2 ) ∈ ℝ+ )
287 38 272 286 sylancl ( 𝜑 → ( ( 𝑍 / 𝑉 ) ↑ 2 ) ∈ ℝ+ )
288 37 287 logled ( 𝜑 → ( 𝑍 ≤ ( ( 𝑍 / 𝑉 ) ↑ 2 ) ↔ ( log ‘ 𝑍 ) ≤ ( log ‘ ( ( 𝑍 / 𝑉 ) ↑ 2 ) ) ) )
289 285 288 mpbid ( 𝜑 → ( log ‘ 𝑍 ) ≤ ( log ‘ ( ( 𝑍 / 𝑉 ) ↑ 2 ) ) )
290 relogexp ( ( ( 𝑍 / 𝑉 ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( log ‘ ( ( 𝑍 / 𝑉 ) ↑ 2 ) ) = ( 2 · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
291 38 272 290 sylancl ( 𝜑 → ( log ‘ ( ( 𝑍 / 𝑉 ) ↑ 2 ) ) = ( 2 · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
292 289 291 breqtrd ( 𝜑 → ( log ‘ 𝑍 ) ≤ ( 2 · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
293 37 relogcld ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℝ )
294 38 relogcld ( 𝜑 → ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℝ )
295 ledivmul ( ( ( log ‘ 𝑍 ) ∈ ℝ ∧ ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( log ‘ 𝑍 ) / 2 ) ≤ ( log ‘ ( 𝑍 / 𝑉 ) ) ↔ ( log ‘ 𝑍 ) ≤ ( 2 · ( log ‘ ( 𝑍 / 𝑉 ) ) ) ) )
296 293 294 193 195 295 syl112anc ( 𝜑 → ( ( ( log ‘ 𝑍 ) / 2 ) ≤ ( log ‘ ( 𝑍 / 𝑉 ) ) ↔ ( log ‘ 𝑍 ) ≤ ( 2 · ( log ‘ ( 𝑍 / 𝑉 ) ) ) ) )
297 292 296 mpbird ( 𝜑 → ( ( log ‘ 𝑍 ) / 2 ) ≤ ( log ‘ ( 𝑍 / 𝑉 ) ) )
298 34 rprege0d ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐿 · 𝐸 ) / 4 ) ) )
299 45 38 rerpdivcld ( 𝜑 → ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) ∈ ℝ )
300 36 simp2d ( 𝜑 → ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) )
301 300 simp1d ( 𝜑 → 1 < 𝑍 )
302 111 301 rplogcld ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℝ+ )
303 302 rphalfcld ( 𝜑 → ( ( log ‘ 𝑍 ) / 2 ) ∈ ℝ+ )
304 303 rprege0d ( 𝜑 → ( ( ( log ‘ 𝑍 ) / 2 ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ 𝑍 ) / 2 ) ) )
305 lemul12a ( ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐿 · 𝐸 ) / 4 ) ) ∧ ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) ∈ ℝ ) ∧ ( ( ( ( log ‘ 𝑍 ) / 2 ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ 𝑍 ) / 2 ) ) ∧ ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℝ ) ) → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) ≤ ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) ∧ ( ( log ‘ 𝑍 ) / 2 ) ≤ ( log ‘ ( 𝑍 / 𝑉 ) ) ) → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) ≤ ( ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) ) )
306 298 299 304 294 305 syl22anc ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) ≤ ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) ∧ ( ( log ‘ 𝑍 ) / 2 ) ≤ ( log ‘ ( 𝑍 / 𝑉 ) ) ) → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) ≤ ( ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) ) )
307 259 297 306 mp2and ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) ≤ ( ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
308 302 rpcnd ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℂ )
309 8nn 8 ∈ ℕ
310 nnrp ( 8 ∈ ℕ → 8 ∈ ℝ+ )
311 309 310 ax-mp 8 ∈ ℝ+
312 rpcnne0 ( 8 ∈ ℝ+ → ( 8 ∈ ℂ ∧ 8 ≠ 0 ) )
313 311 312 mp1i ( 𝜑 → ( 8 ∈ ℂ ∧ 8 ≠ 0 ) )
314 div23 ( ( ( 𝐿 · 𝐸 ) ∈ ℂ ∧ ( log ‘ 𝑍 ) ∈ ℂ ∧ ( 8 ∈ ℂ ∧ 8 ≠ 0 ) ) → ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / 8 ) = ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) )
315 150 308 313 314 syl3anc ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / 8 ) = ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) )
316 divmuldiv ( ( ( ( 𝐿 · 𝐸 ) ∈ ℂ ∧ ( log ‘ 𝑍 ) ∈ ℂ ) ∧ ( ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) ) → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) = ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / ( 4 · 2 ) ) )
317 150 308 143 153 316 syl22anc ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) = ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / ( 4 · 2 ) ) )
318 4t2e8 ( 4 · 2 ) = 8
319 318 oveq2i ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / ( 4 · 2 ) ) = ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / 8 )
320 317 319 eqtr2di ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / 8 ) = ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) )
321 315 320 eqtr3d ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) = ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) )
322 45 recnd ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℂ )
323 294 recnd ( 𝜑 → ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℂ )
324 38 rpcnne0d ( 𝜑 → ( ( 𝑍 / 𝑉 ) ∈ ℂ ∧ ( 𝑍 / 𝑉 ) ≠ 0 ) )
325 divass ( ( ( ♯ ‘ 𝐼 ) ∈ ℂ ∧ ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℂ ∧ ( ( 𝑍 / 𝑉 ) ∈ ℂ ∧ ( 𝑍 / 𝑉 ) ≠ 0 ) ) → ( ( ( ♯ ‘ 𝐼 ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) / ( 𝑍 / 𝑉 ) ) = ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) )
326 div23 ( ( ( ♯ ‘ 𝐼 ) ∈ ℂ ∧ ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℂ ∧ ( ( 𝑍 / 𝑉 ) ∈ ℂ ∧ ( 𝑍 / 𝑉 ) ≠ 0 ) ) → ( ( ( ♯ ‘ 𝐼 ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) / ( 𝑍 / 𝑉 ) ) = ( ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
327 325 326 eqtr3d ( ( ( ♯ ‘ 𝐼 ) ∈ ℂ ∧ ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℂ ∧ ( ( 𝑍 / 𝑉 ) ∈ ℂ ∧ ( 𝑍 / 𝑉 ) ≠ 0 ) ) → ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) = ( ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
328 322 323 324 327 syl3anc ( 𝜑 → ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) = ( ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
329 307 321 328 3brtr4d ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ≤ ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) )
330 rpdivcl ( ( ( 𝐿 · 𝐸 ) ∈ ℝ+ ∧ 8 ∈ ℝ+ ) → ( ( 𝐿 · 𝐸 ) / 8 ) ∈ ℝ+ )
331 29 311 330 sylancl ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 8 ) ∈ ℝ+ )
332 331 302 rpmulcld ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ∈ ℝ+ )
333 332 rpred ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ∈ ℝ )
334 294 38 rerpdivcld ( 𝜑 → ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ∈ ℝ )
335 45 334 remulcld ( 𝜑 → ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ∈ ℝ )
336 183 simp3d ( 𝜑 → ( 𝑈𝐸 ) ∈ ℝ+ )
337 333 335 336 lemul2d ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ≤ ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ↔ ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ ( ( 𝑈𝐸 ) · ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) ) )
338 329 337 mpbid ( 𝜑 → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ ( ( 𝑈𝐸 ) · ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) )
339 336 rpcnd ( 𝜑 → ( 𝑈𝐸 ) ∈ ℂ )
340 334 recnd ( 𝜑 → ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ∈ ℂ )
341 339 322 340 mul12d ( 𝜑 → ( ( 𝑈𝐸 ) · ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) = ( ( ♯ ‘ 𝐼 ) · ( ( 𝑈𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) )
342 338 341 breqtrd ( 𝜑 → ( ( 𝑈𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ ( ( ♯ ‘ 𝐼 ) · ( ( 𝑈𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) )