pntlemr - Metamath Proof Explorer

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

Theorem pntlemr 27720

Description: Lemma for pntlemj 27721. (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**
Step	Hyp	Ref	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)))
7	1, 2, 3, 4, 5, 6	pntlemd 27712	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 ∈ ℝ⁺ ∧ 𝐷 ∈ ℝ⁺ ∧ 𝐹 ∈ ℝ⁺))
8	7	simp1d 1158	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 ∈ ℝ⁺)
9		pntlem1.u	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ∈ ℝ⁺)
10		pntlem1.u2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑈 ≤ 𝐴)
11		pntlem1.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (𝑈 / 𝐷)
12		pntlem1.k	. . . . . . . . . . . . 13 ⊢ 𝐾 = (exp‘(𝐵 / 𝐸))
13	1, 2, 3, 4, 5, 6, 9, 10, 11, 12	pntlemc 27713	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∈ ℝ⁺ ∧ 𝐾 ∈ ℝ⁺ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈ ℝ⁺)))
14	13	simp1d 1158	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
15	8, 14	rpmulcld 13064	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ⁺)
16		4re 12313	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
17		4pos 12339	. . . . . . . . . . 11 ⊢ 0 < 4
18	16, 17	elrpii 13007	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
19		rpdivcl 13031	. . . . . . . . . 10 ⊢ (((𝐿 · 𝐸) ∈ ℝ⁺ ∧ 4 ∈ ℝ⁺) → ((𝐿 · 𝐸) / 4) ∈ ℝ⁺)
20	15, 18, 19	sylancl 597	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℝ⁺)
21	20	rpred 13048	. . . . . . . 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 ⊢ (𝜑 → 𝑍 ∈ (𝑊[,)+∞))
27	1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26	pntlemb 27715	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 ∈ ℝ⁺ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))))
28	27	simp1d 1158	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ ℝ⁺)
29		pntlem1.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ℝ⁺)
30	28, 29	rpdivcld 13065	. . . . . . . . 9 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ⁺)
31	30	rpred 13048	. . . . . . . 8 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ)
32	21, 31	remulcld 11227	. . . . . . 7 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ)
33		pntlem1.i	. . . . . . . . . 10 ⊢ 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))
34		fzfid 13997	. . . . . . . . . 10 ⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ∈ Fin)
35	33, 34	eqeltrid 2869	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ Fin)
36		hashcl 14380	. . . . . . . . 9 ⊢ (𝐼 ∈ Fin → (♯‘𝐼) ∈ ℕ₀)
37	35, 36	syl 18	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐼) ∈ ℕ₀)
38	37	nn0red 12554	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐼) ∈ ℝ)
39	32	recnd 11225	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℂ)
40		1rp 13008	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ⁺
41		rpaddcl 13028	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ⁺ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → (1 + (𝐿 · 𝐸)) ∈ ℝ⁺)
42	40, 15, 41	sylancr 598	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ⁺)
43	42, 29	rpmulcld 13064	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ⁺)
44	28, 43	rpdivcld 13065	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ⁺)
45	44	rpred 13048	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ)
46		reflcl 13817	. . . . . . . . . . . . . 14 ⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
47	45, 46	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
48	47	recnd 11225	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℂ)
49		1cnd 11190	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
50	39, 48, 49	add32d 11426	. . . . . . . . . . 11 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) = (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
51		peano2re 11371	. . . . . . . . . . . . . 14 ⊢ ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ)
52	32, 51	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ)
53	52, 47	readdcld 11226	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ)
54		reflcl 13817	. . . . . . . . . . . . . 14 ⊢ ((𝑍 / 𝑉) ∈ ℝ → (⌊‘(𝑍 / 𝑉)) ∈ ℝ)
55	31, 54	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℝ)
56		peano2re 11371	. . . . . . . . . . . . 13 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ ℝ → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ)
57	55, 56	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ)
58	15	rphalfcld 13060	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ⁺)
59	58, 30	rpmulcld 13064	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ⁺)
60	59	rpred 13048	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ)
61	60, 45	readdcld 11226	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
62		rpdivcl 13031	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((4 ∈ ℝ⁺ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → (4 / (𝐿 · 𝐸)) ∈ ℝ⁺)
63	18, 15, 62	sylancr 598	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ⁺)
64	63	rpred 13048	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ)
65	28	rpsqrtcld 15451	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑍) ∈ ℝ⁺)
66	65	rpred 13048	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (√‘𝑍) ∈ ℝ)
67	27	simp3d 1160	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))
68	67	simp1d 1158	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (√‘𝑍))
69	43	rpred 13048	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ)
70	13	simp2d 1159	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐾 ∈ ℝ⁺)
71		pntlem1.j	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 ∈ (𝑀..^𝑁))
72		elfzoelz 13675	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ)
73	71, 72	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐽 ∈ ℤ)
74	73	peano2zd 12691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐽 + 1) ∈ ℤ)
75	70, 74	rpexpcld 14271	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ⁺)
76	75	rpred 13048	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ)
77		pntlem1.V	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
78	77	simplrd 781	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽)))
79	70	rpcnd 13050	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐾 ∈ ℂ)
80	70, 73	rpexpcld 14271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝐾↑𝐽) ∈ ℝ⁺)
81	80	rpcnd 13050	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐾↑𝐽) ∈ ℂ)
82	79, 81	mulcomd 11218	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = ((𝐾↑𝐽) · 𝐾))
83		pntlem1.m	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)
84		pntlem1.n	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))
85	1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 83, 84	pntlemg 27716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ_≥‘𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀)))
86	85	simp1d 1158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ ℕ)
87		elfzouz 13680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ_≥‘𝑀))
88	71, 87	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝐽 ∈ (ℤ_≥‘𝑀))
89		eluznn 12930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑀 ∈ ℕ ∧ 𝐽 ∈ (ℤ_≥‘𝑀)) → 𝐽 ∈ ℕ)
90	86, 88, 89	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐽 ∈ ℕ)
91	90	nnnn0d 12553	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
92	79, 91	expp1d 14171	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾↑𝐽) · 𝐾))
93	82, 92	eqtr4d 2803	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = (𝐾↑(𝐽 + 1)))
94	78, 93	breqtrd 5130	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1)))
95	69, 76, 94	ltled 11346	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1)))
96		fzofzp1 13781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐽 ∈ (𝑀..^𝑁) → (𝐽 + 1) ∈ (𝑀...𝑁))
97	71, 96	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐽 + 1) ∈ (𝑀...𝑁))
98	1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 83, 84	pntlemh 27717	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝐽 + 1) ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
99	97, 98	mpdan 699	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
100	99	simprd 500	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))
101	69, 76, 66, 95, 100	letrd 11355	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍))
102	69, 66, 65	lemul2d 13092	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍) ↔ ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍))))
103	101, 102	mpbid 235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍)))
104	28	rprege0d 13055	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍))
105		remsqsqrt 15295	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
106	104, 105	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
107	103, 106	breqtrd 5130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍)
108	28	rpred 13048	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑍 ∈ ℝ)
109	66, 108, 43	lemuldivd 13097	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍 ↔ (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
110	107, 109	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
111	29	rpcnd 13050	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑉 ∈ ℂ)
112	111	mullidd 11215	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑉) = 𝑉)
113		1red 11197	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℝ)
114	42	rpred 13048	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ)
115		1re 11196	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℝ
116		ltaddrp 13043	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1 ∈ ℝ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → 1 < (1 + (𝐿 · 𝐸)))
117	115, 15, 116	sylancr 598	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 < (1 + (𝐿 · 𝐸)))
118	113, 114, 29, 117	ltmul1dd 13103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑉) < ((1 + (𝐿 · 𝐸)) · 𝑉))
119	112, 118	eqbrtrrd 5128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉))
120	29, 43, 28	ltdiv2d 13071	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉) ↔ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉)))
121	119, 120	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉))
122	45, 31, 121	ltled 11346	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉))
123	66, 45, 31, 110, 122	letrd 11355	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / 𝑉))
124	64, 66, 31, 68, 123	letrd 11355	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (𝑍 / 𝑉))
125	64, 31, 31, 124	leadd2dd 11817	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ ((𝑍 / 𝑉) + (𝑍 / 𝑉)))
126	30	rpcnd 13050	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℂ)
127	126	2timesd 12475	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑍 / 𝑉)) = ((𝑍 / 𝑉) + (𝑍 / 𝑉)))
128	125, 127	breqtrrd 5132	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)))
129	31, 64	readdcld 11226	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ∈ ℝ)
130		2re 12303	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
131		remulcl 11173	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ) → (2 · (𝑍 / 𝑉)) ∈ ℝ)
132	130, 31, 131	sylancr 598	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑍 / 𝑉)) ∈ ℝ)
133	129, 132, 20	lemul2d 13092	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉)))))
134	128, 133	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))
135	20	rpcnd 13050	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℂ)
136	63	rpcnd 13050	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℂ)
137	135, 126, 136	adddid 11221	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))))
138	15	rpcnne0d 13057	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0))
139		rpcnne0 13023	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 ∈ ℝ⁺ → (4 ∈ ℂ ∧ 4 ≠ 0))
140	18, 139	mp1i 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 ∈ ℂ ∧ 4 ≠ 0))
141		divcan6 11910	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0) ∧ (4 ∈ ℂ ∧ 4 ≠ 0)) → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1)
142	138, 140, 141	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1)
143	142	oveq2d 7416	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1))
144	137, 143	eqtrd 2800	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1))
145		2cnd 12307	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℂ)
146	135, 145, 126	mulassd 11220	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))
147	15	rpcnd 13050	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℂ)
148		2rp 13009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ⁺
149		rpcnne0 13023	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 ∈ ℝ⁺ → (2 ∈ ℂ ∧ 2 ≠ 0))
150	148, 149	mp1i 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2 ∈ ℂ ∧ 2 ≠ 0))
151		divdiv1 11914	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2)))
152	147, 150, 150, 151	syl3anc 1394	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2)))
153		2t2e4 12392	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 · 2) = 4
154	153	oveq2i 7411	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐿 · 𝐸) / (2 · 2)) = ((𝐿 · 𝐸) / 4)
155	152, 154	eqtr2di 2817	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) = (((𝐿 · 𝐸) / 2) / 2))
156	155	oveq1d 7415	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((((𝐿 · 𝐸) / 2) / 2) · 2))
157	147	halfcld 12477	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℂ)
158	150	simprd 500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 2 ≠ 0)
159	157, 145, 158	divcan1d 11980	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) / 2) · 2) = ((𝐿 · 𝐸) / 2))
160	156, 159	eqtrd 2800	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((𝐿 · 𝐸) / 2))
161	160	oveq1d 7415	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
162	146, 161	eqtr3d 2802	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
163	134, 144, 162	3brtr3d 5135	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ≤ (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
164		flle 13820	. . . . . . . . . . . . . . 15 ⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
165	45, 164	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
166	52, 47, 60, 45, 163, 165	le2addd 11821	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ≤ ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
167	58	rpred 13048	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ)
168	42	rprecred 13059	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℝ)
169	167, 168	readdcld 11226	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) ∈ ℝ)
170	15	rpred 13048	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ)
171	14	rpred 13048	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 ∈ ℝ)
172	8	rpred 13048	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 ∈ ℝ)
173		eliooord 13420	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ (0(,)1) → (0 < 𝐿 ∧ 𝐿 < 1))
174	4, 173	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (0 < 𝐿 ∧ 𝐿 < 1))
175	174	simprd 500	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 < 1)
176	172, 113, 14, 175	ltmul1dd 13103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐿 · 𝐸) < (1 · 𝐸))
177	14	rpcnd 13050	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 ∈ ℂ)
178	177	mullidd 11215	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1 · 𝐸) = 𝐸)
179	176, 178	breqtrd 5130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝐸) < 𝐸)
180	13	simp3d 1160	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈ ℝ⁺))
181	180	simp1d 1158	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 ∈ (0(,)1))
182		eliooord 13420	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐸 ∈ (0(,)1) → (0 < 𝐸 ∧ 𝐸 < 1))
183	181, 182	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1))
184	183	simprd 500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 < 1)
185	170, 171, 113, 179, 184	lttrd 11359	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 · 𝐸) < 1)
186	170, 113, 113, 185	ltadd2dd 11357	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < (1 + 1))
187		df-2 12291	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 = (1 + 1)
188	186, 187	breqtrrdi 5146	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < 2)
189	42	rpregt0d 13054	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸))))
190	130	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 2 ∈ ℝ)
191		2pos 12333	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
192	191	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 2)
193	15	rpregt0d 13054	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸)))
194		ltdiv2 12089	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸))) ∧ (2 ∈ ℝ ∧ 0 < 2) ∧ ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸))) → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))))
195	189, 190, 192, 193, 194	syl121anc 1398	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))))
196	188, 195	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))
197	42	rpcnd 13050	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℂ)
198	42	rpcnne0d 13057	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0))
199		divsubdir 11896	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ 1 ∈ ℂ ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))))
200	197, 49, 198, 199	syl3anc 1394	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))))
201		ax-1cn 11146	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℂ
202		pncan2 11452	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ (𝐿 · 𝐸) ∈ ℂ) → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸))
203	201, 147, 202	sylancr 598	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸))
204	203	oveq1d 7415	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))
205		divid 11890	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0) → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1)
206	198, 205	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1)
207	206	oveq1d 7415	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))) = (1 − (1 / (1 + (𝐿 · 𝐸)))))
208	200, 204, 207	3eqtr3d 2808	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))) = (1 − (1 / (1 + (𝐿 · 𝐸)))))
209	196, 208	breqtrd 5130	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸)))))
210	167, 168, 113	ltaddsubd 11802	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1 ↔ ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸))))))
211	209, 210	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1)
212	169, 113, 30, 211	ltmul1dd 13103	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) < (1 · (𝑍 / 𝑉)))
213		reccl 11867	. . . . . . . . . . . . . . . . 17 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0) → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ)
214	198, 213	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ)
215	157, 214, 126	adddird 11222	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))))
216	197, 111	mulcomd 11218	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) = (𝑉 · (1 + (𝐿 · 𝐸))))
217	216	oveq2d 7416	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
218	28	rpcnd 13050	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑍 ∈ ℂ)
219	29	rpcnne0d 13057	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0))
220		divdiv1 11914	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑍 ∈ ℂ ∧ (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0) ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
221	218, 219, 198, 220	syl3anc 1394	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
222	42	rpne0d 13053	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ≠ 0)
223	126, 197, 222	divrec2d 11983	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))
224	217, 221, 223	3eqtr2d 2806	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))
225	224	oveq2d 7416	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))))
226	215, 225	eqtr4d 2803	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
227	126	mullidd 11215	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · (𝑍 / 𝑉)) = (𝑍 / 𝑉))
228	212, 226, 227	3brtr3d 5135	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) < (𝑍 / 𝑉))
229	53, 61, 31, 166, 228	lelttrd 11356	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (𝑍 / 𝑉))
230		fllep1 13822	. . . . . . . . . . . . 13 ⊢ ((𝑍 / 𝑉) ∈ ℝ → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1))
231	31, 230	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1))
232	53, 31, 57, 229, 231	ltletrd 11358	. . . . . . . . . . 11 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < ((⌊‘(𝑍 / 𝑉)) + 1))
233	50, 232	eqbrtrd 5126	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1))
234	32, 47	readdcld 11226	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ)
235	234, 55, 113	ltadd1d 11795	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1)))
236	233, 235	mpbird 260	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)))
237	32, 47, 55	ltaddsubd 11802	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))))
238	236, 237	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
239	31	flcld 13819	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℤ)
240		fzval3 13751	. . . . . . . . . . . 12 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ ℤ → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
241	239, 240	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
242	33, 241	eqtrid 2812	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
243	242	fveq2d 6875	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐼) = (♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))))
244		flword2 13834	. . . . . . . . . . . 12 ⊢ (((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ ∧ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉)) → (⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
245	45, 31, 122, 244	syl3anc 1394	. . . . . . . . . . 11 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
246		eluzp1p1 12878	. . . . . . . . . . 11 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ_≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
247	245, 246	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ_≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
248		hashfzo 14454	. . . . . . . . . 10 ⊢ (((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ_≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) → (♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) = (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
249	247, 248	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) = (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
250	55	recnd 11225	. . . . . . . . . 10 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℂ)
251	250, 48, 49	pnpcan2d 11595	. . . . . . . . 9 ⊢ (𝜑 → (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
252	243, 249, 251	3eqtrd 2804	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐼) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
253	238, 252	breqtrrd 5132	. . . . . . 7 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < (♯‘𝐼))
254	32, 38, 253	ltled 11346	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼))
255	21, 38, 30	lemuldivd 13097	. . . . . 6 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼) ↔ ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉))))
256	254, 255	mpbid 235	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)))
257	29	rpred 13048	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ ℝ)
258	69, 76, 66, 94, 100	ltletrd 11358	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (√‘𝑍))
259	257, 69, 66, 119, 258	lttrd 11359	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 < (√‘𝑍))
260	257, 66, 259	ltled 11346	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ≤ (√‘𝑍))
261	29	rprege0d 13055	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑉 ∈ ℝ ∧ 0 ≤ 𝑉))
262	65	rprege0d 13055	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((√‘𝑍) ∈ ℝ ∧ 0 ≤ (√‘𝑍)))
263		le2sq 14158	. . . . . . . . . . . . . . 15 ⊢ (((𝑉 ∈ ℝ ∧ 0 ≤ 𝑉) ∧ ((√‘𝑍) ∈ ℝ ∧ 0 ≤ (√‘𝑍))) → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2)))
264	261, 262, 263	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2)))
265	260, 264	mpbid 235	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉↑2) ≤ ((√‘𝑍)↑2))
266		resqrtth 15294	. . . . . . . . . . . . . 14 ⊢ ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍)↑2) = 𝑍)
267	104, 266	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘𝑍)↑2) = 𝑍)
268	265, 267	breqtrd 5130	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉↑2) ≤ 𝑍)
269		2z 12614	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
270		rpexpcl 14104	. . . . . . . . . . . . . . 15 ⊢ ((𝑉 ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (𝑉↑2) ∈ ℝ⁺)
271	29, 269, 270	sylancl 597	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉↑2) ∈ ℝ⁺)
272	271	rpred 13048	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉↑2) ∈ ℝ)
273	272, 108, 28	lemul2d 13092	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑉↑2) ≤ 𝑍 ↔ (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍)))
274	268, 273	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍))
275	218	sqvald 14167	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍↑2) = (𝑍 · 𝑍))
276	274, 275	breqtrrd 5132	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍↑2))
277	108	resqcld 14149	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍↑2) ∈ ℝ)
278	108, 277, 271	lemuldivd 13097	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑍 · (𝑉↑2)) ≤ (𝑍↑2) ↔ 𝑍 ≤ ((𝑍↑2) / (𝑉↑2))))
279	276, 278	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ≤ ((𝑍↑2) / (𝑉↑2)))
280	29	rpne0d 13053	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ≠ 0)
281	218, 111, 280	sqdivd 14183	. . . . . . . . 9 ⊢ (𝜑 → ((𝑍 / 𝑉)↑2) = ((𝑍↑2) / (𝑉↑2)))
282	279, 281	breqtrrd 5132	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ≤ ((𝑍 / 𝑉)↑2))
283		rpexpcl 14104	. . . . . . . . . 10 ⊢ (((𝑍 / 𝑉) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((𝑍 / 𝑉)↑2) ∈ ℝ⁺)
284	30, 269, 283	sylancl 597	. . . . . . . . 9 ⊢ (𝜑 → ((𝑍 / 𝑉)↑2) ∈ ℝ⁺)
285	28, 284	logled 26746	. . . . . . . 8 ⊢ (𝜑 → (𝑍 ≤ ((𝑍 / 𝑉)↑2) ↔ (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2))))
286	282, 285	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2)))
287		relogexp 26715	. . . . . . . 8 ⊢ (((𝑍 / 𝑉) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉))))
288	30, 269, 287	sylancl 597	. . . . . . 7 ⊢ (𝜑 → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉))))
289	286, 288	breqtrd 5130	. . . . . 6 ⊢ (𝜑 → (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉))))
290	28	relogcld 26742	. . . . . . 7 ⊢ (𝜑 → (log‘𝑍) ∈ ℝ)
291	30	relogcld 26742	. . . . . . 7 ⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℝ)
292		ledivmul 12079	. . . . . . 7 ⊢ (((log‘𝑍) ∈ ℝ ∧ (log‘(𝑍 / 𝑉)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉)))))
293	290, 291, 190, 192, 292	syl112anc 1397	. . . . . 6 ⊢ (𝜑 → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉)))))
294	289, 293	mpbird 260	. . . . 5 ⊢ (𝜑 → ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)))
295	20	rprege0d 13055	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) ∈ ℝ ∧ 0 ≤ ((𝐿 · 𝐸) / 4)))
296	38, 30	rerpdivcld 13079	. . . . . 6 ⊢ (𝜑 → ((♯‘𝐼) / (𝑍 / 𝑉)) ∈ ℝ)
297	27	simp2d 1159	. . . . . . . . . 10 ⊢ (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
298	297	simp1d 1158	. . . . . . . . 9 ⊢ (𝜑 → 1 < 𝑍)
299	108, 298	rplogcld 26748	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑍) ∈ ℝ⁺)
300	299	rphalfcld 13060	. . . . . . 7 ⊢ (𝜑 → ((log‘𝑍) / 2) ∈ ℝ⁺)
301	300	rprege0d 13055	. . . . . 6 ⊢ (𝜑 → (((log‘𝑍) / 2) ∈ ℝ ∧ 0 ≤ ((log‘𝑍) / 2)))
302		lemul12a 12061	. . . . . 6 ⊢ ((((((𝐿 · 𝐸) / 4) ∈ ℝ ∧ 0 ≤ ((𝐿 · 𝐸) / 4)) ∧ ((♯‘𝐼) / (𝑍 / 𝑉)) ∈ ℝ) ∧ ((((log‘𝑍) / 2) ∈ ℝ ∧ 0 ≤ ((log‘𝑍) / 2)) ∧ (log‘(𝑍 / 𝑉)) ∈ ℝ)) → ((((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)) ∧ ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))))
303	295, 296, 301, 291, 302	syl22anc 851	. . . . 5 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)) ∧ ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))))
304	256, 294, 303	mp2and 711	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
305	299	rpcnd 13050	. . . . . 6 ⊢ (𝜑 → (log‘𝑍) ∈ ℂ)
306		8nn 12324	. . . . . . . 8 ⊢ 8 ∈ ℕ
307		nnrp 13016	. . . . . . . 8 ⊢ (8 ∈ ℕ → 8 ∈ ℝ⁺)
308	306, 307	ax-mp 5	. . . . . . 7 ⊢ 8 ∈ ℝ⁺
309		rpcnne0 13023	. . . . . . 7 ⊢ (8 ∈ ℝ⁺ → (8 ∈ ℂ ∧ 8 ≠ 0))
310	308, 309	mp1i 14	. . . . . 6 ⊢ (𝜑 → (8 ∈ ℂ ∧ 8 ≠ 0))
311		div23 11879	. . . . . 6 ⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0)) → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍)))
312	147, 305, 310, 311	syl3anc 1394	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍)))
313		divmuldiv 11903	. . . . . . 7 ⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)))
314	147, 305, 140, 150, 313	syl22anc 851	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)))
315		4t2e8 12397	. . . . . . 7 ⊢ (4 · 2) = 8
316	315	oveq2i 7411	. . . . . 6 ⊢ (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / 8)
317	314, 316	eqtr2di 2817	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)))
318	312, 317	eqtr3d 2802	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)))
319	38	recnd 11225	. . . . 5 ⊢ (𝜑 → (♯‘𝐼) ∈ ℂ)
320	291	recnd 11225	. . . . 5 ⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℂ)
321	30	rpcnne0d 13057	. . . . 5 ⊢ (𝜑 → ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0))
322		divass 11878	. . . . . 6 ⊢ (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))
323		div23 11879	. . . . . 6 ⊢ (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
324	322, 323	eqtr3d 2802	. . . . 5 ⊢ (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
325	319, 320, 321, 324	syl3anc 1394	. . . 4 ⊢ (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
326	304, 318, 325	3brtr4d 5136	. . 3 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))
327		rpdivcl 13031	. . . . . . 7 ⊢ (((𝐿 · 𝐸) ∈ ℝ⁺ ∧ 8 ∈ ℝ⁺) → ((𝐿 · 𝐸) / 8) ∈ ℝ⁺)
328	15, 308, 327	sylancl 597	. . . . . 6 ⊢ (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℝ⁺)
329	328, 299	rpmulcld 13064	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ⁺)
330	329	rpred 13048	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ)
331	291, 30	rerpdivcld 13079	. . . . 5 ⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ)
332	38, 331	remulcld 11227	. . . 4 ⊢ (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
333	180	simp3d 1160	. . . 4 ⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℝ⁺)
334	330, 332, 333	lemul2d 13092	. . 3 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ↔ ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))))
335	326, 334	mpbid 235	. 2 ⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
336	333	rpcnd 13050	. . 3 ⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℂ)
337	331	recnd 11225	. . 3 ⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℂ)
338	336, 319, 337	mul12d 11407	. 2 ⊢ (𝜑 → ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) = ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
339	335, 338	breqtrd 5130	1 ⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 ∀wral 3079 ∃wrex 3089 class class class wbr 5104 ↦ cmpt 5185 ‘cfv 6525 (class class class)co 7400 Fincfn 8931 ℂcc 11086 ℝcr 11087 0cc0 11088 1c1 11089 + caddc 11091 · cmul 11093 +∞cpnf 11228 < clt 11231 ≤ cle 11232 − cmin 11429 / cdiv 11859 ℕcn 12221 2c2 12283 3c3 12284 4c4 12285 8c8 12289 ℕ₀cn0 12492 ℤcz 12579 cdc 12699 ℤ_≥cuz 12850 ℝ⁺crp 13004 (,)cioo 13360 [,)cico 13362 [,]cicc 13363 ...cfz 13523 ..^cfzo 13670 ⌊cfl 13811 ↑cexp 14085 ♯chash 14354 √csqrt 15272 abscabs 15273 expce 16103 eceu 16104 logclog 26673 ψcchp 27211

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5231 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 ax-inf2 9598 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166 ax-addf 11167

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5105 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6291 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-isom 6534 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-of 7664 df-om 7851 df-1st 7974 df-2nd 7975 df-supp 8145 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-2o 8442 df-er 8682 df-map 8814 df-pm 8815 df-ixp 8884 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-fsupp 9310 df-fi 9359 df-sup 9390 df-inf 9391 df-oi 9460 df-card 9913 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12222 df-2 12291 df-3 12292 df-4 12293 df-5 12294 df-6 12295 df-7 12296 df-8 12297 df-9 12298 df-n0 12493 df-z 12580 df-dec 12700 df-uz 12851 df-q 12961 df-rp 13005 df-xneg 13125 df-xadd 13126 df-xmul 13127 df-ioo 13364 df-ioc 13365 df-ico 13366 df-icc 13367 df-fz 13524 df-fzo 13671 df-fl 13813 df-mod 13891 df-seq 14026 df-exp 14086 df-fac 14298 df-bc 14327 df-hash 14355 df-shft 15092 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-limsup 15510 df-clim 15527 df-rlim 15528 df-sum 15726 df-ef 16109 df-e 16110 df-sin 16111 df-cos 16112 df-pi 16114 df-struct 17195 df-sets 17212 df-slot 17230 df-ndx 17242 df-base 17258 df-ress 17279 df-plusg 17311 df-mulr 17312 df-starv 17313 df-sca 17314 df-vsca 17315 df-ip 17316 df-tset 17317 df-ple 17318 df-ds 17320 df-unif 17321 df-hom 17322 df-cco 17323 df-rest 17463 df-topn 17464 df-0g 17482 df-gsum 17483 df-topgen 17484 df-pt 17485 df-prds 17488 df-xrs 17544 df-qtop 17549 df-imas 17550 df-xps 17552 df-mre 17626 df-mrc 17627 df-acs 17629 df-mgm 18686 df-sgrp 18765 df-mnd 18781 df-submnd 18830 df-mulg 19122 df-cntz 19375 df-cmn 19840 df-psmet 21471 df-xmet 21472 df-met 21473 df-bl 21474 df-mopn 21475 df-fbas 21476 df-fg 21477 df-cnfld 21480 df-top 23008 df-topon 23025 df-topsp 23047 df-bases 23060 df-cld 23133 df-ntr 23134 df-cls 23135 df-nei 23212 df-lp 23250 df-perf 23251 df-cn 23341 df-cnp 23342 df-haus 23429 df-tx 23676 df-hmeo 23869 df-fil 23960 df-fm 24052 df-flim 24053 df-flf 24054 df-xms 24434 df-ms 24435 df-tms 24436 df-cncf 24994 df-limc 25982 df-dv 25983 df-log 26675

This theorem is referenced by: pntlemj 27721

W3C validator