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 27664

Description: Lemma for pntlemj 27665. (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 27656	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 ∈ ℝ⁺ ∧ 𝐷 ∈ ℝ⁺ ∧ 𝐹 ∈ ℝ⁺))
8	7	simp1d 1142	. . . . . . . . . . 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 27657	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∈ ℝ⁺ ∧ 𝐾 ∈ ℝ⁺ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈ ℝ⁺)))
14	13	simp1d 1142	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
15	8, 14	rpmulcld 13115	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ⁺)
16		4re 12377	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
17		4pos 12400	. . . . . . . . . . 11 ⊢ 0 < 4
18	16, 17	elrpii 13060	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
19		rpdivcl 13082	. . . . . . . . . 10 ⊢ (((𝐿 · 𝐸) ∈ ℝ⁺ ∧ 4 ∈ ℝ⁺) → ((𝐿 · 𝐸) / 4) ∈ ℝ⁺)
20	15, 18, 19	sylancl 585	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℝ⁺)
21	20	rpred 13099	. . . . . . . 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 27659	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 ∈ ℝ⁺ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))))
28	27	simp1d 1142	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ ℝ⁺)
29		pntlem1.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ℝ⁺)
30	28, 29	rpdivcld 13116	. . . . . . . . 9 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ⁺)
31	30	rpred 13099	. . . . . . . 8 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ)
32	21, 31	remulcld 11320	. . . . . . 7 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ)
33		pntlem1.i	. . . . . . . . . 10 ⊢ 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))
34		fzfid 14024	. . . . . . . . . 10 ⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ∈ Fin)
35	33, 34	eqeltrid 2848	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ Fin)
36		hashcl 14405	. . . . . . . . 9 ⊢ (𝐼 ∈ Fin → (♯‘𝐼) ∈ ℕ₀)
37	35, 36	syl 17	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐼) ∈ ℕ₀)
38	37	nn0red 12614	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐼) ∈ ℝ)
39	32	recnd 11318	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℂ)
40		1rp 13061	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ⁺
41		rpaddcl 13079	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ⁺ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → (1 + (𝐿 · 𝐸)) ∈ ℝ⁺)
42	40, 15, 41	sylancr 586	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ⁺)
43	42, 29	rpmulcld 13115	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ⁺)
44	28, 43	rpdivcld 13116	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ⁺)
45	44	rpred 13099	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ)
46		reflcl 13847	. . . . . . . . . . . . . 14 ⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
47	45, 46	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
48	47	recnd 11318	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℂ)
49		1cnd 11285	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
50	39, 48, 49	add32d 11517	. . . . . . . . . . 11 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) = (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
51		peano2re 11463	. . . . . . . . . . . . . 14 ⊢ ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ)
52	32, 51	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ)
53	52, 47	readdcld 11319	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ)
54		reflcl 13847	. . . . . . . . . . . . . 14 ⊢ ((𝑍 / 𝑉) ∈ ℝ → (⌊‘(𝑍 / 𝑉)) ∈ ℝ)
55	31, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℝ)
56		peano2re 11463	. . . . . . . . . . . . 13 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ ℝ → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ)
57	55, 56	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ)
58	15	rphalfcld 13111	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ⁺)
59	58, 30	rpmulcld 13115	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ⁺)
60	59	rpred 13099	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ)
61	60, 45	readdcld 11319	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
62		rpdivcl 13082	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((4 ∈ ℝ⁺ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → (4 / (𝐿 · 𝐸)) ∈ ℝ⁺)
63	18, 15, 62	sylancr 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ⁺)
64	63	rpred 13099	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ)
65	28	rpsqrtcld 15460	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑍) ∈ ℝ⁺)
66	65	rpred 13099	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (√‘𝑍) ∈ ℝ)
67	27	simp3d 1144	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))
68	67	simp1d 1142	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (√‘𝑍))
69	43	rpred 13099	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ)
70	13	simp2d 1143	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐾 ∈ ℝ⁺)
71		pntlem1.j	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 ∈ (𝑀..^𝑁))
72		elfzoelz 13716	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ)
73	71, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐽 ∈ ℤ)
74	73	peano2zd 12750	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐽 + 1) ∈ ℤ)
75	70, 74	rpexpcld 14296	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ⁺)
76	75	rpred 13099	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ)
77		pntlem1.V	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
78	77	simplrd 769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽)))
79	70	rpcnd 13101	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐾 ∈ ℂ)
80	70, 73	rpexpcld 14296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝐾↑𝐽) ∈ ℝ⁺)
81	80	rpcnd 13101	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐾↑𝐽) ∈ ℂ)
82	79, 81	mulcomd 11311	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 27660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ_≥‘𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀)))
86	85	simp1d 1142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ ℕ)
87		elfzouz 13720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ_≥‘𝑀))
88	71, 87	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝐽 ∈ (ℤ_≥‘𝑀))
89		eluznn 12983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑀 ∈ ℕ ∧ 𝐽 ∈ (ℤ_≥‘𝑀)) → 𝐽 ∈ ℕ)
90	86, 88, 89	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐽 ∈ ℕ)
91	90	nnnn0d 12613	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
92	79, 91	expp1d 14197	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾↑𝐽) · 𝐾))
93	82, 92	eqtr4d 2783	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = (𝐾↑(𝐽 + 1)))
94	78, 93	breqtrd 5192	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1)))
95	69, 76, 94	ltled 11438	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1)))
96		fzofzp1 13814	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐽 ∈ (𝑀..^𝑁) → (𝐽 + 1) ∈ (𝑀...𝑁))
97	71, 96	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐽 + 1) ∈ (𝑀...𝑁))
98	1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 22, 23, 24, 25, 26, 83, 84	pntlemh 27661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝐽 + 1) ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
99	97, 98	mpdan 686	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
100	99	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))
101	69, 76, 66, 95, 100	letrd 11447	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍))
102	69, 66, 65	lemul2d 13143	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍) ↔ ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍))))
103	101, 102	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍)))
104	28	rprege0d 13106	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍))
105		remsqsqrt 15305	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
107	103, 106	breqtrd 5192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍)
108	28	rpred 13099	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑍 ∈ ℝ)
109	66, 108, 43	lemuldivd 13148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍 ↔ (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
110	107, 109	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
111	29	rpcnd 13101	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑉 ∈ ℂ)
112	111	mullidd 11308	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑉) = 𝑉)
113		1red 11291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℝ)
114	42	rpred 13099	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ)
115		1re 11290	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℝ
116		ltaddrp 13094	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1 ∈ ℝ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → 1 < (1 + (𝐿 · 𝐸)))
117	115, 15, 116	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 < (1 + (𝐿 · 𝐸)))
118	113, 114, 29, 117	ltmul1dd 13154	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑉) < ((1 + (𝐿 · 𝐸)) · 𝑉))
119	112, 118	eqbrtrrd 5190	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉))
120	29, 43, 28	ltdiv2d 13122	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉) ↔ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉)))
121	119, 120	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉))
122	45, 31, 121	ltled 11438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉))
123	66, 45, 31, 110, 122	letrd 11447	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / 𝑉))
124	64, 66, 31, 68, 123	letrd 11447	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (𝑍 / 𝑉))
125	64, 31, 31, 124	leadd2dd 11905	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ ((𝑍 / 𝑉) + (𝑍 / 𝑉)))
126	30	rpcnd 13101	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℂ)
127	126	2timesd 12536	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑍 / 𝑉)) = ((𝑍 / 𝑉) + (𝑍 / 𝑉)))
128	125, 127	breqtrrd 5194	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)))
129	31, 64	readdcld 11319	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ∈ ℝ)
130		2re 12367	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
131		remulcl 11269	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ) → (2 · (𝑍 / 𝑉)) ∈ ℝ)
132	130, 31, 131	sylancr 586	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑍 / 𝑉)) ∈ ℝ)
133	129, 132, 20	lemul2d 13143	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉)))))
134	128, 133	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))
135	20	rpcnd 13101	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℂ)
136	63	rpcnd 13101	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℂ)
137	135, 126, 136	adddid 11314	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))))
138	15	rpcnne0d 13108	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0))
139		rpcnne0 13075	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 ∈ ℝ⁺ → (4 ∈ ℂ ∧ 4 ≠ 0))
140	18, 139	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 ∈ ℂ ∧ 4 ≠ 0))
141		divcan6 12001	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0) ∧ (4 ∈ ℂ ∧ 4 ≠ 0)) → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1)
142	138, 140, 141	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1)
143	142	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1))
144	137, 143	eqtrd 2780	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1))
145		2cnd 12371	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℂ)
146	135, 145, 126	mulassd 11313	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))
147	15	rpcnd 13101	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℂ)
148		2rp 13062	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ⁺
149		rpcnne0 13075	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 ∈ ℝ⁺ → (2 ∈ ℂ ∧ 2 ≠ 0))
150	148, 149	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2 ∈ ℂ ∧ 2 ≠ 0))
151		divdiv1 12005	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2)))
152	147, 150, 150, 151	syl3anc 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2)))
153		2t2e4 12457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 · 2) = 4
154	153	oveq2i 7459	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐿 · 𝐸) / (2 · 2)) = ((𝐿 · 𝐸) / 4)
155	152, 154	eqtr2di 2797	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) = (((𝐿 · 𝐸) / 2) / 2))
156	155	oveq1d 7463	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((((𝐿 · 𝐸) / 2) / 2) · 2))
157	147	halfcld 12538	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℂ)
158	150	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 2 ≠ 0)
159	157, 145, 158	divcan1d 12071	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) / 2) · 2) = ((𝐿 · 𝐸) / 2))
160	156, 159	eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((𝐿 · 𝐸) / 2))
161	160	oveq1d 7463	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
162	146, 161	eqtr3d 2782	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
163	134, 144, 162	3brtr3d 5197	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ≤ (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
164		flle 13850	. . . . . . . . . . . . . . 15 ⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
165	45, 164	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
166	52, 47, 60, 45, 163, 165	le2addd 11909	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ≤ ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
167	58	rpred 13099	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ)
168	42	rprecred 13110	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℝ)
169	167, 168	readdcld 11319	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) ∈ ℝ)
170	15	rpred 13099	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ)
171	14	rpred 13099	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 ∈ ℝ)
172	8	rpred 13099	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 ∈ ℝ)
173		eliooord 13466	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ (0(,)1) → (0 < 𝐿 ∧ 𝐿 < 1))
174	4, 173	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (0 < 𝐿 ∧ 𝐿 < 1))
175	174	simprd 495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 < 1)
176	172, 113, 14, 175	ltmul1dd 13154	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐿 · 𝐸) < (1 · 𝐸))
177	14	rpcnd 13101	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 ∈ ℂ)
178	177	mullidd 11308	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1 · 𝐸) = 𝐸)
179	176, 178	breqtrd 5192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝐸) < 𝐸)
180	13	simp3d 1144	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈ ℝ⁺))
181	180	simp1d 1142	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 ∈ (0(,)1))
182		eliooord 13466	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐸 ∈ (0(,)1) → (0 < 𝐸 ∧ 𝐸 < 1))
183	181, 182	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1))
184	183	simprd 495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 < 1)
185	170, 171, 113, 179, 184	lttrd 11451	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 · 𝐸) < 1)
186	170, 113, 113, 185	ltadd2dd 11449	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < (1 + 1))
187		df-2 12356	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 = (1 + 1)
188	186, 187	breqtrrdi 5208	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < 2)
189	42	rpregt0d 13105	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸))))
190	130	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 2 ∈ ℝ)
191		2pos 12396	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
192	191	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 2)
193	15	rpregt0d 13105	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸)))
194		ltdiv2 12181	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸))) ∧ (2 ∈ ℝ ∧ 0 < 2) ∧ ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸))) → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))))
195	189, 190, 192, 193, 194	syl121anc 1375	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))))
196	188, 195	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))
197	42	rpcnd 13101	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℂ)
198	42	rpcnne0d 13108	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0))
199		divsubdir 11988	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ 1 ∈ ℂ ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))))
200	197, 49, 198, 199	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))))
201		ax-1cn 11242	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℂ
202		pncan2 11543	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ (𝐿 · 𝐸) ∈ ℂ) → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸))
203	201, 147, 202	sylancr 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸))
204	203	oveq1d 7463	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))
205		divid 11980	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0) → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1)
206	198, 205	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1)
207	206	oveq1d 7463	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))) = (1 − (1 / (1 + (𝐿 · 𝐸)))))
208	200, 204, 207	3eqtr3d 2788	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))) = (1 − (1 / (1 + (𝐿 · 𝐸)))))
209	196, 208	breqtrd 5192	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸)))))
210	167, 168, 113	ltaddsubd 11890	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1 ↔ ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸))))))
211	209, 210	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1)
212	169, 113, 30, 211	ltmul1dd 13154	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) < (1 · (𝑍 / 𝑉)))
213		reccl 11956	. . . . . . . . . . . . . . . . 17 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0) → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ)
214	198, 213	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ)
215	157, 214, 126	adddird 11315	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))))
216	197, 111	mulcomd 11311	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) = (𝑉 · (1 + (𝐿 · 𝐸))))
217	216	oveq2d 7464	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
218	28	rpcnd 13101	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑍 ∈ ℂ)
219	29	rpcnne0d 13108	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0))
220		divdiv1 12005	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑍 ∈ ℂ ∧ (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0) ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
221	218, 219, 198, 220	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
222	42	rpne0d 13104	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ≠ 0)
223	126, 197, 222	divrec2d 12074	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))
224	217, 221, 223	3eqtr2d 2786	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))
225	224	oveq2d 7464	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))))
226	215, 225	eqtr4d 2783	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
227	126	mullidd 11308	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · (𝑍 / 𝑉)) = (𝑍 / 𝑉))
228	212, 226, 227	3brtr3d 5197	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) < (𝑍 / 𝑉))
229	53, 61, 31, 166, 228	lelttrd 11448	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (𝑍 / 𝑉))
230		fllep1 13852	. . . . . . . . . . . . 13 ⊢ ((𝑍 / 𝑉) ∈ ℝ → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1))
231	31, 230	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1))
232	53, 31, 57, 229, 231	ltletrd 11450	. . . . . . . . . . 11 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < ((⌊‘(𝑍 / 𝑉)) + 1))
233	50, 232	eqbrtrd 5188	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1))
234	32, 47	readdcld 11319	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ)
235	234, 55, 113	ltadd1d 11883	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1)))
236	233, 235	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)))
237	32, 47, 55	ltaddsubd 11890	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))))
238	236, 237	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
239	31	flcld 13849	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℤ)
240		fzval3 13785	. . . . . . . . . . . 12 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ ℤ → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
241	239, 240	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
242	33, 241	eqtrid 2792	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
243	242	fveq2d 6924	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐼) = (♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))))
244		flword2 13864	. . . . . . . . . . . 12 ⊢ (((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ ∧ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉)) → (⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
245	45, 31, 122, 244	syl3anc 1371	. . . . . . . . . . 11 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
246		eluzp1p1 12931	. . . . . . . . . . 11 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ_≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
247	245, 246	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ_≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
248		hashfzo 14478	. . . . . . . . . 10 ⊢ (((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ_≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) → (♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) = (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
249	247, 248	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))) = (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
250	55	recnd 11318	. . . . . . . . . 10 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℂ)
251	250, 48, 49	pnpcan2d 11685	. . . . . . . . 9 ⊢ (𝜑 → (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
252	243, 249, 251	3eqtrd 2784	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐼) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
253	238, 252	breqtrrd 5194	. . . . . . 7 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < (♯‘𝐼))
254	32, 38, 253	ltled 11438	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼))
255	21, 38, 30	lemuldivd 13148	. . . . . 6 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼) ↔ ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉))))
256	254, 255	mpbid 232	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)))
257	29	rpred 13099	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ ℝ)
258	69, 76, 66, 94, 100	ltletrd 11450	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (√‘𝑍))
259	257, 69, 66, 119, 258	lttrd 11451	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 < (√‘𝑍))
260	257, 66, 259	ltled 11438	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ≤ (√‘𝑍))
261	29	rprege0d 13106	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑉 ∈ ℝ ∧ 0 ≤ 𝑉))
262	65	rprege0d 13106	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((√‘𝑍) ∈ ℝ ∧ 0 ≤ (√‘𝑍)))
263		le2sq 14184	. . . . . . . . . . . . . . 15 ⊢ (((𝑉 ∈ ℝ ∧ 0 ≤ 𝑉) ∧ ((√‘𝑍) ∈ ℝ ∧ 0 ≤ (√‘𝑍))) → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2)))
264	261, 262, 263	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2)))
265	260, 264	mpbid 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉↑2) ≤ ((√‘𝑍)↑2))
266		resqrtth 15304	. . . . . . . . . . . . . 14 ⊢ ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍)↑2) = 𝑍)
267	104, 266	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘𝑍)↑2) = 𝑍)
268	265, 267	breqtrd 5192	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉↑2) ≤ 𝑍)
269		2z 12675	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
270		rpexpcl 14131	. . . . . . . . . . . . . . 15 ⊢ ((𝑉 ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (𝑉↑2) ∈ ℝ⁺)
271	29, 269, 270	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉↑2) ∈ ℝ⁺)
272	271	rpred 13099	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉↑2) ∈ ℝ)
273	272, 108, 28	lemul2d 13143	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑉↑2) ≤ 𝑍 ↔ (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍)))
274	268, 273	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍))
275	218	sqvald 14193	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍↑2) = (𝑍 · 𝑍))
276	274, 275	breqtrrd 5194	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍↑2))
277	108	resqcld 14175	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍↑2) ∈ ℝ)
278	108, 277, 271	lemuldivd 13148	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑍 · (𝑉↑2)) ≤ (𝑍↑2) ↔ 𝑍 ≤ ((𝑍↑2) / (𝑉↑2))))
279	276, 278	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ≤ ((𝑍↑2) / (𝑉↑2)))
280	29	rpne0d 13104	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ≠ 0)
281	218, 111, 280	sqdivd 14209	. . . . . . . . 9 ⊢ (𝜑 → ((𝑍 / 𝑉)↑2) = ((𝑍↑2) / (𝑉↑2)))
282	279, 281	breqtrrd 5194	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ≤ ((𝑍 / 𝑉)↑2))
283		rpexpcl 14131	. . . . . . . . . 10 ⊢ (((𝑍 / 𝑉) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((𝑍 / 𝑉)↑2) ∈ ℝ⁺)
284	30, 269, 283	sylancl 585	. . . . . . . . 9 ⊢ (𝜑 → ((𝑍 / 𝑉)↑2) ∈ ℝ⁺)
285	28, 284	logled 26687	. . . . . . . 8 ⊢ (𝜑 → (𝑍 ≤ ((𝑍 / 𝑉)↑2) ↔ (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2))))
286	282, 285	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2)))
287		relogexp 26656	. . . . . . . 8 ⊢ (((𝑍 / 𝑉) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉))))
288	30, 269, 287	sylancl 585	. . . . . . 7 ⊢ (𝜑 → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉))))
289	286, 288	breqtrd 5192	. . . . . 6 ⊢ (𝜑 → (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉))))
290	28	relogcld 26683	. . . . . . 7 ⊢ (𝜑 → (log‘𝑍) ∈ ℝ)
291	30	relogcld 26683	. . . . . . 7 ⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℝ)
292		ledivmul 12171	. . . . . . 7 ⊢ (((log‘𝑍) ∈ ℝ ∧ (log‘(𝑍 / 𝑉)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉)))))
293	290, 291, 190, 192, 292	syl112anc 1374	. . . . . 6 ⊢ (𝜑 → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉)))))
294	289, 293	mpbird 257	. . . . 5 ⊢ (𝜑 → ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)))
295	20	rprege0d 13106	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) ∈ ℝ ∧ 0 ≤ ((𝐿 · 𝐸) / 4)))
296	38, 30	rerpdivcld 13130	. . . . . 6 ⊢ (𝜑 → ((♯‘𝐼) / (𝑍 / 𝑉)) ∈ ℝ)
297	27	simp2d 1143	. . . . . . . . . 10 ⊢ (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
298	297	simp1d 1142	. . . . . . . . 9 ⊢ (𝜑 → 1 < 𝑍)
299	108, 298	rplogcld 26689	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑍) ∈ ℝ⁺)
300	299	rphalfcld 13111	. . . . . . 7 ⊢ (𝜑 → ((log‘𝑍) / 2) ∈ ℝ⁺)
301	300	rprege0d 13106	. . . . . 6 ⊢ (𝜑 → (((log‘𝑍) / 2) ∈ ℝ ∧ 0 ≤ ((log‘𝑍) / 2)))
302		lemul12a 12152	. . . . . 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 838	. . . . 5 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)) ∧ ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))))
304	256, 294, 303	mp2and 698	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
305	299	rpcnd 13101	. . . . . 6 ⊢ (𝜑 → (log‘𝑍) ∈ ℂ)
306		8nn 12388	. . . . . . . 8 ⊢ 8 ∈ ℕ
307		nnrp 13068	. . . . . . . 8 ⊢ (8 ∈ ℕ → 8 ∈ ℝ⁺)
308	306, 307	ax-mp 5	. . . . . . 7 ⊢ 8 ∈ ℝ⁺
309		rpcnne0 13075	. . . . . . 7 ⊢ (8 ∈ ℝ⁺ → (8 ∈ ℂ ∧ 8 ≠ 0))
310	308, 309	mp1i 13	. . . . . 6 ⊢ (𝜑 → (8 ∈ ℂ ∧ 8 ≠ 0))
311		div23 11968	. . . . . 6 ⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0)) → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍)))
312	147, 305, 310, 311	syl3anc 1371	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍)))
313		divmuldiv 11994	. . . . . . 7 ⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)))
314	147, 305, 140, 150, 313	syl22anc 838	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)))
315		4t2e8 12461	. . . . . . 7 ⊢ (4 · 2) = 8
316	315	oveq2i 7459	. . . . . 6 ⊢ (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / 8)
317	314, 316	eqtr2di 2797	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)))
318	312, 317	eqtr3d 2782	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)))
319	38	recnd 11318	. . . . 5 ⊢ (𝜑 → (♯‘𝐼) ∈ ℂ)
320	291	recnd 11318	. . . . 5 ⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℂ)
321	30	rpcnne0d 13108	. . . . 5 ⊢ (𝜑 → ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0))
322		divass 11967	. . . . . 6 ⊢ (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))
323		div23 11968	. . . . . 6 ⊢ (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
324	322, 323	eqtr3d 2782	. . . . 5 ⊢ (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
325	319, 320, 321, 324	syl3anc 1371	. . . 4 ⊢ (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
326	304, 318, 325	3brtr4d 5198	. . 3 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))
327		rpdivcl 13082	. . . . . . 7 ⊢ (((𝐿 · 𝐸) ∈ ℝ⁺ ∧ 8 ∈ ℝ⁺) → ((𝐿 · 𝐸) / 8) ∈ ℝ⁺)
328	15, 308, 327	sylancl 585	. . . . . 6 ⊢ (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℝ⁺)
329	328, 299	rpmulcld 13115	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ⁺)
330	329	rpred 13099	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ)
331	291, 30	rerpdivcld 13130	. . . . 5 ⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ)
332	38, 331	remulcld 11320	. . . 4 ⊢ (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
333	180	simp3d 1144	. . . 4 ⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℝ⁺)
334	330, 332, 333	lemul2d 13143	. . 3 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ↔ ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))))
335	326, 334	mpbid 232	. 2 ⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
336	333	rpcnd 13101	. . 3 ⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℂ)
337	331	recnd 11318	. . 3 ⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℂ)
338	336, 319, 337	mul12d 11499	. 2 ⊢ (𝜑 → ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) = ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
339	335, 338	breqtrd 5192	1 ⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∀wral 3067 ∃wrex 3076 class class class wbr 5166 ↦ cmpt 5249 ‘cfv 6573 (class class class)co 7448 Fincfn 9003 ℂcc 11182 ℝcr 11183 0cc0 11184 1c1 11185 + caddc 11187 · cmul 11189 +∞cpnf 11321 < clt 11324 ≤ cle 11325 − cmin 11520 / cdiv 11947 ℕcn 12293 2c2 12348 3c3 12349 4c4 12350 8c8 12354 ℕ₀cn0 12553 ℤcz 12639 cdc 12758 ℤ_≥cuz 12903 ℝ⁺crp 13057 (,)cioo 13407 [,)cico 13409 [,]cicc 13410 ...cfz 13567 ..^cfzo 13711 ⌊cfl 13841 ↑cexp 14112 ♯chash 14379 √csqrt 15282 abscabs 15283 expce 16109 eceu 16110 logclog 26614 ψcchp 27154

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-inf2 9710 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262 ax-addf 11263

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-iin 5018 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-of 7714 df-om 7904 df-1st 8030 df-2nd 8031 df-supp 8202 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-2o 8523 df-er 8763 df-map 8886 df-pm 8887 df-ixp 8956 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-fsupp 9432 df-fi 9480 df-sup 9511 df-inf 9512 df-oi 9579 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-4 12358 df-5 12359 df-6 12360 df-7 12361 df-8 12362 df-9 12363 df-n0 12554 df-z 12640 df-dec 12759 df-uz 12904 df-q 13014 df-rp 13058 df-xneg 13175 df-xadd 13176 df-xmul 13177 df-ioo 13411 df-ioc 13412 df-ico 13413 df-icc 13414 df-fz 13568 df-fzo 13712 df-fl 13843 df-mod 13921 df-seq 14053 df-exp 14113 df-fac 14323 df-bc 14352 df-hash 14380 df-shft 15116 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-limsup 15517 df-clim 15534 df-rlim 15535 df-sum 15735 df-ef 16115 df-e 16116 df-sin 16117 df-cos 16118 df-pi 16120 df-struct 17194 df-sets 17211 df-slot 17229 df-ndx 17241 df-base 17259 df-ress 17288 df-plusg 17324 df-mulr 17325 df-starv 17326 df-sca 17327 df-vsca 17328 df-ip 17329 df-tset 17330 df-ple 17331 df-ds 17333 df-unif 17334 df-hom 17335 df-cco 17336 df-rest 17482 df-topn 17483 df-0g 17501 df-gsum 17502 df-topgen 17503 df-pt 17504 df-prds 17507 df-xrs 17562 df-qtop 17567 df-imas 17568 df-xps 17570 df-mre 17644 df-mrc 17645 df-acs 17647 df-mgm 18678 df-sgrp 18757 df-mnd 18773 df-submnd 18819 df-mulg 19108 df-cntz 19357 df-cmn 19824 df-psmet 21379 df-xmet 21380 df-met 21381 df-bl 21382 df-mopn 21383 df-fbas 21384 df-fg 21385 df-cnfld 21388 df-top 22921 df-topon 22938 df-topsp 22960 df-bases 22974 df-cld 23048 df-ntr 23049 df-cls 23050 df-nei 23127 df-lp 23165 df-perf 23166 df-cn 23256 df-cnp 23257 df-haus 23344 df-tx 23591 df-hmeo 23784 df-fil 23875 df-fm 23967 df-flim 23968 df-flf 23969 df-xms 24351 df-ms 24352 df-tms 24353 df-cncf 24923 df-limc 25921 df-dv 25922 df-log 26616

This theorem is referenced by: pntlemj 27665

W3C validator