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 syl5eq ⊢ ( 𝜑 → 𝐼 = ( ( ( ⌊ ‘ ( 𝑍 / ( ( 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 ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) )