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 27795

Description: Lemma for pntlemj 27796. (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 27787	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 ∈ ℝ⁺ ∧ 𝐷 ∈ ℝ⁺ ∧ 𝐹 ∈ ℝ⁺))
8	7	simp1d 1160	. . . . . . . . . . 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 27788	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∈ ℝ⁺ ∧ 𝐾 ∈ ℝ⁺ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈ ℝ⁺)))
14	13	simp1d 1160	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
15	8, 14	rpmulcld 13087	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ⁺)
16		4re 12336	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
17		4pos 12362	. . . . . . . . . . 11 ⊢ 0 < 4
18	16, 17	elrpii 13030	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
19		rpdivcl 13054	. . . . . . . . . 10 ⊢ (((𝐿 · 𝐸) ∈ ℝ⁺ ∧ 4 ∈ ℝ⁺) → ((𝐿 · 𝐸) / 4) ∈ ℝ⁺)
20	15, 18, 19	sylancl 598	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℝ⁺)
21	20	rpred 13071	. . . . . . . 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 27790	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 ∈ ℝ⁺ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))))
28	27	simp1d 1160	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ ℝ⁺)
29		pntlem1.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ℝ⁺)
30	28, 29	rpdivcld 13088	. . . . . . . . 9 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ⁺)
31	30	rpred 13071	. . . . . . . 8 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ)
32	21, 31	remulcld 11250	. . . . . . 7 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ)
33		pntlem1.i	. . . . . . . . . 10 ⊢ 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))
34		fzfid 14022	. . . . . . . . . 10 ⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ∈ Fin)
35	33, 34	eqeltrid 2869	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ Fin)
36		hashcl 14405	. . . . . . . . 9 ⊢ (𝐼 ∈ Fin → (♯‘𝐼) ∈ ℕ₀)
37	35, 36	syl 18	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐼) ∈ ℕ₀)
38	37	nn0red 12577	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐼) ∈ ℝ)
39	32	recnd 11248	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℂ)
40		1rp 13031	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ⁺
41		rpaddcl 13051	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ⁺ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → (1 + (𝐿 · 𝐸)) ∈ ℝ⁺)
42	40, 15, 41	sylancr 599	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ⁺)
43	42, 29	rpmulcld 13087	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ⁺)
44	28, 43	rpdivcld 13088	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ⁺)
45	44	rpred 13071	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ)
46		reflcl 13842	. . . . . . . . . . . . . 14 ⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
47	45, 46	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
48	47	recnd 11248	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℂ)
49		1cnd 11213	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
50	39, 48, 49	add32d 11449	. . . . . . . . . . 11 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) = (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
51		peano2re 11394	. . . . . . . . . . . . . 14 ⊢ ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ)
52	32, 51	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ)
53	52, 47	readdcld 11249	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ)
54		reflcl 13842	. . . . . . . . . . . . . 14 ⊢ ((𝑍 / 𝑉) ∈ ℝ → (⌊‘(𝑍 / 𝑉)) ∈ ℝ)
55	31, 54	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℝ)
56		peano2re 11394	. . . . . . . . . . . . 13 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ ℝ → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ)
57	55, 56	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ)
58	15	rphalfcld 13083	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ⁺)
59	58, 30	rpmulcld 13087	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ⁺)
60	59	rpred 13071	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ)
61	60, 45	readdcld 11249	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
62		rpdivcl 13054	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((4 ∈ ℝ⁺ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → (4 / (𝐿 · 𝐸)) ∈ ℝ⁺)
63	18, 15, 62	sylancr 599	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ⁺)
64	63	rpred 13071	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ)
65	28	rpsqrtcld 15482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑍) ∈ ℝ⁺)
66	65	rpred 13071	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (√‘𝑍) ∈ ℝ)
67	27	simp3d 1162	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))
68	67	simp1d 1160	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (√‘𝑍))
69	43	rpred 13071	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ)
70	13	simp2d 1161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐾 ∈ ℝ⁺)
71		pntlem1.j	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 ∈ (𝑀..^𝑁))
72		elfzoelz 13699	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ)
73	71, 72	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐽 ∈ ℤ)
74	73	peano2zd 12714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐽 + 1) ∈ ℤ)
75	70, 74	rpexpcld 14296	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ⁺)
76	75	rpred 13071	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ)
77		pntlem1.V	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
78	77	simplrd 782	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽)))
79	70	rpcnd 13073	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐾 ∈ ℂ)
80	70, 73	rpexpcld 14296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝐾↑𝐽) ∈ ℝ⁺)
81	80	rpcnd 13073	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐾↑𝐽) ∈ ℂ)
82	79, 81	mulcomd 11241	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 27791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ_≥‘𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀)))
86	85	simp1d 1160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ ℕ)
87		elfzouz 13704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ_≥‘𝑀))
88	71, 87	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝐽 ∈ (ℤ_≥‘𝑀))
89		eluznn 12953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑀 ∈ ℕ ∧ 𝐽 ∈ (ℤ_≥‘𝑀)) → 𝐽 ∈ ℕ)
90	86, 88, 89	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐽 ∈ ℕ)
91	90	nnnn0d 12576	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
92	79, 91	expp1d 14196	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾↑𝐽) · 𝐾))
93	82, 92	eqtr4d 2803	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = (𝐾↑(𝐽 + 1)))
94	78, 93	breqtrd 5139	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1)))
95	69, 76, 94	ltled 11369	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1)))
96		fzofzp1 13805	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 27792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝐽 + 1) ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
99	97, 98	mpdan 700	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
100	99	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))
101	69, 76, 66, 95, 100	letrd 11378	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍))
102	69, 66, 65	lemul2d 13115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍) ↔ ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍))))
103	101, 102	mpbid 235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍)))
104	28	rprege0d 13078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍))
105		remsqsqrt 15326	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
106	104, 105	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
107	103, 106	breqtrd 5139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍)
108	28	rpred 13071	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑍 ∈ ℝ)
109	66, 108, 43	lemuldivd 13120	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍 ↔ (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
110	107, 109	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
111	29	rpcnd 13073	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑉 ∈ ℂ)
112	111	mullidd 11238	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑉) = 𝑉)
113		1red 11220	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℝ)
114	42	rpred 13071	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ)
115		1re 11219	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℝ
116		ltaddrp 13066	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1 ∈ ℝ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → 1 < (1 + (𝐿 · 𝐸)))
117	115, 15, 116	sylancr 599	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 < (1 + (𝐿 · 𝐸)))
118	113, 114, 29, 117	ltmul1dd 13126	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑉) < ((1 + (𝐿 · 𝐸)) · 𝑉))
119	112, 118	eqbrtrrd 5137	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉))
120	29, 43, 28	ltdiv2d 13094	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉) ↔ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉)))
121	119, 120	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉))
122	45, 31, 121	ltled 11369	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉))
123	66, 45, 31, 110, 122	letrd 11378	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / 𝑉))
124	64, 66, 31, 68, 123	letrd 11378	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (𝑍 / 𝑉))
125	64, 31, 31, 124	leadd2dd 11840	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ ((𝑍 / 𝑉) + (𝑍 / 𝑉)))
126	30	rpcnd 13073	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℂ)
127	126	2timesd 12498	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑍 / 𝑉)) = ((𝑍 / 𝑉) + (𝑍 / 𝑉)))
128	125, 127	breqtrrd 5141	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)))
129	31, 64	readdcld 11249	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ∈ ℝ)
130		2re 12326	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
131		remulcl 11196	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ) → (2 · (𝑍 / 𝑉)) ∈ ℝ)
132	130, 31, 131	sylancr 599	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑍 / 𝑉)) ∈ ℝ)
133	129, 132, 20	lemul2d 13115	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉)))))
134	128, 133	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))
135	20	rpcnd 13073	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℂ)
136	63	rpcnd 13073	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℂ)
137	135, 126, 136	adddid 11244	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))))
138	15	rpcnne0d 13080	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0))
139		rpcnne0 13046	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 ∈ ℝ⁺ → (4 ∈ ℂ ∧ 4 ≠ 0))
140	18, 139	mp1i 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 ∈ ℂ ∧ 4 ≠ 0))
141		divcan6 11933	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0) ∧ (4 ∈ ℂ ∧ 4 ≠ 0)) → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1)
142	138, 140, 141	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1)
143	142	oveq2d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1))
144	137, 143	eqtrd 2800	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1))
145		2cnd 12330	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℂ)
146	135, 145, 126	mulassd 11243	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))
147	15	rpcnd 13073	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℂ)
148		2rp 13032	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ⁺
149		rpcnne0 13046	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 ∈ ℝ⁺ → (2 ∈ ℂ ∧ 2 ≠ 0))
150	148, 149	mp1i 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2 ∈ ℂ ∧ 2 ≠ 0))
151		divdiv1 11937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2)))
152	147, 150, 150, 151	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2)))
153		2t2e4 12415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 · 2) = 4
154	153	oveq2i 7427	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐿 · 𝐸) / (2 · 2)) = ((𝐿 · 𝐸) / 4)
155	152, 154	eqtr2di 2817	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) = (((𝐿 · 𝐸) / 2) / 2))
156	155	oveq1d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((((𝐿 · 𝐸) / 2) / 2) · 2))
157	147	halfcld 12500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℂ)
158	150	simprd 501	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 2 ≠ 0)
159	157, 145, 158	divcan1d 12003	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) / 2) · 2) = ((𝐿 · 𝐸) / 2))
160	156, 159	eqtrd 2800	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((𝐿 · 𝐸) / 2))
161	160	oveq1d 7431	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
162	146, 161	eqtr3d 2802	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
163	134, 144, 162	3brtr3d 5144	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ≤ (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
164		flle 13845	. . . . . . . . . . . . . . 15 ⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
165	45, 164	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
166	52, 47, 60, 45, 163, 165	le2addd 11844	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ≤ ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
167	58	rpred 13071	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ)
168	42	rprecred 13082	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℝ)
169	167, 168	readdcld 11249	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) ∈ ℝ)
170	15	rpred 13071	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ)
171	14	rpred 13071	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 ∈ ℝ)
172	8	rpred 13071	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 ∈ ℝ)
173		eliooord 13443	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ (0(,)1) → (0 < 𝐿 ∧ 𝐿 < 1))
174	4, 173	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (0 < 𝐿 ∧ 𝐿 < 1))
175	174	simprd 501	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 < 1)
176	172, 113, 14, 175	ltmul1dd 13126	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐿 · 𝐸) < (1 · 𝐸))
177	14	rpcnd 13073	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 ∈ ℂ)
178	177	mullidd 11238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1 · 𝐸) = 𝐸)
179	176, 178	breqtrd 5139	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝐸) < 𝐸)
180	13	simp3d 1162	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈ ℝ⁺))
181	180	simp1d 1160	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 ∈ (0(,)1))
182		eliooord 13443	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐸 ∈ (0(,)1) → (0 < 𝐸 ∧ 𝐸 < 1))
183	181, 182	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1))
184	183	simprd 501	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 < 1)
185	170, 171, 113, 179, 184	lttrd 11382	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 · 𝐸) < 1)
186	170, 113, 113, 185	ltadd2dd 11380	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < (1 + 1))
187		df-2 12314	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 = (1 + 1)
188	186, 187	breqtrrdi 5155	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < 2)
189	42	rpregt0d 13077	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸))))
190	130	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 2 ∈ ℝ)
191		2pos 12356	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
192	191	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 2)
193	15	rpregt0d 13077	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸)))
194		ltdiv2 12112	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸))) ∧ (2 ∈ ℝ ∧ 0 < 2) ∧ ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸))) → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))))
195	189, 190, 192, 193, 194	syl121anc 1402	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))))
196	188, 195	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))
197	42	rpcnd 13073	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℂ)
198	42	rpcnne0d 13080	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0))
199		divsubdir 11919	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ 1 ∈ ℂ ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))))
200	197, 49, 198, 199	syl3anc 1398	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))))
201		ax-1cn 11169	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℂ
202		pncan2 11475	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ (𝐿 · 𝐸) ∈ ℂ) → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸))
203	201, 147, 202	sylancr 599	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸))
204	203	oveq1d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))
205		divid 11913	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0) → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1)
206	198, 205	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1)
207	206	oveq1d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))) = (1 − (1 / (1 + (𝐿 · 𝐸)))))
208	200, 204, 207	3eqtr3d 2808	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))) = (1 − (1 / (1 + (𝐿 · 𝐸)))))
209	196, 208	breqtrd 5139	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸)))))
210	167, 168, 113	ltaddsubd 11825	. . . . . . . . . . . . . . . 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 13126	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) < (1 · (𝑍 / 𝑉)))
213		reccl 11890	. . . . . . . . . . . . . . . . 17 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0) → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ)
214	198, 213	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ)
215	157, 214, 126	adddird 11245	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))))
216	197, 111	mulcomd 11241	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) = (𝑉 · (1 + (𝐿 · 𝐸))))
217	216	oveq2d 7432	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
218	28	rpcnd 13073	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑍 ∈ ℂ)
219	29	rpcnne0d 13080	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0))
220		divdiv1 11937	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑍 ∈ ℂ ∧ (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0) ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
221	218, 219, 198, 220	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
222	42	rpne0d 13076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ≠ 0)
223	126, 197, 222	divrec2d 12006	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))
224	217, 221, 223	3eqtr2d 2806	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))
225	224	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))))
226	215, 225	eqtr4d 2803	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
227	126	mullidd 11238	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · (𝑍 / 𝑉)) = (𝑍 / 𝑉))
228	212, 226, 227	3brtr3d 5144	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) < (𝑍 / 𝑉))
229	53, 61, 31, 166, 228	lelttrd 11379	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (𝑍 / 𝑉))
230		fllep1 13847	. . . . . . . . . . . . 13 ⊢ ((𝑍 / 𝑉) ∈ ℝ → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1))
231	31, 230	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1))
232	53, 31, 57, 229, 231	ltletrd 11381	. . . . . . . . . . 11 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < ((⌊‘(𝑍 / 𝑉)) + 1))
233	50, 232	eqbrtrd 5135	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1))
234	32, 47	readdcld 11249	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ)
235	234, 55, 113	ltadd1d 11818	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1)))
236	233, 235	mpbird 260	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)))
237	32, 47, 55	ltaddsubd 11825	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))))
238	236, 237	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
239	31	flcld 13844	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℤ)
240		fzval3 13775	. . . . . . . . . . . 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 6889	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐼) = (♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))))
244		flword2 13859	. . . . . . . . . . . 12 ⊢ (((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ ∧ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉)) → (⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
245	45, 31, 122, 244	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
246		eluzp1p1 12901	. . . . . . . . . . 11 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ_≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
247	245, 246	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ_≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
248		hashfzo 14479	. . . . . . . . . 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 11248	. . . . . . . . . 10 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℂ)
251	250, 48, 49	pnpcan2d 11618	. . . . . . . . 9 ⊢ (𝜑 → (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
252	243, 249, 251	3eqtrd 2804	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐼) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
253	238, 252	breqtrrd 5141	. . . . . . 7 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < (♯‘𝐼))
254	32, 38, 253	ltled 11369	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼))
255	21, 38, 30	lemuldivd 13120	. . . . . 6 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼) ↔ ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉))))
256	254, 255	mpbid 235	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)))
257	29	rpred 13071	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ ℝ)
258	69, 76, 66, 94, 100	ltletrd 11381	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (√‘𝑍))
259	257, 69, 66, 119, 258	lttrd 11382	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 < (√‘𝑍))
260	257, 66, 259	ltled 11369	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ≤ (√‘𝑍))
261	29	rprege0d 13078	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑉 ∈ ℝ ∧ 0 ≤ 𝑉))
262	65	rprege0d 13078	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((√‘𝑍) ∈ ℝ ∧ 0 ≤ (√‘𝑍)))
263		le2sq 14183	. . . . . . . . . . . . . . 15 ⊢ (((𝑉 ∈ ℝ ∧ 0 ≤ 𝑉) ∧ ((√‘𝑍) ∈ ℝ ∧ 0 ≤ (√‘𝑍))) → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2)))
264	261, 262, 263	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2)))
265	260, 264	mpbid 235	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉↑2) ≤ ((√‘𝑍)↑2))
266		resqrtth 15325	. . . . . . . . . . . . . 14 ⊢ ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍)↑2) = 𝑍)
267	104, 266	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘𝑍)↑2) = 𝑍)
268	265, 267	breqtrd 5139	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉↑2) ≤ 𝑍)
269		2z 12637	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
270		rpexpcl 14129	. . . . . . . . . . . . . . 15 ⊢ ((𝑉 ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (𝑉↑2) ∈ ℝ⁺)
271	29, 269, 270	sylancl 598	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉↑2) ∈ ℝ⁺)
272	271	rpred 13071	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉↑2) ∈ ℝ)
273	272, 108, 28	lemul2d 13115	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑉↑2) ≤ 𝑍 ↔ (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍)))
274	268, 273	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍))
275	218	sqvald 14192	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍↑2) = (𝑍 · 𝑍))
276	274, 275	breqtrrd 5141	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍↑2))
277	108	resqcld 14174	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍↑2) ∈ ℝ)
278	108, 277, 271	lemuldivd 13120	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑍 · (𝑉↑2)) ≤ (𝑍↑2) ↔ 𝑍 ≤ ((𝑍↑2) / (𝑉↑2))))
279	276, 278	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ≤ ((𝑍↑2) / (𝑉↑2)))
280	29	rpne0d 13076	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ≠ 0)
281	218, 111, 280	sqdivd 14208	. . . . . . . . 9 ⊢ (𝜑 → ((𝑍 / 𝑉)↑2) = ((𝑍↑2) / (𝑉↑2)))
282	279, 281	breqtrrd 5141	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ≤ ((𝑍 / 𝑉)↑2))
283		rpexpcl 14129	. . . . . . . . . 10 ⊢ (((𝑍 / 𝑉) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((𝑍 / 𝑉)↑2) ∈ ℝ⁺)
284	30, 269, 283	sylancl 598	. . . . . . . . 9 ⊢ (𝜑 → ((𝑍 / 𝑉)↑2) ∈ ℝ⁺)
285	28, 284	logled 26821	. . . . . . . 8 ⊢ (𝜑 → (𝑍 ≤ ((𝑍 / 𝑉)↑2) ↔ (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2))))
286	282, 285	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2)))
287		relogexp 26790	. . . . . . . 8 ⊢ (((𝑍 / 𝑉) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉))))
288	30, 269, 287	sylancl 598	. . . . . . 7 ⊢ (𝜑 → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉))))
289	286, 288	breqtrd 5139	. . . . . 6 ⊢ (𝜑 → (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉))))
290	28	relogcld 26817	. . . . . . 7 ⊢ (𝜑 → (log‘𝑍) ∈ ℝ)
291	30	relogcld 26817	. . . . . . 7 ⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℝ)
292		ledivmul 12102	. . . . . . 7 ⊢ (((log‘𝑍) ∈ ℝ ∧ (log‘(𝑍 / 𝑉)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉)))))
293	290, 291, 190, 192, 292	syl112anc 1401	. . . . . 6 ⊢ (𝜑 → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉)))))
294	289, 293	mpbird 260	. . . . 5 ⊢ (𝜑 → ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)))
295	20	rprege0d 13078	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) ∈ ℝ ∧ 0 ≤ ((𝐿 · 𝐸) / 4)))
296	38, 30	rerpdivcld 13102	. . . . . 6 ⊢ (𝜑 → ((♯‘𝐼) / (𝑍 / 𝑉)) ∈ ℝ)
297	27	simp2d 1161	. . . . . . . . . 10 ⊢ (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
298	297	simp1d 1160	. . . . . . . . 9 ⊢ (𝜑 → 1 < 𝑍)
299	108, 298	rplogcld 26823	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑍) ∈ ℝ⁺)
300	299	rphalfcld 13083	. . . . . . 7 ⊢ (𝜑 → ((log‘𝑍) / 2) ∈ ℝ⁺)
301	300	rprege0d 13078	. . . . . 6 ⊢ (𝜑 → (((log‘𝑍) / 2) ∈ ℝ ∧ 0 ≤ ((log‘𝑍) / 2)))
302		lemul12a 12084	. . . . . 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 852	. . . . 5 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)) ∧ ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))))
304	256, 294, 303	mp2and 712	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
305	299	rpcnd 13073	. . . . . 6 ⊢ (𝜑 → (log‘𝑍) ∈ ℂ)
306		8nn 12347	. . . . . . . 8 ⊢ 8 ∈ ℕ
307		nnrp 13039	. . . . . . . 8 ⊢ (8 ∈ ℕ → 8 ∈ ℝ⁺)
308	306, 307	ax-mp 5	. . . . . . 7 ⊢ 8 ∈ ℝ⁺
309		rpcnne0 13046	. . . . . . 7 ⊢ (8 ∈ ℝ⁺ → (8 ∈ ℂ ∧ 8 ≠ 0))
310	308, 309	mp1i 14	. . . . . 6 ⊢ (𝜑 → (8 ∈ ℂ ∧ 8 ≠ 0))
311		div23 11902	. . . . . 6 ⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0)) → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍)))
312	147, 305, 310, 311	syl3anc 1398	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍)))
313		divmuldiv 11926	. . . . . . 7 ⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)))
314	147, 305, 140, 150, 313	syl22anc 852	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)))
315		4t2e8 12420	. . . . . . 7 ⊢ (4 · 2) = 8
316	315	oveq2i 7427	. . . . . 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 11248	. . . . 5 ⊢ (𝜑 → (♯‘𝐼) ∈ ℂ)
320	291	recnd 11248	. . . . 5 ⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℂ)
321	30	rpcnne0d 13080	. . . . 5 ⊢ (𝜑 → ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0))
322		divass 11901	. . . . . 6 ⊢ (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))
323		div23 11902	. . . . . 6 ⊢ (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
324	322, 323	eqtr3d 2802	. . . . 5 ⊢ (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
325	319, 320, 321, 324	syl3anc 1398	. . . 4 ⊢ (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
326	304, 318, 325	3brtr4d 5145	. . 3 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))
327		rpdivcl 13054	. . . . . . 7 ⊢ (((𝐿 · 𝐸) ∈ ℝ⁺ ∧ 8 ∈ ℝ⁺) → ((𝐿 · 𝐸) / 8) ∈ ℝ⁺)
328	15, 308, 327	sylancl 598	. . . . . 6 ⊢ (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℝ⁺)
329	328, 299	rpmulcld 13087	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ⁺)
330	329	rpred 13071	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ)
331	291, 30	rerpdivcld 13102	. . . . 5 ⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ)
332	38, 331	remulcld 11250	. . . 4 ⊢ (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
333	180	simp3d 1162	. . . 4 ⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℝ⁺)
334	330, 332, 333	lemul2d 13115	. . 3 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ↔ ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))))
335	326, 334	mpbid 235	. 2 ⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
336	333	rpcnd 13073	. . 3 ⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℂ)
337	331	recnd 11248	. . 3 ⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℂ)
338	336, 319, 337	mul12d 11430	. 2 ⊢ (𝜑 → ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) = ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
339	335, 338	breqtrd 5139	1 ⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 class class class wbr 5111 ↦ cmpt 5194 ‘cfv 6540 (class class class)co 7416 Fincfn 8945 ℂcc 11109 ℝcr 11110 0cc0 11111 1c1 11112 + caddc 11114 · cmul 11116 +∞cpnf 11251 < clt 11254 ≤ cle 11255 − cmin 11452 / cdiv 11882 ℕcn 12244 2c2 12306 3c3 12307 4c4 12308 8c8 12312 ℕ₀cn0 12515 ℤcz 12602 cdc 12722 ℤ_≥cuz 12873 ℝ⁺crp 13027 (,)cioo 13383 [,)cico 13385 [,]cicc 13386 ...cfz 13546 ..^cfzo 13694 ⌊cfl 13836 ↑cexp 14110 ♯chash 14379 √csqrt 15303 abscabs 15304 expce 16132 eceu 16133 logclog 26748 ψcchp 27286

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7738 ax-inf2 9613 ax-cnex 11167 ax-resscn 11168 ax-1cn 11169 ax-icn 11170 ax-addcl 11171 ax-addrcl 11172 ax-mulcl 11173 ax-mulrcl 11174 ax-mulcom 11175 ax-addass 11176 ax-mulass 11177 ax-distr 11178 ax-i2m1 11179 ax-1ne0 11180 ax-1rid 11181 ax-rnegex 11182 ax-rrecex 11183 ax-cnre 11184 ax-pre-lttri 11185 ax-pre-lttrn 11186 ax-pre-ltadd 11187 ax-pre-mulgt0 11188 ax-pre-sup 11189 ax-addf 11190

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7680 df-om 7865 df-1st 7988 df-2nd 7989 df-supp 8159 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-er 8696 df-map 8828 df-pm 8829 df-ixp 8898 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fsupp 9325 df-fi 9374 df-sup 9405 df-inf 9406 df-oi 9475 df-card 9937 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11454 df-neg 11455 df-div 11883 df-nn 12245 df-2 12314 df-3 12315 df-4 12316 df-5 12317 df-6 12318 df-7 12319 df-8 12320 df-9 12321 df-n0 12516 df-z 12603 df-dec 12723 df-uz 12874 df-q 12984 df-rp 13028 df-xneg 13148 df-xadd 13149 df-xmul 13150 df-ioo 13387 df-ioc 13388 df-ico 13389 df-icc 13390 df-fz 13547 df-fzo 13695 df-fl 13838 df-mod 13916 df-seq 14051 df-exp 14111 df-fac 14323 df-bc 14352 df-hash 14380 df-shft 15123 df-cj 15169 df-re 15170 df-im 15171 df-sqrt 15305 df-abs 15306 df-limsup 15541 df-clim 15558 df-rlim 15559 df-sum 15757 df-ef 16138 df-e 16139 df-sin 16140 df-cos 16141 df-pi 16143 df-struct 17224 df-sets 17241 df-slot 17259 df-ndx 17271 df-base 17287 df-ress 17308 df-plusg 17340 df-mulr 17341 df-starv 17342 df-sca 17343 df-vsca 17344 df-ip 17345 df-tset 17346 df-ple 17347 df-ds 17349 df-unif 17350 df-hom 17351 df-cco 17352 df-rest 17492 df-topn 17493 df-0g 17511 df-gsum 17512 df-topgen 17513 df-pt 17514 df-prds 17517 df-xrs 17573 df-qtop 17578 df-imas 17579 df-xps 17581 df-mre 17655 df-mrc 17656 df-acs 17658 df-mgm 18715 df-sgrp 18798 df-mnd 18814 df-submnd 18865 df-mulg 19157 df-cntz 19410 df-cmn 19875 df-psmet 21543 df-xmet 21544 df-met 21545 df-bl 21546 df-mopn 21547 df-fbas 21548 df-fg 21549 df-cnfld 21552 df-top 23080 df-topon 23097 df-topsp 23119 df-bases 23132 df-cld 23205 df-ntr 23206 df-cls 23207 df-nei 23284 df-lp 23322 df-perf 23323 df-cn 23413 df-cnp 23414 df-haus 23501 df-tx 23748 df-hmeo 23941 df-fil 24032 df-fm 24124 df-flim 24125 df-flf 24126 df-xms 24506 df-ms 24507 df-tms 24508 df-cncf 25066 df-limc 26054 df-dv 26055 df-log 26750

This theorem is used by: pntlemj 27796

W3C validator