MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pntlemr Structured version   Visualization version   GIF version

Theorem pntlemr 26987
Description: Lemma for pntlemj 26988. (Contributed by Mario Carneiro, 7-Jun-2016.)
Hypotheses
Ref Expression
pntlem1.r 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
pntlem1.a (𝜑𝐴 ∈ ℝ+)
pntlem1.b (𝜑𝐵 ∈ ℝ+)
pntlem1.l (𝜑𝐿 ∈ (0(,)1))
pntlem1.d 𝐷 = (𝐴 + 1)
pntlem1.f 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))
pntlem1.u (𝜑𝑈 ∈ ℝ+)
pntlem1.u2 (𝜑𝑈𝐴)
pntlem1.e 𝐸 = (𝑈 / 𝐷)
pntlem1.k 𝐾 = (exp‘(𝐵 / 𝐸))
pntlem1.y (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))
pntlem1.x (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))
pntlem1.c (𝜑𝐶 ∈ ℝ+)
pntlem1.w 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑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
Ref Expression
pntlemr (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
Distinct variable groups:   𝑧,𝐶   𝑦,𝑧,𝐽   𝑦,𝑢,𝑧,𝐿   𝑦,𝐾,𝑧   𝑧,𝑀   𝑧,𝑂   𝑧,𝑁   𝑢,𝑅,𝑦,𝑧   𝑢,𝑉   𝑧,𝑈   𝑧,𝑊   𝑦,𝑋,𝑧   𝑧,𝑌   𝑢,𝑎,𝑦,𝑧,𝐸   𝑢,𝑍,𝑧
Allowed substitution hints:   𝜑(𝑦,𝑧,𝑢,𝑎)   𝐴(𝑦,𝑧,𝑢,𝑎)   𝐵(𝑦,𝑧,𝑢,𝑎)   𝐶(𝑦,𝑢,𝑎)   𝐷(𝑦,𝑧,𝑢,𝑎)   𝑅(𝑎)   𝑈(𝑦,𝑢,𝑎)   𝐹(𝑦,𝑧,𝑢,𝑎)   𝐼(𝑦,𝑧,𝑢,𝑎)   𝐽(𝑢,𝑎)   𝐾(𝑢,𝑎)   𝐿(𝑎)   𝑀(𝑦,𝑢,𝑎)   𝑁(𝑦,𝑢,𝑎)   𝑂(𝑦,𝑢,𝑎)   𝑉(𝑦,𝑧,𝑎)   𝑊(𝑦,𝑢,𝑎)   𝑋(𝑢,𝑎)   𝑌(𝑦,𝑢,𝑎)   𝑍(𝑦,𝑎)

Proof of Theorem pntlemr
StepHypRef Expression
1 pntlem1.r . . . . . . . . . . . . 13 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
2 pntlem1.a . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ+)
3 pntlem1.b . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℝ+)
4 pntlem1.l . . . . . . . . . . . . 13 (𝜑𝐿 ∈ (0(,)1))
5 pntlem1.d . . . . . . . . . . . . 13 𝐷 = (𝐴 + 1)
6 pntlem1.f . . . . . . . . . . . . 13 𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))
71, 2, 3, 4, 5, 6pntlemd 26979 . . . . . . . . . . . 12 (𝜑 → (𝐿 ∈ ℝ+𝐷 ∈ ℝ+𝐹 ∈ ℝ+))
87simp1d 1142 . . . . . . . . . . 11 (𝜑𝐿 ∈ ℝ+)
9 pntlem1.u . . . . . . . . . . . . 13 (𝜑𝑈 ∈ ℝ+)
10 pntlem1.u2 . . . . . . . . . . . . 13 (𝜑𝑈𝐴)
11 pntlem1.e . . . . . . . . . . . . 13 𝐸 = (𝑈 / 𝐷)
12 pntlem1.k . . . . . . . . . . . . 13 𝐾 = (exp‘(𝐵 / 𝐸))
131, 2, 3, 4, 5, 6, 9, 10, 11, 12pntlemc 26980 . . . . . . . . . . . 12 (𝜑 → (𝐸 ∈ ℝ+𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+)))
1413simp1d 1142 . . . . . . . . . . 11 (𝜑𝐸 ∈ ℝ+)
158, 14rpmulcld 12982 . . . . . . . . . 10 (𝜑 → (𝐿 · 𝐸) ∈ ℝ+)
16 4re 12246 . . . . . . . . . . 11 4 ∈ ℝ
17 4pos 12269 . . . . . . . . . . 11 0 < 4
1816, 17elrpii 12927 . . . . . . . . . 10 4 ∈ ℝ+
19 rpdivcl 12949 . . . . . . . . . 10 (((𝐿 · 𝐸) ∈ ℝ+ ∧ 4 ∈ ℝ+) → ((𝐿 · 𝐸) / 4) ∈ ℝ+)
2015, 18, 19sylancl 586 . . . . . . . . 9 (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℝ+)
2120rpred 12966 . . . . . . . 8 (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℝ)
22 pntlem1.y . . . . . . . . . . . 12 (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))
23 pntlem1.x . . . . . . . . . . . 12 (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))
24 pntlem1.c . . . . . . . . . . . 12 (𝜑𝐶 ∈ ℝ+)
25 pntlem1.w . . . . . . . . . . . 12 𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))
26 pntlem1.z . . . . . . . . . . . 12 (𝜑𝑍 ∈ (𝑊[,)+∞))
271, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26pntlemb 26982 . . . . . . . . . . 11 (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))
2827simp1d 1142 . . . . . . . . . 10 (𝜑𝑍 ∈ ℝ+)
29 pntlem1.v . . . . . . . . . 10 (𝜑𝑉 ∈ ℝ+)
3028, 29rpdivcld 12983 . . . . . . . . 9 (𝜑 → (𝑍 / 𝑉) ∈ ℝ+)
3130rpred 12966 . . . . . . . 8 (𝜑 → (𝑍 / 𝑉) ∈ ℝ)
3221, 31remulcld 11194 . . . . . . 7 (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ)
33 pntlem1.i . . . . . . . . . 10 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))
34 fzfid 13888 . . . . . . . . . 10 (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ∈ Fin)
3533, 34eqeltrid 2836 . . . . . . . . 9 (𝜑𝐼 ∈ Fin)
36 hashcl 14266 . . . . . . . . 9 (𝐼 ∈ Fin → (♯‘𝐼) ∈ ℕ0)
3735, 36syl 17 . . . . . . . 8 (𝜑 → (♯‘𝐼) ∈ ℕ0)
3837nn0red 12483 . . . . . . 7 (𝜑 → (♯‘𝐼) ∈ ℝ)
3932recnd 11192 . . . . . . . . . . . 12 (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℂ)
40 1rp 12928 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ+
41 rpaddcl 12946 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (1 + (𝐿 · 𝐸)) ∈ ℝ+)
4240, 15, 41sylancr 587 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ+)
4342, 29rpmulcld 12982 . . . . . . . . . . . . . . . 16 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ+)
4428, 43rpdivcld 12983 . . . . . . . . . . . . . . 15 (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ+)
4544rpred 12966 . . . . . . . . . . . . . 14 (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ)
46 reflcl 13711 . . . . . . . . . . . . . 14 ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
4745, 46syl 17 . . . . . . . . . . . . 13 (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
4847recnd 11192 . . . . . . . . . . . 12 (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℂ)
49 1cnd 11159 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
5039, 48, 49add32d 11391 . . . . . . . . . . 11 (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) = (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
51 peano2re 11337 . . . . . . . . . . . . . 14 ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ)
5232, 51syl 17 . . . . . . . . . . . . 13 (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ)
5352, 47readdcld 11193 . . . . . . . . . . . 12 (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ)
54 reflcl 13711 . . . . . . . . . . . . . 14 ((𝑍 / 𝑉) ∈ ℝ → (⌊‘(𝑍 / 𝑉)) ∈ ℝ)
5531, 54syl 17 . . . . . . . . . . . . 13 (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℝ)
56 peano2re 11337 . . . . . . . . . . . . 13 ((⌊‘(𝑍 / 𝑉)) ∈ ℝ → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ)
5755, 56syl 17 . . . . . . . . . . . 12 (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ)
5815rphalfcld 12978 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ+)
5958, 30rpmulcld 12982 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ+)
6059rpred 12966 . . . . . . . . . . . . . 14 (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ)
6160, 45readdcld 11193 . . . . . . . . . . . . 13 (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
62 rpdivcl 12949 . . . . . . . . . . . . . . . . . . . 20 ((4 ∈ ℝ+ ∧ (𝐿 · 𝐸) ∈ ℝ+) → (4 / (𝐿 · 𝐸)) ∈ ℝ+)
6318, 15, 62sylancr 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ+)
6463rpred 12966 . . . . . . . . . . . . . . . . . 18 (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ)
6528rpsqrtcld 15308 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (√‘𝑍) ∈ ℝ+)
6665rpred 12966 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (√‘𝑍) ∈ ℝ)
6727simp3d 1144 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍))))
6867simp1d 1142 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (√‘𝑍))
6943rpred 12966 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ)
7013simp2d 1143 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐾 ∈ ℝ+)
71 pntlem1.j . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐽 ∈ (𝑀..^𝑁))
72 elfzoelz 13582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ)
7371, 72syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐽 ∈ ℤ)
7473peano2zd 12619 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐽 + 1) ∈ ℤ)
7570, 74rpexpcld 14160 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ+)
7675rpred 12966 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ)
77 pntlem1.V . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (((𝐾𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))
7877simplrd 768 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾𝐽)))
7970rpcnd 12968 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐾 ∈ ℂ)
8070, 73rpexpcld 14160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝐾𝐽) ∈ ℝ+)
8180rpcnd 12968 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐾𝐽) ∈ ℂ)
8279, 81mulcomd 11185 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐾 · (𝐾𝐽)) = ((𝐾𝐽) · 𝐾))
83 pntlem1.m . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)
84 pntlem1.n . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))
851, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 83, 84pntlemg 26983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀)))
8685simp1d 1142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑀 ∈ ℕ)
87 elfzouz 13586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ𝑀))
8871, 87syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝐽 ∈ (ℤ𝑀))
89 eluznn 12852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑀 ∈ ℕ ∧ 𝐽 ∈ (ℤ𝑀)) → 𝐽 ∈ ℕ)
9086, 88, 89syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐽 ∈ ℕ)
9190nnnn0d 12482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐽 ∈ ℕ0)
9279, 91expp1d 14062 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾𝐽) · 𝐾))
9382, 92eqtr4d 2774 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐾 · (𝐾𝐽)) = (𝐾↑(𝐽 + 1)))
9478, 93breqtrd 5136 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1)))
9569, 76, 94ltled 11312 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1)))
96 fzofzp1 13679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐽 ∈ (𝑀..^𝑁) → (𝐽 + 1) ∈ (𝑀...𝑁))
9771, 96syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐽 + 1) ∈ (𝑀...𝑁))
981, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 83, 84pntlemh 26984 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝐽 + 1) ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
9997, 98mpdan 685 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
10099simprd 496 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))
10169, 76, 66, 95, 100letrd 11321 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍))
10269, 66, 65lemul2d 13010 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍) ↔ ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍))))
103101, 102mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍)))
10428rprege0d 12973 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍))
105 remsqsqrt 15153 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
106104, 105syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
107103, 106breqtrd 5136 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍)
10828rpred 12966 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑍 ∈ ℝ)
10966, 108, 43lemuldivd 13015 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍 ↔ (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
110107, 109mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
11129rpcnd 12968 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑉 ∈ ℂ)
112111mullidd 11182 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 · 𝑉) = 𝑉)
113 1red 11165 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ ℝ)
11442rpred 12966 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ)
115 1re 11164 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℝ
116 ltaddrp 12961 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 ∈ ℝ ∧ (𝐿 · 𝐸) ∈ ℝ+) → 1 < (1 + (𝐿 · 𝐸)))
117115, 15, 116sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 < (1 + (𝐿 · 𝐸)))
118113, 114, 29, 117ltmul1dd 13021 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 · 𝑉) < ((1 + (𝐿 · 𝐸)) · 𝑉))
119112, 118eqbrtrrd 5134 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉))
12029, 43, 28ltdiv2d 12989 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉) ↔ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉)))
121119, 120mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉))
12245, 31, 121ltled 11312 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉))
12366, 45, 31, 110, 122letrd 11321 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (√‘𝑍) ≤ (𝑍 / 𝑉))
12464, 66, 31, 68, 123letrd 11321 . . . . . . . . . . . . . . . . . 18 (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (𝑍 / 𝑉))
12564, 31, 31, 124leadd2dd 11779 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ ((𝑍 / 𝑉) + (𝑍 / 𝑉)))
12630rpcnd 12968 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑍 / 𝑉) ∈ ℂ)
1271262timesd 12405 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 · (𝑍 / 𝑉)) = ((𝑍 / 𝑉) + (𝑍 / 𝑉)))
128125, 127breqtrrd 5138 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)))
12931, 64readdcld 11193 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ∈ ℝ)
130 2re 12236 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
131 remulcl 11145 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ) → (2 · (𝑍 / 𝑉)) ∈ ℝ)
132130, 31, 131sylancr 587 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 · (𝑍 / 𝑉)) ∈ ℝ)
133129, 132, 20lemul2d 13010 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉)))))
134128, 133mpbid 231 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))
13520rpcnd 12968 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℂ)
13663rpcnd 12968 . . . . . . . . . . . . . . . . 17 (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℂ)
137135, 126, 136adddid 11188 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))))
13815rpcnne0d 12975 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0))
139 rpcnne0 12942 . . . . . . . . . . . . . . . . . . 19 (4 ∈ ℝ+ → (4 ∈ ℂ ∧ 4 ≠ 0))
14018, 139mp1i 13 . . . . . . . . . . . . . . . . . 18 (𝜑 → (4 ∈ ℂ ∧ 4 ≠ 0))
141 divcan6 11871 . . . . . . . . . . . . . . . . . 18 ((((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0) ∧ (4 ∈ ℂ ∧ 4 ≠ 0)) → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1)
142138, 140, 141syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1)
143142oveq2d 7378 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1))
144137, 143eqtrd 2771 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1))
145 2cnd 12240 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℂ)
146135, 145, 126mulassd 11187 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))
14715rpcnd 12968 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 · 𝐸) ∈ ℂ)
148 2rp 12929 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℝ+
149 rpcnne0 12942 . . . . . . . . . . . . . . . . . . . . . 22 (2 ∈ ℝ+ → (2 ∈ ℂ ∧ 2 ≠ 0))
150148, 149mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 ∈ ℂ ∧ 2 ≠ 0))
151 divdiv1 11875 . . . . . . . . . . . . . . . . . . . . 21 (((𝐿 · 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2)))
152147, 150, 150, 151syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2)))
153 2t2e4 12326 . . . . . . . . . . . . . . . . . . . . 21 (2 · 2) = 4
154153oveq2i 7373 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 · 𝐸) / (2 · 2)) = ((𝐿 · 𝐸) / 4)
155152, 154eqtr2di 2788 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐿 · 𝐸) / 4) = (((𝐿 · 𝐸) / 2) / 2))
156155oveq1d 7377 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((((𝐿 · 𝐸) / 2) / 2) · 2))
157147halfcld 12407 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℂ)
158150simprd 496 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 2 ≠ 0)
159157, 145, 158divcan1d 11941 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝐿 · 𝐸) / 2) / 2) · 2) = ((𝐿 · 𝐸) / 2))
160156, 159eqtrd 2771 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((𝐿 · 𝐸) / 2))
161160oveq1d 7377 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
162146, 161eqtr3d 2773 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
163134, 144, 1623brtr3d 5141 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ≤ (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
164 flle 13714 . . . . . . . . . . . . . . 15 ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
16545, 164syl 17 . . . . . . . . . . . . . 14 (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
16652, 47, 60, 45, 163, 165le2addd 11783 . . . . . . . . . . . . 13 (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ≤ ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
16758rpred 12966 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ)
16842rprecred 12977 . . . . . . . . . . . . . . . 16 (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℝ)
169167, 168readdcld 11193 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) ∈ ℝ)
17015rpred 12966 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐿 · 𝐸) ∈ ℝ)
17114rpred 12966 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐸 ∈ ℝ)
1728rpred 12966 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐿 ∈ ℝ)
173 eliooord 13333 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐿 ∈ (0(,)1) → (0 < 𝐿𝐿 < 1))
1744, 173syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (0 < 𝐿𝐿 < 1))
175174simprd 496 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐿 < 1)
176172, 113, 14, 175ltmul1dd 13021 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐿 · 𝐸) < (1 · 𝐸))
17714rpcnd 12968 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐸 ∈ ℂ)
178177mullidd 11182 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1 · 𝐸) = 𝐸)
179176, 178breqtrd 5136 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 · 𝐸) < 𝐸)
18013simp3d 1144 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+))
181180simp1d 1142 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐸 ∈ (0(,)1))
182 eliooord 13333 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐸 ∈ (0(,)1) → (0 < 𝐸𝐸 < 1))
183181, 182syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0 < 𝐸𝐸 < 1))
184183simprd 496 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐸 < 1)
185170, 171, 113, 179, 184lttrd 11325 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐿 · 𝐸) < 1)
186170, 113, 113, 185ltadd2dd 11323 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1 + (𝐿 · 𝐸)) < (1 + 1))
187 df-2 12225 . . . . . . . . . . . . . . . . . . 19 2 = (1 + 1)
188186, 187breqtrrdi 5152 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 + (𝐿 · 𝐸)) < 2)
18942rpregt0d 12972 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸))))
190130a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 2 ∈ ℝ)
191 2pos 12265 . . . . . . . . . . . . . . . . . . . 20 0 < 2
192191a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 2)
19315rpregt0d 12972 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸)))
194 ltdiv2 12050 . . . . . . . . . . . . . . . . . . 19 ((((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸))) ∧ (2 ∈ ℝ ∧ 0 < 2) ∧ ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸))) → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))))
195189, 190, 192, 193, 194syl121anc 1375 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))))
196188, 195mpbid 231 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))
19742rpcnd 12968 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℂ)
19842rpcnne0d 12975 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0))
199 divsubdir 11858 . . . . . . . . . . . . . . . . . . 19 (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ 1 ∈ ℂ ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))))
200197, 49, 198, 199syl3anc 1371 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))))
201 ax-1cn 11118 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℂ
202 pncan2 11417 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℂ ∧ (𝐿 · 𝐸) ∈ ℂ) → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸))
203201, 147, 202sylancr 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸))
204203oveq1d 7377 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))
205 divid 11851 . . . . . . . . . . . . . . . . . . . 20 (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0) → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1)
206198, 205syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1)
207206oveq1d 7377 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))) = (1 − (1 / (1 + (𝐿 · 𝐸)))))
208200, 204, 2073eqtr3d 2779 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))) = (1 − (1 / (1 + (𝐿 · 𝐸)))))
209196, 208breqtrd 5136 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸)))))
210167, 168, 113ltaddsubd 11764 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1 ↔ ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸))))))
211209, 210mpbird 256 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1)
212169, 113, 30, 211ltmul1dd 13021 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) < (1 · (𝑍 / 𝑉)))
213 reccl 11829 . . . . . . . . . . . . . . . . 17 (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0) → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ)
214198, 213syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ)
215157, 214, 126adddird 11189 . . . . . . . . . . . . . . 15 (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))))
216197, 111mulcomd 11185 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) = (𝑉 · (1 + (𝐿 · 𝐸))))
217216oveq2d 7378 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
21828rpcnd 12968 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍 ∈ ℂ)
21929rpcnne0d 12975 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0))
220 divdiv1 11875 . . . . . . . . . . . . . . . . . 18 ((𝑍 ∈ ℂ ∧ (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0) ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
221218, 219, 198, 220syl3anc 1371 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
22242rpne0d 12971 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 + (𝐿 · 𝐸)) ≠ 0)
223126, 197, 222divrec2d 11944 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))
224217, 221, 2233eqtr2d 2777 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))
225224oveq2d 7378 . . . . . . . . . . . . . . 15 (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))))
226215, 225eqtr4d 2774 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
227126mullidd 11182 . . . . . . . . . . . . . 14 (𝜑 → (1 · (𝑍 / 𝑉)) = (𝑍 / 𝑉))
228212, 226, 2273brtr3d 5141 . . . . . . . . . . . . 13 (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) < (𝑍 / 𝑉))
22953, 61, 31, 166, 228lelttrd 11322 . . . . . . . . . . . 12 (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (𝑍 / 𝑉))
230 fllep1 13716 . . . . . . . . . . . . 13 ((𝑍 / 𝑉) ∈ ℝ → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1))
23131, 230syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1))
23253, 31, 57, 229, 231ltletrd 11324 . . . . . . . . . . 11 (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < ((⌊‘(𝑍 / 𝑉)) + 1))
23350, 232eqbrtrd 5132 . . . . . . . . . 10 (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1))
23432, 47readdcld 11193 . . . . . . . . . . 11 (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ)
235234, 55, 113ltadd1d 11757 . . . . . . . . . 10 (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1)))
236233, 235mpbird 256 . . . . . . . . 9 (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)))
23732, 47, 55ltaddsubd 11764 . . . . . . . . 9 (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))))
238236, 237mpbid 231 . . . . . . . 8 (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
23931flcld 13713 . . . . . . . . . . . 12 (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℤ)
240 fzval3 13651 . . . . . . . . . . . 12 ((⌊‘(𝑍 / 𝑉)) ∈ ℤ → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
241239, 240syl 17 . . . . . . . . . . 11 (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
24233, 241eqtrid 2783 . . . . . . . . . 10 (𝜑𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
243242fveq2d 6851 . . . . . . . . 9 (𝜑 → (♯‘𝐼) = (♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))))
244 flword2 13728 . . . . . . . . . . . 12 (((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ ∧ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉)) → (⌊‘(𝑍 / 𝑉)) ∈ (ℤ‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
24545, 31, 122, 244syl3anc 1371 . . . . . . . . . . 11 (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ (ℤ‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
246 eluzp1p1 12800 . . . . . . . . . . 11 ((⌊‘(𝑍 / 𝑉)) ∈ (ℤ‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
247245, 246syl 17 . . . . . . . . . 10 (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
248 hashfzo 14339 . . . . . . . . . 10 (((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) → (♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) = (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
249247, 248syl 17 . . . . . . . . 9 (𝜑 → (♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) = (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
25055recnd 11192 . . . . . . . . . 10 (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℂ)
251250, 48, 49pnpcan2d 11559 . . . . . . . . 9 (𝜑 → (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
252243, 249, 2513eqtrd 2775 . . . . . . . 8 (𝜑 → (♯‘𝐼) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
253238, 252breqtrrd 5138 . . . . . . 7 (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < (♯‘𝐼))
25432, 38, 253ltled 11312 . . . . . 6 (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼))
25521, 38, 30lemuldivd 13015 . . . . . 6 (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼) ↔ ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉))))
256254, 255mpbid 231 . . . . 5 (𝜑 → ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)))
25729rpred 12966 . . . . . . . . . . . . . . 15 (𝜑𝑉 ∈ ℝ)
25869, 76, 66, 94, 100ltletrd 11324 . . . . . . . . . . . . . . . 16 (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (√‘𝑍))
259257, 69, 66, 119, 258lttrd 11325 . . . . . . . . . . . . . . 15 (𝜑𝑉 < (√‘𝑍))
260257, 66, 259ltled 11312 . . . . . . . . . . . . . 14 (𝜑𝑉 ≤ (√‘𝑍))
26129rprege0d 12973 . . . . . . . . . . . . . . 15 (𝜑 → (𝑉 ∈ ℝ ∧ 0 ≤ 𝑉))
26265rprege0d 12973 . . . . . . . . . . . . . . 15 (𝜑 → ((√‘𝑍) ∈ ℝ ∧ 0 ≤ (√‘𝑍)))
263 le2sq 14049 . . . . . . . . . . . . . . 15 (((𝑉 ∈ ℝ ∧ 0 ≤ 𝑉) ∧ ((√‘𝑍) ∈ ℝ ∧ 0 ≤ (√‘𝑍))) → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2)))
264261, 262, 263syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2)))
265260, 264mpbid 231 . . . . . . . . . . . . 13 (𝜑 → (𝑉↑2) ≤ ((√‘𝑍)↑2))
266 resqrtth 15152 . . . . . . . . . . . . . 14 ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍)↑2) = 𝑍)
267104, 266syl 17 . . . . . . . . . . . . 13 (𝜑 → ((√‘𝑍)↑2) = 𝑍)
268265, 267breqtrd 5136 . . . . . . . . . . . 12 (𝜑 → (𝑉↑2) ≤ 𝑍)
269 2z 12544 . . . . . . . . . . . . . . 15 2 ∈ ℤ
270 rpexpcl 13996 . . . . . . . . . . . . . . 15 ((𝑉 ∈ ℝ+ ∧ 2 ∈ ℤ) → (𝑉↑2) ∈ ℝ+)
27129, 269, 270sylancl 586 . . . . . . . . . . . . . 14 (𝜑 → (𝑉↑2) ∈ ℝ+)
272271rpred 12966 . . . . . . . . . . . . 13 (𝜑 → (𝑉↑2) ∈ ℝ)
273272, 108, 28lemul2d 13010 . . . . . . . . . . . 12 (𝜑 → ((𝑉↑2) ≤ 𝑍 ↔ (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍)))
274268, 273mpbid 231 . . . . . . . . . . 11 (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍))
275218sqvald 14058 . . . . . . . . . . 11 (𝜑 → (𝑍↑2) = (𝑍 · 𝑍))
276274, 275breqtrrd 5138 . . . . . . . . . 10 (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍↑2))
277108resqcld 14040 . . . . . . . . . . 11 (𝜑 → (𝑍↑2) ∈ ℝ)
278108, 277, 271lemuldivd 13015 . . . . . . . . . 10 (𝜑 → ((𝑍 · (𝑉↑2)) ≤ (𝑍↑2) ↔ 𝑍 ≤ ((𝑍↑2) / (𝑉↑2))))
279276, 278mpbid 231 . . . . . . . . 9 (𝜑𝑍 ≤ ((𝑍↑2) / (𝑉↑2)))
28029rpne0d 12971 . . . . . . . . . 10 (𝜑𝑉 ≠ 0)
281218, 111, 280sqdivd 14074 . . . . . . . . 9 (𝜑 → ((𝑍 / 𝑉)↑2) = ((𝑍↑2) / (𝑉↑2)))
282279, 281breqtrrd 5138 . . . . . . . 8 (𝜑𝑍 ≤ ((𝑍 / 𝑉)↑2))
283 rpexpcl 13996 . . . . . . . . . 10 (((𝑍 / 𝑉) ∈ ℝ+ ∧ 2 ∈ ℤ) → ((𝑍 / 𝑉)↑2) ∈ ℝ+)
28430, 269, 283sylancl 586 . . . . . . . . 9 (𝜑 → ((𝑍 / 𝑉)↑2) ∈ ℝ+)
28528, 284logled 26019 . . . . . . . 8 (𝜑 → (𝑍 ≤ ((𝑍 / 𝑉)↑2) ↔ (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2))))
286282, 285mpbid 231 . . . . . . 7 (𝜑 → (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2)))
287 relogexp 25988 . . . . . . . 8 (((𝑍 / 𝑉) ∈ ℝ+ ∧ 2 ∈ ℤ) → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉))))
28830, 269, 287sylancl 586 . . . . . . 7 (𝜑 → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉))))
289286, 288breqtrd 5136 . . . . . 6 (𝜑 → (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉))))
29028relogcld 26015 . . . . . . 7 (𝜑 → (log‘𝑍) ∈ ℝ)
29130relogcld 26015 . . . . . . 7 (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℝ)
292 ledivmul 12040 . . . . . . 7 (((log‘𝑍) ∈ ℝ ∧ (log‘(𝑍 / 𝑉)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉)))))
293290, 291, 190, 192, 292syl112anc 1374 . . . . . 6 (𝜑 → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉)))))
294289, 293mpbird 256 . . . . 5 (𝜑 → ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)))
29520rprege0d 12973 . . . . . 6 (𝜑 → (((𝐿 · 𝐸) / 4) ∈ ℝ ∧ 0 ≤ ((𝐿 · 𝐸) / 4)))
29638, 30rerpdivcld 12997 . . . . . 6 (𝜑 → ((♯‘𝐼) / (𝑍 / 𝑉)) ∈ ℝ)
29727simp2d 1143 . . . . . . . . . 10 (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
298297simp1d 1142 . . . . . . . . 9 (𝜑 → 1 < 𝑍)
299108, 298rplogcld 26021 . . . . . . . 8 (𝜑 → (log‘𝑍) ∈ ℝ+)
300299rphalfcld 12978 . . . . . . 7 (𝜑 → ((log‘𝑍) / 2) ∈ ℝ+)
301300rprege0d 12973 . . . . . 6 (𝜑 → (((log‘𝑍) / 2) ∈ ℝ ∧ 0 ≤ ((log‘𝑍) / 2)))
302 lemul12a 12022 . . . . . 6 ((((((𝐿 · 𝐸) / 4) ∈ ℝ ∧ 0 ≤ ((𝐿 · 𝐸) / 4)) ∧ ((♯‘𝐼) / (𝑍 / 𝑉)) ∈ ℝ) ∧ ((((log‘𝑍) / 2) ∈ ℝ ∧ 0 ≤ ((log‘𝑍) / 2)) ∧ (log‘(𝑍 / 𝑉)) ∈ ℝ)) → ((((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)) ∧ ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))))
303295, 296, 301, 291, 302syl22anc 837 . . . . 5 (𝜑 → ((((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)) ∧ ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))))
304256, 294, 303mp2and 697 . . . 4 (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
305299rpcnd 12968 . . . . . 6 (𝜑 → (log‘𝑍) ∈ ℂ)
306 8nn 12257 . . . . . . . 8 8 ∈ ℕ
307 nnrp 12935 . . . . . . . 8 (8 ∈ ℕ → 8 ∈ ℝ+)
308306, 307ax-mp 5 . . . . . . 7 8 ∈ ℝ+
309 rpcnne0 12942 . . . . . . 7 (8 ∈ ℝ+ → (8 ∈ ℂ ∧ 8 ≠ 0))
310308, 309mp1i 13 . . . . . 6 (𝜑 → (8 ∈ ℂ ∧ 8 ≠ 0))
311 div23 11841 . . . . . 6 (((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0)) → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍)))
312147, 305, 310, 311syl3anc 1371 . . . . 5 (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍)))
313 divmuldiv 11864 . . . . . . 7 ((((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)))
314147, 305, 140, 150, 313syl22anc 837 . . . . . 6 (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)))
315 4t2e8 12330 . . . . . . 7 (4 · 2) = 8
316315oveq2i 7373 . . . . . 6 (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / 8)
317314, 316eqtr2di 2788 . . . . 5 (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)))
318312, 317eqtr3d 2773 . . . 4 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)))
31938recnd 11192 . . . . 5 (𝜑 → (♯‘𝐼) ∈ ℂ)
320291recnd 11192 . . . . 5 (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℂ)
32130rpcnne0d 12975 . . . . 5 (𝜑 → ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0))
322 divass 11840 . . . . . 6 (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))
323 div23 11841 . . . . . 6 (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
324322, 323eqtr3d 2773 . . . . 5 (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
325319, 320, 321, 324syl3anc 1371 . . . 4 (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
326304, 318, 3253brtr4d 5142 . . 3 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))
327 rpdivcl 12949 . . . . . . 7 (((𝐿 · 𝐸) ∈ ℝ+ ∧ 8 ∈ ℝ+) → ((𝐿 · 𝐸) / 8) ∈ ℝ+)
32815, 308, 327sylancl 586 . . . . . 6 (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℝ+)
329328, 299rpmulcld 12982 . . . . 5 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ+)
330329rpred 12966 . . . 4 (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ)
331291, 30rerpdivcld 12997 . . . . 5 (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ)
33238, 331remulcld 11194 . . . 4 (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
333180simp3d 1144 . . . 4 (𝜑 → (𝑈𝐸) ∈ ℝ+)
334330, 332, 333lemul2d 13010 . . 3 (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ↔ ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))))
335326, 334mpbid 231 . 2 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
336333rpcnd 12968 . . 3 (𝜑 → (𝑈𝐸) ∈ ℂ)
337331recnd 11192 . . 3 (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℂ)
338336, 319, 337mul12d 11373 . 2 (𝜑 → ((𝑈𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) = ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
339335, 338breqtrd 5136 1 (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((♯‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2939  wral 3060  wrex 3069   class class class wbr 5110  cmpt 5193  cfv 6501  (class class class)co 7362  Fincfn 8890  cc 11058  cr 11059  0cc0 11060  1c1 11061   + caddc 11063   · cmul 11065  +∞cpnf 11195   < clt 11198  cle 11199  cmin 11394   / cdiv 11821  cn 12162  2c2 12217  3c3 12218  4c4 12219  8c8 12223  0cn0 12422  cz 12508  cdc 12627  cuz 12772  +crp 12924  (,)cioo 13274  [,)cico 13276  [,]cicc 13277  ...cfz 13434  ..^cfzo 13577  cfl 13705  cexp 13977  chash 14240  csqrt 15130  abscabs 15131  expce 15955  eceu 15956  logclog 25947  ψcchp 26479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9586  ax-cnex 11116  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1ne0 11129  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136  ax-pre-mulgt0 11137  ax-pre-sup 11138  ax-addf 11139  ax-mulf 11140
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9356  df-sup 9387  df-inf 9388  df-oi 9455  df-card 9884  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204  df-sub 11396  df-neg 11397  df-div 11822  df-nn 12163  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229  df-7 12230  df-8 12231  df-9 12232  df-n0 12423  df-z 12509  df-dec 12628  df-uz 12773  df-q 12883  df-rp 12925  df-xneg 13042  df-xadd 13043  df-xmul 13044  df-ioo 13278  df-ioc 13279  df-ico 13280  df-icc 13281  df-fz 13435  df-fzo 13578  df-fl 13707  df-mod 13785  df-seq 13917  df-exp 13978  df-fac 14184  df-bc 14213  df-hash 14241  df-shft 14964  df-cj 14996  df-re 14997  df-im 14998  df-sqrt 15132  df-abs 15133  df-limsup 15365  df-clim 15382  df-rlim 15383  df-sum 15583  df-ef 15961  df-e 15962  df-sin 15963  df-cos 15964  df-pi 15966  df-struct 17030  df-sets 17047  df-slot 17065  df-ndx 17077  df-base 17095  df-ress 17124  df-plusg 17160  df-mulr 17161  df-starv 17162  df-sca 17163  df-vsca 17164  df-ip 17165  df-tset 17166  df-ple 17167  df-ds 17169  df-unif 17170  df-hom 17171  df-cco 17172  df-rest 17318  df-topn 17319  df-0g 17337  df-gsum 17338  df-topgen 17339  df-pt 17340  df-prds 17343  df-xrs 17398  df-qtop 17403  df-imas 17404  df-xps 17406  df-mre 17480  df-mrc 17481  df-acs 17483  df-mgm 18511  df-sgrp 18560  df-mnd 18571  df-submnd 18616  df-mulg 18887  df-cntz 19111  df-cmn 19578  df-psmet 20825  df-xmet 20826  df-met 20827  df-bl 20828  df-mopn 20829  df-fbas 20830  df-fg 20831  df-cnfld 20834  df-top 22280  df-topon 22297  df-topsp 22319  df-bases 22333  df-cld 22407  df-ntr 22408  df-cls 22409  df-nei 22486  df-lp 22524  df-perf 22525  df-cn 22615  df-cnp 22616  df-haus 22703  df-tx 22950  df-hmeo 23143  df-fil 23234  df-fm 23326  df-flim 23327  df-flf 23328  df-xms 23710  df-ms 23711  df-tms 23712  df-cncf 24278  df-limc 25267  df-dv 25268  df-log 25949
This theorem is referenced by:  pntlemj  26988
  Copyright terms: Public domain W3C validator