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 25291

Description: Lemma for pntlemj 25292. (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 25283	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 ∈ ℝ⁺ ∧ 𝐷 ∈ ℝ⁺ ∧ 𝐹 ∈ ℝ⁺))
8	7	simp1d 1073	. . . . . . . . . . 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 25284	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∈ ℝ⁺ ∧ 𝐾 ∈ ℝ⁺ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈ ℝ⁺)))
14	13	simp1d 1073	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
15	8, 14	rpmulcld 11888	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ⁺)
16		4re 11097	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
17		4pos 11116	. . . . . . . . . . 11 ⊢ 0 < 4
18	16, 17	elrpii 11835	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
19		rpdivcl 11856	. . . . . . . . . 10 ⊢ (((𝐿 · 𝐸) ∈ ℝ⁺ ∧ 4 ∈ ℝ⁺) → ((𝐿 · 𝐸) / 4) ∈ ℝ⁺)
20	15, 18, 19	sylancl 694	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℝ⁺)
21	20	rpred 11872	. . . . . . . 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 25286	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 ∈ ℝ⁺ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))))
28	27	simp1d 1073	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ ℝ⁺)
29		pntlem1.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ℝ⁺)
30	28, 29	rpdivcld 11889	. . . . . . . . 9 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ⁺)
31	30	rpred 11872	. . . . . . . 8 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ)
32	21, 31	remulcld 10070	. . . . . . 7 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ)
33		pntlem1.i	. . . . . . . . . 10 ⊢ 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))
34		fzfid 12772	. . . . . . . . . 10 ⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ∈ Fin)
35	33, 34	syl5eqel 2705	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ Fin)
36		hashcl 13147	. . . . . . . . 9 ⊢ (𝐼 ∈ Fin → (#‘𝐼) ∈ ℕ₀)
37	35, 36	syl 17	. . . . . . . 8 ⊢ (𝜑 → (#‘𝐼) ∈ ℕ₀)
38	37	nn0red 11352	. . . . . . 7 ⊢ (𝜑 → (#‘𝐼) ∈ ℝ)
39	32	recnd 10068	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℂ)
40		1rp 11836	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ⁺
41		rpaddcl 11854	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ⁺ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → (1 + (𝐿 · 𝐸)) ∈ ℝ⁺)
42	40, 15, 41	sylancr 695	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ⁺)
43	42, 29	rpmulcld 11888	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ⁺)
44	28, 43	rpdivcld 11889	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ⁺)
45	44	rpred 11872	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ)
46		reflcl 12597	. . . . . . . . . . . . . 14 ⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
47	45, 46	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
48	47	recnd 10068	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℂ)
49		1cnd 10056	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
50	39, 48, 49	add32d 10263	. . . . . . . . . . 11 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) = (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
51		peano2re 10209	. . . . . . . . . . . . . 14 ⊢ ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ)
52	32, 51	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ)
53	52, 47	readdcld 10069	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ)
54		reflcl 12597	. . . . . . . . . . . . . 14 ⊢ ((𝑍 / 𝑉) ∈ ℝ → (⌊‘(𝑍 / 𝑉)) ∈ ℝ)
55	31, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℝ)
56		peano2re 10209	. . . . . . . . . . . . 13 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ ℝ → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ)
57	55, 56	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ)
58	15	rphalfcld 11884	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ⁺)
59	58, 30	rpmulcld 11888	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ⁺)
60	59	rpred 11872	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ)
61	60, 45	readdcld 10069	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
62		rpdivcl 11856	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((4 ∈ ℝ⁺ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → (4 / (𝐿 · 𝐸)) ∈ ℝ⁺)
63	18, 15, 62	sylancr 695	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ⁺)
64	63	rpred 11872	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ)
65	28	rpsqrtcld 14150	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑍) ∈ ℝ⁺)
66	65	rpred 11872	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (√‘𝑍) ∈ ℝ)
67	27	simp3d 1075	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))
68	67	simp1d 1073	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (√‘𝑍))
69	43	rpred 11872	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ)
70	13	simp2d 1074	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐾 ∈ ℝ⁺)
71		pntlem1.j	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 ∈ (𝑀..^𝑁))
72		elfzoelz 12470	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ)
73	71, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐽 ∈ ℤ)
74	73	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐽 + 1) ∈ ℤ)
75	70, 74	rpexpcld 13032	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ⁺)
76	75	rpred 11872	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ)
77		pntlem1.V	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
78	77	simpld 475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))))
79	78	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽)))
80	70	rpcnd 11874	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐾 ∈ ℂ)
81	70, 73	rpexpcld 13032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝐾↑𝐽) ∈ ℝ⁺)
82	81	rpcnd 11874	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐾↑𝐽) ∈ ℂ)
83	80, 82	mulcomd 10061	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = ((𝐾↑𝐽) · 𝐾))
84		pntlem1.m	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)
85		pntlem1.n	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))
86	1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 84, 85	pntlemg 25287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ_≥‘𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀)))
87	86	simp1d 1073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ ℕ)
88		elfzouz 12474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ_≥‘𝑀))
89	71, 88	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝐽 ∈ (ℤ_≥‘𝑀))
90		eluznn 11758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑀 ∈ ℕ ∧ 𝐽 ∈ (ℤ_≥‘𝑀)) → 𝐽 ∈ ℕ)
91	87, 89, 90	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐽 ∈ ℕ)
92	91	nnnn0d 11351	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
93	80, 92	expp1d 13009	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾↑𝐽) · 𝐾))
94	83, 93	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = (𝐾↑(𝐽 + 1)))
95	79, 94	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1)))
96	69, 76, 95	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1)))
97		fzofzp1 12565	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐽 ∈ (𝑀..^𝑁) → (𝐽 + 1) ∈ (𝑀...𝑁))
98	71, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐽 + 1) ∈ (𝑀...𝑁))
99	1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 84, 85	pntlemh 25288	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝐽 + 1) ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
100	98, 99	mpdan 702	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
101	100	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))
102	69, 76, 66, 96, 101	letrd 10194	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍))
103	69, 66, 65	lemul2d 11916	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍) ↔ ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍))))
104	102, 103	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍)))
105	28	rprege0d 11879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍))
106		remsqsqrt 13997	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
107	105, 106	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
108	104, 107	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍)
109	28	rpred 11872	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑍 ∈ ℝ)
110	66, 109, 43	lemuldivd 11921	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍 ↔ (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
111	108, 110	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
112	29	rpcnd 11874	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑉 ∈ ℂ)
113	112	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑉) = 𝑉)
114		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℝ)
115	42	rpred 11872	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ)
116		1re 10039	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℝ
117		ltaddrp 11867	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1 ∈ ℝ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → 1 < (1 + (𝐿 · 𝐸)))
118	116, 15, 117	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 < (1 + (𝐿 · 𝐸)))
119	114, 115, 29, 118	ltmul1dd 11927	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑉) < ((1 + (𝐿 · 𝐸)) · 𝑉))
120	113, 119	eqbrtrrd 4677	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉))
121	29, 43, 28	ltdiv2d 11895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉) ↔ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉)))
122	120, 121	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉))
123	45, 31, 122	ltled 10185	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉))
124	66, 45, 31, 111, 123	letrd 10194	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / 𝑉))
125	64, 66, 31, 68, 124	letrd 10194	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (𝑍 / 𝑉))
126	64, 31, 31, 125	leadd2dd 10642	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ ((𝑍 / 𝑉) + (𝑍 / 𝑉)))
127	30	rpcnd 11874	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℂ)
128	127	2timesd 11275	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑍 / 𝑉)) = ((𝑍 / 𝑉) + (𝑍 / 𝑉)))
129	126, 128	breqtrrd 4681	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)))
130	31, 64	readdcld 10069	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ∈ ℝ)
131		2re 11090	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
132		remulcl 10021	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ) → (2 · (𝑍 / 𝑉)) ∈ ℝ)
133	131, 31, 132	sylancr 695	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑍 / 𝑉)) ∈ ℝ)
134	130, 133, 20	lemul2d 11916	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉)))))
135	129, 134	mpbid 222	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))
136	20	rpcnd 11874	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℂ)
137	63	rpcnd 11874	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℂ)
138	136, 127, 137	adddid 10064	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))))
139	15	rpcnne0d 11881	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0))
140		rpcnne0 11850	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 ∈ ℝ⁺ → (4 ∈ ℂ ∧ 4 ≠ 0))
141	18, 140	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 ∈ ℂ ∧ 4 ≠ 0))
142		divcan6 10732	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0) ∧ (4 ∈ ℂ ∧ 4 ≠ 0)) → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1)
143	139, 141, 142	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1)
144	143	oveq2d 6666	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1))
145	138, 144	eqtrd 2656	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1))
146		2cnd 11093	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℂ)
147	136, 146, 127	mulassd 10063	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))
148	15	rpcnd 11874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℂ)
149		2rp 11837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ⁺
150		rpcnne0 11850	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 ∈ ℝ⁺ → (2 ∈ ℂ ∧ 2 ≠ 0))
151	149, 150	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2 ∈ ℂ ∧ 2 ≠ 0))
152		divdiv1 10736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2)))
153	148, 151, 151, 152	syl3anc 1326	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2)))
154		2t2e4 11177	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 · 2) = 4
155	154	oveq2i 6661	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐿 · 𝐸) / (2 · 2)) = ((𝐿 · 𝐸) / 4)
156	153, 155	syl6req 2673	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) = (((𝐿 · 𝐸) / 2) / 2))
157	156	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((((𝐿 · 𝐸) / 2) / 2) · 2))
158	148	halfcld 11277	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℂ)
159	151	simprd 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 2 ≠ 0)
160	158, 146, 159	divcan1d 10802	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) / 2) · 2) = ((𝐿 · 𝐸) / 2))
161	157, 160	eqtrd 2656	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((𝐿 · 𝐸) / 2))
162	161	oveq1d 6665	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
163	147, 162	eqtr3d 2658	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
164	135, 145, 163	3brtr3d 4684	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ≤ (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
165		flle 12600	. . . . . . . . . . . . . . 15 ⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
166	45, 165	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
167	52, 47, 60, 45, 164, 166	le2addd 10646	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ≤ ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
168	58	rpred 11872	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ)
169	42	rprecred 11883	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℝ)
170	168, 169	readdcld 10069	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) ∈ ℝ)
171	15	rpred 11872	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ)
172	14	rpred 11872	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 ∈ ℝ)
173	8	rpred 11872	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 ∈ ℝ)
174		eliooord 12233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ (0(,)1) → (0 < 𝐿 ∧ 𝐿 < 1))
175	4, 174	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (0 < 𝐿 ∧ 𝐿 < 1))
176	175	simprd 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 < 1)
177	173, 114, 14, 176	ltmul1dd 11927	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐿 · 𝐸) < (1 · 𝐸))
178	14	rpcnd 11874	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 ∈ ℂ)
179	178	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1 · 𝐸) = 𝐸)
180	177, 179	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝐸) < 𝐸)
181	13	simp3d 1075	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈ ℝ⁺))
182	181	simp1d 1073	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 ∈ (0(,)1))
183		eliooord 12233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐸 ∈ (0(,)1) → (0 < 𝐸 ∧ 𝐸 < 1))
184	182, 183	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1))
185	184	simprd 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 < 1)
186	171, 172, 114, 180, 185	lttrd 10198	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 · 𝐸) < 1)
187	171, 114, 114, 186	ltadd2dd 10196	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < (1 + 1))
188		df-2 11079	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 = (1 + 1)
189	187, 188	syl6breqr 4695	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < 2)
190	42	rpregt0d 11878	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸))))
191	131	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 2 ∈ ℝ)
192		2pos 11112	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
193	192	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 2)
194	15	rpregt0d 11878	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸)))
195		ltdiv2 10909	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸))) ∧ (2 ∈ ℝ ∧ 0 < 2) ∧ ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸))) → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))))
196	190, 191, 193, 194, 195	syl121anc 1331	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))))
197	189, 196	mpbid 222	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))
198	42	rpcnd 11874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℂ)
199	42	rpcnne0d 11881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0))
200		divsubdir 10721	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ 1 ∈ ℂ ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))))
201	198, 49, 199, 200	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))))
202		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℂ
203		pncan2 10288	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ (𝐿 · 𝐸) ∈ ℂ) → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸))
204	202, 148, 203	sylancr 695	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸))
205	204	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))
206		divid 10714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0) → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1)
207	199, 206	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1)
208	207	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))) = (1 − (1 / (1 + (𝐿 · 𝐸)))))
209	201, 205, 208	3eqtr3d 2664	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))) = (1 − (1 / (1 + (𝐿 · 𝐸)))))
210	197, 209	breqtrd 4679	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸)))))
211	168, 169, 114	ltaddsubd 10627	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1 ↔ ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸))))))
212	210, 211	mpbird 247	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1)
213	170, 114, 30, 212	ltmul1dd 11927	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) < (1 · (𝑍 / 𝑉)))
214		reccl 10692	. . . . . . . . . . . . . . . . 17 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0) → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ)
215	199, 214	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ)
216	158, 215, 127	adddird 10065	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))))
217	198, 112	mulcomd 10061	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) = (𝑉 · (1 + (𝐿 · 𝐸))))
218	217	oveq2d 6666	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
219	28	rpcnd 11874	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑍 ∈ ℂ)
220	29	rpcnne0d 11881	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0))
221		divdiv1 10736	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑍 ∈ ℂ ∧ (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0) ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
222	219, 220, 199, 221	syl3anc 1326	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
223	42	rpne0d 11877	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ≠ 0)
224	127, 198, 223	divrec2d 10805	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))
225	218, 222, 224	3eqtr2d 2662	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))
226	225	oveq2d 6666	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))))
227	216, 226	eqtr4d 2659	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
228	127	mulid2d 10058	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · (𝑍 / 𝑉)) = (𝑍 / 𝑉))
229	213, 227, 228	3brtr3d 4684	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) < (𝑍 / 𝑉))
230	53, 61, 31, 167, 229	lelttrd 10195	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (𝑍 / 𝑉))
231		fllep1 12602	. . . . . . . . . . . . 13 ⊢ ((𝑍 / 𝑉) ∈ ℝ → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1))
232	31, 231	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1))
233	53, 31, 57, 230, 232	ltletrd 10197	. . . . . . . . . . 11 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < ((⌊‘(𝑍 / 𝑉)) + 1))
234	50, 233	eqbrtrd 4675	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1))
235	32, 47	readdcld 10069	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ)
236	235, 55, 114	ltadd1d 10620	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1)))
237	234, 236	mpbird 247	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)))
238	32, 47, 55	ltaddsubd 10627	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))))
239	237, 238	mpbid 222	. . . . . . . 8 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
240	31	flcld 12599	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℤ)
241		fzval3 12536	. . . . . . . . . . . 12 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ ℤ → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
242	240, 241	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
243	33, 242	syl5eq 2668	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
244	243	fveq2d 6195	. . . . . . . . 9 ⊢ (𝜑 → (#‘𝐼) = (#‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))))
245		flword2 12614	. . . . . . . . . . . 12 ⊢ (((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ ∧ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉)) → (⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
246	45, 31, 123, 245	syl3anc 1326	. . . . . . . . . . 11 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
247		eluzp1p1 11713	. . . . . . . . . . 11 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ_≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
248	246, 247	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ_≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
249		hashfzo 13216	. . . . . . . . . 10 ⊢ (((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ_≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) → (#‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) = (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
250	248, 249	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (#‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) = (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
251	55	recnd 10068	. . . . . . . . . 10 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℂ)
252	251, 48, 49	pnpcan2d 10430	. . . . . . . . 9 ⊢ (𝜑 → (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
253	244, 250, 252	3eqtrd 2660	. . . . . . . 8 ⊢ (𝜑 → (#‘𝐼) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
254	239, 253	breqtrrd 4681	. . . . . . 7 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < (#‘𝐼))
255	32, 38, 254	ltled 10185	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (#‘𝐼))
256	21, 38, 30	lemuldivd 11921	. . . . . 6 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (#‘𝐼) ↔ ((𝐿 · 𝐸) / 4) ≤ ((#‘𝐼) / (𝑍 / 𝑉))))
257	255, 256	mpbid 222	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ≤ ((#‘𝐼) / (𝑍 / 𝑉)))
258	29	rpred 11872	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ ℝ)
259	69, 76, 66, 95, 101	ltletrd 10197	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (√‘𝑍))
260	258, 69, 66, 120, 259	lttrd 10198	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 < (√‘𝑍))
261	258, 66, 260	ltled 10185	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ≤ (√‘𝑍))
262	29	rprege0d 11879	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑉 ∈ ℝ ∧ 0 ≤ 𝑉))
263	65	rprege0d 11879	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((√‘𝑍) ∈ ℝ ∧ 0 ≤ (√‘𝑍)))
264		le2sq 12938	. . . . . . . . . . . . . . 15 ⊢ (((𝑉 ∈ ℝ ∧ 0 ≤ 𝑉) ∧ ((√‘𝑍) ∈ ℝ ∧ 0 ≤ (√‘𝑍))) → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2)))
265	262, 263, 264	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2)))
266	261, 265	mpbid 222	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉↑2) ≤ ((√‘𝑍)↑2))
267		resqrtth 13996	. . . . . . . . . . . . . 14 ⊢ ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍)↑2) = 𝑍)
268	105, 267	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘𝑍)↑2) = 𝑍)
269	266, 268	breqtrd 4679	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉↑2) ≤ 𝑍)
270		2z 11409	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
271		rpexpcl 12879	. . . . . . . . . . . . . . 15 ⊢ ((𝑉 ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (𝑉↑2) ∈ ℝ⁺)
272	29, 270, 271	sylancl 694	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉↑2) ∈ ℝ⁺)
273	272	rpred 11872	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉↑2) ∈ ℝ)
274	273, 109, 28	lemul2d 11916	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑉↑2) ≤ 𝑍 ↔ (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍)))
275	269, 274	mpbid 222	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍))
276	219	sqvald 13005	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍↑2) = (𝑍 · 𝑍))
277	275, 276	breqtrrd 4681	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍↑2))
278	109	resqcld 13035	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍↑2) ∈ ℝ)
279	109, 278, 272	lemuldivd 11921	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑍 · (𝑉↑2)) ≤ (𝑍↑2) ↔ 𝑍 ≤ ((𝑍↑2) / (𝑉↑2))))
280	277, 279	mpbid 222	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ≤ ((𝑍↑2) / (𝑉↑2)))
281	29	rpne0d 11877	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ≠ 0)
282	219, 112, 281	sqdivd 13021	. . . . . . . . 9 ⊢ (𝜑 → ((𝑍 / 𝑉)↑2) = ((𝑍↑2) / (𝑉↑2)))
283	280, 282	breqtrrd 4681	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ≤ ((𝑍 / 𝑉)↑2))
284		rpexpcl 12879	. . . . . . . . . 10 ⊢ (((𝑍 / 𝑉) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((𝑍 / 𝑉)↑2) ∈ ℝ⁺)
285	30, 270, 284	sylancl 694	. . . . . . . . 9 ⊢ (𝜑 → ((𝑍 / 𝑉)↑2) ∈ ℝ⁺)
286	28, 285	logled 24373	. . . . . . . 8 ⊢ (𝜑 → (𝑍 ≤ ((𝑍 / 𝑉)↑2) ↔ (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2))))
287	283, 286	mpbid 222	. . . . . . 7 ⊢ (𝜑 → (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2)))
288		relogexp 24342	. . . . . . . 8 ⊢ (((𝑍 / 𝑉) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉))))
289	30, 270, 288	sylancl 694	. . . . . . 7 ⊢ (𝜑 → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉))))
290	287, 289	breqtrd 4679	. . . . . 6 ⊢ (𝜑 → (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉))))
291	28	relogcld 24369	. . . . . . 7 ⊢ (𝜑 → (log‘𝑍) ∈ ℝ)
292	30	relogcld 24369	. . . . . . 7 ⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℝ)
293		ledivmul 10899	. . . . . . 7 ⊢ (((log‘𝑍) ∈ ℝ ∧ (log‘(𝑍 / 𝑉)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉)))))
294	291, 292, 191, 193, 293	syl112anc 1330	. . . . . 6 ⊢ (𝜑 → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉)))))
295	290, 294	mpbird 247	. . . . 5 ⊢ (𝜑 → ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)))
296	20	rprege0d 11879	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) ∈ ℝ ∧ 0 ≤ ((𝐿 · 𝐸) / 4)))
297	38, 30	rerpdivcld 11903	. . . . . 6 ⊢ (𝜑 → ((#‘𝐼) / (𝑍 / 𝑉)) ∈ ℝ)
298	27	simp2d 1074	. . . . . . . . . 10 ⊢ (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
299	298	simp1d 1073	. . . . . . . . 9 ⊢ (𝜑 → 1 < 𝑍)
300	109, 299	rplogcld 24375	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑍) ∈ ℝ⁺)
301	300	rphalfcld 11884	. . . . . . 7 ⊢ (𝜑 → ((log‘𝑍) / 2) ∈ ℝ⁺)
302	301	rprege0d 11879	. . . . . 6 ⊢ (𝜑 → (((log‘𝑍) / 2) ∈ ℝ ∧ 0 ≤ ((log‘𝑍) / 2)))
303		lemul12a 10881	. . . . . 6 ⊢ ((((((𝐿 · 𝐸) / 4) ∈ ℝ ∧ 0 ≤ ((𝐿 · 𝐸) / 4)) ∧ ((#‘𝐼) / (𝑍 / 𝑉)) ∈ ℝ) ∧ ((((log‘𝑍) / 2) ∈ ℝ ∧ 0 ≤ ((log‘𝑍) / 2)) ∧ (log‘(𝑍 / 𝑉)) ∈ ℝ)) → ((((𝐿 · 𝐸) / 4) ≤ ((#‘𝐼) / (𝑍 / 𝑉)) ∧ ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((#‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))))
304	296, 297, 302, 292, 303	syl22anc 1327	. . . . 5 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) ≤ ((#‘𝐼) / (𝑍 / 𝑉)) ∧ ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((#‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))))
305	257, 295, 304	mp2and 715	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((#‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
306	300	rpcnd 11874	. . . . . 6 ⊢ (𝜑 → (log‘𝑍) ∈ ℂ)
307		8nn 11191	. . . . . . . 8 ⊢ 8 ∈ ℕ
308		nnrp 11842	. . . . . . . 8 ⊢ (8 ∈ ℕ → 8 ∈ ℝ⁺)
309	307, 308	ax-mp 5	. . . . . . 7 ⊢ 8 ∈ ℝ⁺
310		rpcnne0 11850	. . . . . . 7 ⊢ (8 ∈ ℝ⁺ → (8 ∈ ℂ ∧ 8 ≠ 0))
311	309, 310	mp1i 13	. . . . . 6 ⊢ (𝜑 → (8 ∈ ℂ ∧ 8 ≠ 0))
312		div23 10704	. . . . . 6 ⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0)) → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍)))
313	148, 306, 311, 312	syl3anc 1326	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍)))
314		divmuldiv 10725	. . . . . . 7 ⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)))
315	148, 306, 141, 151, 314	syl22anc 1327	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)))
316		4t2e8 11181	. . . . . . 7 ⊢ (4 · 2) = 8
317	316	oveq2i 6661	. . . . . 6 ⊢ (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / 8)
318	315, 317	syl6req 2673	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)))
319	313, 318	eqtr3d 2658	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)))
320	38	recnd 10068	. . . . 5 ⊢ (𝜑 → (#‘𝐼) ∈ ℂ)
321	292	recnd 10068	. . . . 5 ⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℂ)
322	30	rpcnne0d 11881	. . . . 5 ⊢ (𝜑 → ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0))
323		divass 10703	. . . . . 6 ⊢ (((#‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((#‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = ((#‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))
324		div23 10704	. . . . . 6 ⊢ (((#‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((#‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = (((#‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
325	323, 324	eqtr3d 2658	. . . . 5 ⊢ (((#‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → ((#‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((#‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
326	320, 321, 322, 325	syl3anc 1326	. . . 4 ⊢ (𝜑 → ((#‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((#‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
327	305, 319, 326	3brtr4d 4685	. . 3 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((#‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))
328		rpdivcl 11856	. . . . . . 7 ⊢ (((𝐿 · 𝐸) ∈ ℝ⁺ ∧ 8 ∈ ℝ⁺) → ((𝐿 · 𝐸) / 8) ∈ ℝ⁺)
329	15, 309, 328	sylancl 694	. . . . . 6 ⊢ (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℝ⁺)
330	329, 300	rpmulcld 11888	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ⁺)
331	330	rpred 11872	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ)
332	292, 30	rerpdivcld 11903	. . . . 5 ⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ)
333	38, 332	remulcld 10070	. . . 4 ⊢ (𝜑 → ((#‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
334	181	simp3d 1075	. . . 4 ⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℝ⁺)
335	331, 333, 334	lemul2d 11916	. . 3 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((#‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ↔ ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((#‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))))
336	327, 335	mpbid 222	. 2 ⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((#‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
337	334	rpcnd 11874	. . 3 ⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℂ)
338	332	recnd 10068	. . 3 ⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℂ)
339	337, 320, 338	mul12d 10245	. 2 ⊢ (𝜑 → ((𝑈 − 𝐸) · ((#‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) = ((#‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
340	336, 339	breqtrd 4679	1 ⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((#‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 class class class wbr 4653 ↦ cmpt 4729 ‘cfv 5888 (class class class)co 6650 Fincfn 7955 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 +∞cpnf 10071 < clt 10074 ≤ cle 10075 − cmin 10266 / cdiv 10684 ℕcn 11020 2c2 11070 3c3 11071 4c4 11072 8c8 11076 ℕ₀cn0 11292 ℤcz 11377 cdc 11493 ℤ_≥cuz 11687 ℝ⁺crp 11832 (,)cioo 12175 [,)cico 12177 [,]cicc 12178 ...cfz 12326 ..^cfzo 12465 ⌊cfl 12591 ↑cexp 12860 #chash 13117 √csqrt 13973 abscabs 13974 expce 14792 eceu 14793 logclog 24301 ψcchp 24819

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-sum 14417 df-ef 14798 df-e 14799 df-sin 14800 df-cos 14801 df-pi 14803 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631 df-log 24303

This theorem is referenced by: pntlemj 25292

W3C validator