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 27632

Description: Lemma for pntlemj 27633. (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 27624	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 ∈ ℝ⁺ ∧ 𝐷 ∈ ℝ⁺ ∧ 𝐹 ∈ ℝ⁺))
8	7	simp1d 1151	. . . . . . . . . . 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 27625	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸 ∈ ℝ⁺ ∧ 𝐾 ∈ ℝ⁺ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈ ℝ⁺)))
14	13	simp1d 1151	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
15	8, 14	rpmulcld 13039	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ⁺)
16		4re 12288	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
17		4pos 12314	. . . . . . . . . . 11 ⊢ 0 < 4
18	16, 17	elrpii 12982	. . . . . . . . . 10 ⊢ 4 ∈ ℝ⁺
19		rpdivcl 13006	. . . . . . . . . 10 ⊢ (((𝐿 · 𝐸) ∈ ℝ⁺ ∧ 4 ∈ ℝ⁺) → ((𝐿 · 𝐸) / 4) ∈ ℝ⁺)
20	15, 18, 19	sylancl 594	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℝ⁺)
21	20	rpred 13023	. . . . . . . 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 27627	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 ∈ ℝ⁺ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍)))))
28	27	simp1d 1151	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ ℝ⁺)
29		pntlem1.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ℝ⁺)
30	28, 29	rpdivcld 13040	. . . . . . . . 9 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ⁺)
31	30	rpred 13023	. . . . . . . 8 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℝ)
32	21, 31	remulcld 11198	. . . . . . 7 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ)
33		pntlem1.i	. . . . . . . . . 10 ⊢ 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))
34		fzfid 13972	. . . . . . . . . 10 ⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) ∈ Fin)
35	33, 34	eqeltrid 2856	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ Fin)
36		hashcl 14355	. . . . . . . . 9 ⊢ (𝐼 ∈ Fin → (♯‘𝐼) ∈ ℕ₀)
37	35, 36	syl 17	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐼) ∈ ℕ₀)
38	37	nn0red 12529	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐼) ∈ ℝ)
39	32	recnd 11196	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℂ)
40		1rp 12983	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ⁺
41		rpaddcl 13003	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ⁺ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → (1 + (𝐿 · 𝐸)) ∈ ℝ⁺)
42	40, 15, 41	sylancr 595	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ⁺)
43	42, 29	rpmulcld 13039	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ⁺)
44	28, 43	rpdivcld 13040	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ⁺)
45	44	rpred 13023	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ)
46		reflcl 13792	. . . . . . . . . . . . . 14 ⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
47	45, 46	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
48	47	recnd 11196	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℂ)
49		1cnd 11161	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
50	39, 48, 49	add32d 11397	. . . . . . . . . . 11 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) = (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
51		peano2re 11342	. . . . . . . . . . . . . 14 ⊢ ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ∈ ℝ → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ)
52	32, 51	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ∈ ℝ)
53	52, 47	readdcld 11197	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ)
54		reflcl 13792	. . . . . . . . . . . . . 14 ⊢ ((𝑍 / 𝑉) ∈ ℝ → (⌊‘(𝑍 / 𝑉)) ∈ ℝ)
55	31, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℝ)
56		peano2re 11342	. . . . . . . . . . . . 13 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ ℝ → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ)
57	55, 56	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ ℝ)
58	15	rphalfcld 13035	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ⁺)
59	58, 30	rpmulcld 13039	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ⁺)
60	59	rpred 13023	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) ∈ ℝ)
61	60, 45	readdcld 11197	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ∈ ℝ)
62		rpdivcl 13006	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((4 ∈ ℝ⁺ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → (4 / (𝐿 · 𝐸)) ∈ ℝ⁺)
63	18, 15, 62	sylancr 595	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ⁺)
64	63	rpred 13023	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℝ)
65	28	rpsqrtcld 15411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑍) ∈ ℝ⁺)
66	65	rpred 13023	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (√‘𝑍) ∈ ℝ)
67	27	simp3d 1153	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈 − 𝐸) · ((𝐿 · (𝐸↑2)) / (;32 · 𝐵))) · (log‘𝑍))))
68	67	simp1d 1151	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (√‘𝑍))
69	43	rpred 13023	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ∈ ℝ)
70	13	simp2d 1152	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐾 ∈ ℝ⁺)
71		pntlem1.j	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 ∈ (𝑀..^𝑁))
72		elfzoelz 13650	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ ℤ)
73	71, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐽 ∈ ℤ)
74	73	peano2zd 12666	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐽 + 1) ∈ ℤ)
75	70, 74	rpexpcld 14246	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ⁺)
76	75	rpred 13023	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ∈ ℝ)
77		pntlem1.V	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (((𝐾↑𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
78	77	simplrd 777	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾↑𝐽)))
79	70	rpcnd 13025	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐾 ∈ ℂ)
80	70, 73	rpexpcld 14246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝐾↑𝐽) ∈ ℝ⁺)
81	80	rpcnd 13025	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐾↑𝐽) ∈ ℂ)
82	79, 81	mulcomd 11189	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 27628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ_≥‘𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁 − 𝑀)))
86	85	simp1d 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝑀 ∈ ℕ)
87		elfzouz 13655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐽 ∈ (𝑀..^𝑁) → 𝐽 ∈ (ℤ_≥‘𝑀))
88	71, 87	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → 𝐽 ∈ (ℤ_≥‘𝑀))
89		eluznn 12905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑀 ∈ ℕ ∧ 𝐽 ∈ (ℤ_≥‘𝑀)) → 𝐽 ∈ ℕ)
90	86, 88, 89	syl2anc 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐽 ∈ ℕ)
91	90	nnnn0d 12528	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 ∈ ℕ₀)
92	79, 91	expp1d 14146	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) = ((𝐾↑𝐽) · 𝐾))
93	82, 92	eqtr4d 2790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐾 · (𝐾↑𝐽)) = (𝐾↑(𝐽 + 1)))
94	78, 93	breqtrd 5116	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾↑(𝐽 + 1)))
95	69, 76, 94	ltled 11317	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (𝐾↑(𝐽 + 1)))
96		fzofzp1 13756	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 27629	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝐽 + 1) ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
99	97, 98	mpdan 695	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑋 < (𝐾↑(𝐽 + 1)) ∧ (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍)))
100	99	simprd 498	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐾↑(𝐽 + 1)) ≤ (√‘𝑍))
101	69, 76, 66, 95, 100	letrd 11326	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍))
102	69, 66, 65	lemul2d 13067	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) · 𝑉) ≤ (√‘𝑍) ↔ ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍))))
103	101, 102	mpbid 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ ((√‘𝑍) · (√‘𝑍)))
104	28	rprege0d 13030	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑍 ∈ ℝ ∧ 0 ≤ 𝑍))
105		remsqsqrt 15255	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((√‘𝑍) · (√‘𝑍)) = 𝑍)
107	103, 106	breqtrd 5116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍)
108	28	rpred 13023	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑍 ∈ ℝ)
109	66, 108, 43	lemuldivd 13072	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((√‘𝑍) · ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ 𝑍 ↔ (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
110	107, 109	mpbid 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
111	29	rpcnd 13025	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑉 ∈ ℂ)
112	111	mullidd 11186	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑉) = 𝑉)
113		1red 11168	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℝ)
114	42	rpred 13023	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℝ)
115		1re 11167	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℝ
116		ltaddrp 13018	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1 ∈ ℝ ∧ (𝐿 · 𝐸) ∈ ℝ⁺) → 1 < (1 + (𝐿 · 𝐸)))
117	115, 15, 116	sylancr 595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 < (1 + (𝐿 · 𝐸)))
118	113, 114, 29, 117	ltmul1dd 13078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 · 𝑉) < ((1 + (𝐿 · 𝐸)) · 𝑉))
119	112, 118	eqbrtrrd 5114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉))
120	29, 43, 28	ltdiv2d 13046	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑉 < ((1 + (𝐿 · 𝐸)) · 𝑉) ↔ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉)))
121	119, 120	mpbid 234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) < (𝑍 / 𝑉))
122	45, 31, 121	ltled 11317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉))
123	66, 45, 31, 110, 122	letrd 11326	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (√‘𝑍) ≤ (𝑍 / 𝑉))
124	64, 66, 31, 68, 123	letrd 11326	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ≤ (𝑍 / 𝑉))
125	64, 31, 31, 124	leadd2dd 11788	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ ((𝑍 / 𝑉) + (𝑍 / 𝑉)))
126	30	rpcnd 13025	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑍 / 𝑉) ∈ ℂ)
127	126	2timesd 12450	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑍 / 𝑉)) = ((𝑍 / 𝑉) + (𝑍 / 𝑉)))
128	125, 127	breqtrrd 5118	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)))
129	31, 64	readdcld 11197	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ∈ ℝ)
130		2re 12278	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
131		remulcl 11144	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ) → (2 · (𝑍 / 𝑉)) ∈ ℝ)
132	130, 31, 131	sylancr 595	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑍 / 𝑉)) ∈ ℝ)
133	129, 132, 20	lemul2d 13067	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸))) ≤ (2 · (𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉)))))
134	128, 133	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) ≤ (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))
135	20	rpcnd 13025	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ∈ ℂ)
136	63	rpcnd 13025	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (4 / (𝐿 · 𝐸)) ∈ ℂ)
137	135, 126, 136	adddid 11192	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))))
138	15	rpcnne0d 13032	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0))
139		rpcnne0 12998	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 ∈ ℝ⁺ → (4 ∈ ℂ ∧ 4 ≠ 0))
140	18, 139	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (4 ∈ ℂ ∧ 4 ≠ 0))
141		divcan6 11884	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (𝐿 · 𝐸) ≠ 0) ∧ (4 ∈ ℂ ∧ 4 ≠ 0)) → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1)
142	138, 140, 141	syl2anc 592	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸))) = 1)
143	142	oveq2d 7397	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (((𝐿 · 𝐸) / 4) · (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1))
144	137, 143	eqtrd 2787	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((𝑍 / 𝑉) + (4 / (𝐿 · 𝐸)))) = ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1))
145		2cnd 12282	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℂ)
146	135, 145, 126	mulassd 11191	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))))
147	15	rpcnd 13025	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℂ)
148		2rp 12984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ⁺
149		rpcnne0 12998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 ∈ ℝ⁺ → (2 ∈ ℂ ∧ 2 ≠ 0))
150	148, 149	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (2 ∈ ℂ ∧ 2 ≠ 0))
151		divdiv1 11888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2)))
152	147, 150, 150, 151	syl3anc 1382	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) / 2) = ((𝐿 · 𝐸) / (2 · 2)))
153		2t2e4 12367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 · 2) = 4
154	153	oveq2i 7392	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐿 · 𝐸) / (2 · 2)) = ((𝐿 · 𝐸) / 4)
155	152, 154	eqtr2di 2804	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) = (((𝐿 · 𝐸) / 2) / 2))
156	155	oveq1d 7396	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((((𝐿 · 𝐸) / 2) / 2) · 2))
157	147	halfcld 12452	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℂ)
158	150	simprd 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 2 ≠ 0)
159	157, 145, 158	divcan1d 11954	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) / 2) · 2) = ((𝐿 · 𝐸) / 2))
160	156, 159	eqtrd 2787	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · 2) = ((𝐿 · 𝐸) / 2))
161	160	oveq1d 7396	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · 2) · (𝑍 / 𝑉)) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
162	146, 161	eqtr3d 2789	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (2 · (𝑍 / 𝑉))) = (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
163	134, 144, 162	3brtr3d 5121	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) ≤ (((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)))
164		flle 13795	. . . . . . . . . . . . . . 15 ⊢ ((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
165	45, 164	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) ≤ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))
166	52, 47, 60, 45, 163, 165	le2addd 11792	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ≤ ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
167	58	rpred 13023	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) ∈ ℝ)
168	42	rprecred 13034	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℝ)
169	167, 168	readdcld 11197	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) ∈ ℝ)
170	15	rpred 13023	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 · 𝐸) ∈ ℝ)
171	14	rpred 13023	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 ∈ ℝ)
172	8	rpred 13023	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 ∈ ℝ)
173		eliooord 13395	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ (0(,)1) → (0 < 𝐿 ∧ 𝐿 < 1))
174	4, 173	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (0 < 𝐿 ∧ 𝐿 < 1))
175	174	simprd 498	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐿 < 1)
176	172, 113, 14, 175	ltmul1dd 13078	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐿 · 𝐸) < (1 · 𝐸))
177	14	rpcnd 13025	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 ∈ ℂ)
178	177	mullidd 11186	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1 · 𝐸) = 𝐸)
179	176, 178	breqtrd 5116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 · 𝐸) < 𝐸)
180	13	simp3d 1153	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈 − 𝐸) ∈ ℝ⁺))
181	180	simp1d 1151	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐸 ∈ (0(,)1))
182		eliooord 13395	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐸 ∈ (0(,)1) → (0 < 𝐸 ∧ 𝐸 < 1))
183	181, 182	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1))
184	183	simprd 498	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐸 < 1)
185	170, 171, 113, 179, 184	lttrd 11330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 · 𝐸) < 1)
186	170, 113, 113, 185	ltadd2dd 11328	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < (1 + 1))
187		df-2 12266	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 = (1 + 1)
188	186, 187	breqtrrdi 5132	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) < 2)
189	42	rpregt0d 13029	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸))))
190	130	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 2 ∈ ℝ)
191		2pos 12308	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
192	191	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 0 < 2)
193	15	rpregt0d 13029	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸)))
194		ltdiv2 12064	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((1 + (𝐿 · 𝐸)) ∈ ℝ ∧ 0 < (1 + (𝐿 · 𝐸))) ∧ (2 ∈ ℝ ∧ 0 < 2) ∧ ((𝐿 · 𝐸) ∈ ℝ ∧ 0 < (𝐿 · 𝐸))) → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))))
195	189, 190, 192, 193, 194	syl121anc 1386	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) < 2 ↔ ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸)))))
196	188, 195	mpbid 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))
197	42	rpcnd 13025	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ∈ ℂ)
198	42	rpcnne0d 13032	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0))
199		divsubdir 11870	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ 1 ∈ ℂ ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))))
200	197, 49, 198, 199	syl3anc 1382	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))))
201		ax-1cn 11117	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℂ
202		pncan2 11423	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ (𝐿 · 𝐸) ∈ ℂ) → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸))
203	201, 147, 202	sylancr 595	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) − 1) = (𝐿 · 𝐸))
204	203	oveq1d 7396	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) − 1) / (1 + (𝐿 · 𝐸))) = ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))))
205		divid 11862	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0) → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1)
206	198, 205	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) = 1)
207	206	oveq1d 7396	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((1 + (𝐿 · 𝐸)) / (1 + (𝐿 · 𝐸))) − (1 / (1 + (𝐿 · 𝐸)))) = (1 − (1 / (1 + (𝐿 · 𝐸)))))
208	200, 204, 207	3eqtr3d 2795	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 · 𝐸) / (1 + (𝐿 · 𝐸))) = (1 − (1 / (1 + (𝐿 · 𝐸)))))
209	196, 208	breqtrd 5116	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸)))))
210	167, 168, 113	ltaddsubd 11773	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1 ↔ ((𝐿 · 𝐸) / 2) < (1 − (1 / (1 + (𝐿 · 𝐸))))))
211	209, 210	mpbird 259	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) < 1)
212	169, 113, 30, 211	ltmul1dd 13078	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) < (1 · (𝑍 / 𝑉)))
213		reccl 11838	. . . . . . . . . . . . . . . . 17 ⊢ (((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0) → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ)
214	198, 213	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 / (1 + (𝐿 · 𝐸))) ∈ ℂ)
215	157, 214, 126	adddird 11193	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))))
216	197, 111	mulcomd 11189	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) = (𝑉 · (1 + (𝐿 · 𝐸))))
217	216	oveq2d 7397	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
218	28	rpcnd 13025	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑍 ∈ ℂ)
219	29	rpcnne0d 13032	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0))
220		divdiv1 11888	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑍 ∈ ℂ ∧ (𝑉 ∈ ℂ ∧ 𝑉 ≠ 0) ∧ ((1 + (𝐿 · 𝐸)) ∈ ℂ ∧ (1 + (𝐿 · 𝐸)) ≠ 0)) → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
221	218, 219, 198, 220	syl3anc 1382	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = (𝑍 / (𝑉 · (1 + (𝐿 · 𝐸)))))
222	42	rpne0d 13028	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 + (𝐿 · 𝐸)) ≠ 0)
223	126, 197, 222	divrec2d 11957	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑍 / 𝑉) / (1 + (𝐿 · 𝐸))) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))
224	217, 221, 223	3eqtr2d 2793	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) = ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉)))
225	224	oveq2d 7397	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + ((1 / (1 + (𝐿 · 𝐸))) · (𝑍 / 𝑉))))
226	215, 225	eqtr4d 2790	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) + (1 / (1 + (𝐿 · 𝐸)))) · (𝑍 / 𝑉)) = ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))
227	126	mullidd 11186	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 · (𝑍 / 𝑉)) = (𝑍 / 𝑉))
228	212, 226, 227	3brtr3d 5121	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 2) · (𝑍 / 𝑉)) + (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) < (𝑍 / 𝑉))
229	53, 61, 31, 166, 228	lelttrd 11327	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (𝑍 / 𝑉))
230		fllep1 13797	. . . . . . . . . . . . 13 ⊢ ((𝑍 / 𝑉) ∈ ℝ → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1))
231	31, 230	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑍 / 𝑉) ≤ ((⌊‘(𝑍 / 𝑉)) + 1))
232	53, 31, 57, 229, 231	ltletrd 11329	. . . . . . . . . . 11 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + 1) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < ((⌊‘(𝑍 / 𝑉)) + 1))
233	50, 232	eqbrtrd 5112	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1))
234	32, 47	readdcld 11197	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) ∈ ℝ)
235	234, 55, 113	ltadd1d 11766	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) + 1) < ((⌊‘(𝑍 / 𝑉)) + 1)))
236	233, 235	mpbird 259	. . . . . . . . 9 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)))
237	32, 47, 55	ltaddsubd 11773	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) + (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) < (⌊‘(𝑍 / 𝑉)) ↔ (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))))))
238	236, 237	mpbid 234	. . . . . . . 8 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
239	31	flcld 13794	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℤ)
240		fzval3 13726	. . . . . . . . . . . 12 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ ℤ → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
241	239, 240	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉))) = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
242	33, 241	eqtrid 2799	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1)))
243	242	fveq2d 6856	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝐼) = (♯‘(((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)..^((⌊‘(𝑍 / 𝑉)) + 1))))
244		flword2 13809	. . . . . . . . . . . 12 ⊢ (((𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ∈ ℝ ∧ (𝑍 / 𝑉) ∈ ℝ ∧ (𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)) ≤ (𝑍 / 𝑉)) → (⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
245	45, 31, 122, 244	syl3anc 1382	. . . . . . . . . . 11 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
246		eluzp1p1 12853	. . . . . . . . . . 11 ⊢ ((⌊‘(𝑍 / 𝑉)) ∈ (ℤ_≥‘(⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))) → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ_≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
247	245, 246	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((⌊‘(𝑍 / 𝑉)) + 1) ∈ (ℤ_≥‘((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)))
248		hashfzo 14428	. . . . . . . . . 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 11196	. . . . . . . . . 10 ⊢ (𝜑 → (⌊‘(𝑍 / 𝑉)) ∈ ℂ)
251	250, 48, 49	pnpcan2d 11566	. . . . . . . . 9 ⊢ (𝜑 → (((⌊‘(𝑍 / 𝑉)) + 1) − ((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
252	243, 249, 251	3eqtrd 2791	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐼) = ((⌊‘(𝑍 / 𝑉)) − (⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉)))))
253	238, 252	breqtrrd 5118	. . . . . . 7 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) < (♯‘𝐼))
254	32, 38, 253	ltled 11317	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼))
255	21, 38, 30	lemuldivd 13072	. . . . . 6 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) · (𝑍 / 𝑉)) ≤ (♯‘𝐼) ↔ ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉))))
256	254, 255	mpbid 234	. . . . 5 ⊢ (𝜑 → ((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)))
257	29	rpred 13023	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ ℝ)
258	69, 76, 66, 94, 100	ltletrd 11329	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1 + (𝐿 · 𝐸)) · 𝑉) < (√‘𝑍))
259	257, 69, 66, 119, 258	lttrd 11330	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 < (√‘𝑍))
260	257, 66, 259	ltled 11317	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑉 ≤ (√‘𝑍))
261	29	rprege0d 13030	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑉 ∈ ℝ ∧ 0 ≤ 𝑉))
262	65	rprege0d 13030	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((√‘𝑍) ∈ ℝ ∧ 0 ≤ (√‘𝑍)))
263		le2sq 14133	. . . . . . . . . . . . . . 15 ⊢ (((𝑉 ∈ ℝ ∧ 0 ≤ 𝑉) ∧ ((√‘𝑍) ∈ ℝ ∧ 0 ≤ (√‘𝑍))) → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2)))
264	261, 262, 263	syl2anc 592	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉 ≤ (√‘𝑍) ↔ (𝑉↑2) ≤ ((√‘𝑍)↑2)))
265	260, 264	mpbid 234	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉↑2) ≤ ((√‘𝑍)↑2))
266		resqrtth 15254	. . . . . . . . . . . . . 14 ⊢ ((𝑍 ∈ ℝ ∧ 0 ≤ 𝑍) → ((√‘𝑍)↑2) = 𝑍)
267	104, 266	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘𝑍)↑2) = 𝑍)
268	265, 267	breqtrd 5116	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑉↑2) ≤ 𝑍)
269		2z 12589	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
270		rpexpcl 14079	. . . . . . . . . . . . . . 15 ⊢ ((𝑉 ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (𝑉↑2) ∈ ℝ⁺)
271	29, 269, 270	sylancl 594	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑉↑2) ∈ ℝ⁺)
272	271	rpred 13023	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑉↑2) ∈ ℝ)
273	272, 108, 28	lemul2d 13067	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑉↑2) ≤ 𝑍 ↔ (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍)))
274	268, 273	mpbid 234	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍 · 𝑍))
275	218	sqvald 14142	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍↑2) = (𝑍 · 𝑍))
276	274, 275	breqtrrd 5118	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍 · (𝑉↑2)) ≤ (𝑍↑2))
277	108	resqcld 14124	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍↑2) ∈ ℝ)
278	108, 277, 271	lemuldivd 13072	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑍 · (𝑉↑2)) ≤ (𝑍↑2) ↔ 𝑍 ≤ ((𝑍↑2) / (𝑉↑2))))
279	276, 278	mpbid 234	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ≤ ((𝑍↑2) / (𝑉↑2)))
280	29	rpne0d 13028	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ≠ 0)
281	218, 111, 280	sqdivd 14158	. . . . . . . . 9 ⊢ (𝜑 → ((𝑍 / 𝑉)↑2) = ((𝑍↑2) / (𝑉↑2)))
282	279, 281	breqtrrd 5118	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ≤ ((𝑍 / 𝑉)↑2))
283		rpexpcl 14079	. . . . . . . . . 10 ⊢ (((𝑍 / 𝑉) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((𝑍 / 𝑉)↑2) ∈ ℝ⁺)
284	30, 269, 283	sylancl 594	. . . . . . . . 9 ⊢ (𝜑 → ((𝑍 / 𝑉)↑2) ∈ ℝ⁺)
285	28, 284	logled 26658	. . . . . . . 8 ⊢ (𝜑 → (𝑍 ≤ ((𝑍 / 𝑉)↑2) ↔ (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2))))
286	282, 285	mpbid 234	. . . . . . 7 ⊢ (𝜑 → (log‘𝑍) ≤ (log‘((𝑍 / 𝑉)↑2)))
287		relogexp 26627	. . . . . . . 8 ⊢ (((𝑍 / 𝑉) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉))))
288	30, 269, 287	sylancl 594	. . . . . . 7 ⊢ (𝜑 → (log‘((𝑍 / 𝑉)↑2)) = (2 · (log‘(𝑍 / 𝑉))))
289	286, 288	breqtrd 5116	. . . . . 6 ⊢ (𝜑 → (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉))))
290	28	relogcld 26654	. . . . . . 7 ⊢ (𝜑 → (log‘𝑍) ∈ ℝ)
291	30	relogcld 26654	. . . . . . 7 ⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℝ)
292		ledivmul 12054	. . . . . . 7 ⊢ (((log‘𝑍) ∈ ℝ ∧ (log‘(𝑍 / 𝑉)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉)))))
293	290, 291, 190, 192, 292	syl112anc 1385	. . . . . 6 ⊢ (𝜑 → (((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)) ↔ (log‘𝑍) ≤ (2 · (log‘(𝑍 / 𝑉)))))
294	289, 293	mpbird 259	. . . . 5 ⊢ (𝜑 → ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉)))
295	20	rprege0d 13030	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) ∈ ℝ ∧ 0 ≤ ((𝐿 · 𝐸) / 4)))
296	38, 30	rerpdivcld 13054	. . . . . 6 ⊢ (𝜑 → ((♯‘𝐼) / (𝑍 / 𝑉)) ∈ ℝ)
297	27	simp2d 1152	. . . . . . . . . 10 ⊢ (𝜑 → (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)))
298	297	simp1d 1151	. . . . . . . . 9 ⊢ (𝜑 → 1 < 𝑍)
299	108, 298	rplogcld 26660	. . . . . . . 8 ⊢ (𝜑 → (log‘𝑍) ∈ ℝ⁺)
300	299	rphalfcld 13035	. . . . . . 7 ⊢ (𝜑 → ((log‘𝑍) / 2) ∈ ℝ⁺)
301	300	rprege0d 13030	. . . . . 6 ⊢ (𝜑 → (((log‘𝑍) / 2) ∈ ℝ ∧ 0 ≤ ((log‘𝑍) / 2)))
302		lemul12a 12035	. . . . . 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 847	. . . . 5 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 4) ≤ ((♯‘𝐼) / (𝑍 / 𝑉)) ∧ ((log‘𝑍) / 2) ≤ (log‘(𝑍 / 𝑉))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉)))))
304	256, 294, 303	mp2and 707	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) ≤ (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
305	299	rpcnd 13025	. . . . . 6 ⊢ (𝜑 → (log‘𝑍) ∈ ℂ)
306		8nn 12299	. . . . . . . 8 ⊢ 8 ∈ ℕ
307		nnrp 12991	. . . . . . . 8 ⊢ (8 ∈ ℕ → 8 ∈ ℝ⁺)
308	306, 307	ax-mp 5	. . . . . . 7 ⊢ 8 ∈ ℝ⁺
309		rpcnne0 12998	. . . . . . 7 ⊢ (8 ∈ ℝ⁺ → (8 ∈ ℂ ∧ 8 ≠ 0))
310	308, 309	mp1i 13	. . . . . 6 ⊢ (𝜑 → (8 ∈ ℂ ∧ 8 ≠ 0))
311		div23 11850	. . . . . 6 ⊢ (((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ ∧ (8 ∈ ℂ ∧ 8 ≠ 0)) → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍)))
312	147, 305, 310, 311	syl3anc 1382	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 8) · (log‘𝑍)))
313		divmuldiv 11877	. . . . . . 7 ⊢ ((((𝐿 · 𝐸) ∈ ℂ ∧ (log‘𝑍) ∈ ℂ) ∧ ((4 ∈ ℂ ∧ 4 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0))) → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)))
314	147, 305, 140, 150, 313	syl22anc 847	. . . . . 6 ⊢ (𝜑 → (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)))
315		4t2e8 12372	. . . . . . 7 ⊢ (4 · 2) = 8
316	315	oveq2i 7392	. . . . . 6 ⊢ (((𝐿 · 𝐸) · (log‘𝑍)) / (4 · 2)) = (((𝐿 · 𝐸) · (log‘𝑍)) / 8)
317	314, 316	eqtr2di 2804	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) · (log‘𝑍)) / 8) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)))
318	312, 317	eqtr3d 2789	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) = (((𝐿 · 𝐸) / 4) · ((log‘𝑍) / 2)))
319	38	recnd 11196	. . . . 5 ⊢ (𝜑 → (♯‘𝐼) ∈ ℂ)
320	291	recnd 11196	. . . . 5 ⊢ (𝜑 → (log‘(𝑍 / 𝑉)) ∈ ℂ)
321	30	rpcnne0d 13032	. . . . 5 ⊢ (𝜑 → ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0))
322		divass 11849	. . . . . 6 ⊢ (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))
323		div23 11850	. . . . . 6 ⊢ (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → (((♯‘𝐼) · (log‘(𝑍 / 𝑉))) / (𝑍 / 𝑉)) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
324	322, 323	eqtr3d 2789	. . . . 5 ⊢ (((♯‘𝐼) ∈ ℂ ∧ (log‘(𝑍 / 𝑉)) ∈ ℂ ∧ ((𝑍 / 𝑉) ∈ ℂ ∧ (𝑍 / 𝑉) ≠ 0)) → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
325	319, 320, 321, 324	syl3anc 1382	. . . 4 ⊢ (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) = (((♯‘𝐼) / (𝑍 / 𝑉)) · (log‘(𝑍 / 𝑉))))
326	304, 318, 325	3brtr4d 5122	. . 3 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))
327		rpdivcl 13006	. . . . . . 7 ⊢ (((𝐿 · 𝐸) ∈ ℝ⁺ ∧ 8 ∈ ℝ⁺) → ((𝐿 · 𝐸) / 8) ∈ ℝ⁺)
328	15, 308, 327	sylancl 594	. . . . . 6 ⊢ (𝜑 → ((𝐿 · 𝐸) / 8) ∈ ℝ⁺)
329	328, 299	rpmulcld 13039	. . . . 5 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ⁺)
330	329	rpred 13023	. . . 4 ⊢ (𝜑 → (((𝐿 · 𝐸) / 8) · (log‘𝑍)) ∈ ℝ)
331	291, 30	rerpdivcld 13054	. . . . 5 ⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℝ)
332	38, 331	remulcld 11198	. . . 4 ⊢ (𝜑 → ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ∈ ℝ)
333	180	simp3d 1153	. . . 4 ⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℝ⁺)
334	330, 332, 333	lemul2d 13067	. . 3 ⊢ (𝜑 → ((((𝐿 · 𝐸) / 8) · (log‘𝑍)) ≤ ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))) ↔ ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉))))))
335	326, 334	mpbid 234	. 2 ⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
336	333	rpcnd 13025	. . 3 ⊢ (𝜑 → (𝑈 − 𝐸) ∈ ℂ)
337	331	recnd 11196	. . 3 ⊢ (𝜑 → ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)) ∈ ℂ)
338	336, 319, 337	mul12d 11378	. 2 ⊢ (𝜑 → ((𝑈 − 𝐸) · ((♯‘𝐼) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))) = ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
339	335, 338	breqtrd 5116	1 ⊢ (𝜑 → ((𝑈 − 𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((♯‘𝐼) · ((𝑈 − 𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1095 = wceq 1550 ∈ wcel 2132 ≠ wne 2947 ∀wral 3066 ∃wrex 3076 class class class wbr 5090 ↦ cmpt 5171 ‘cfv 6506 (class class class)co 7381 Fincfn 8912 ℂcc 11057 ℝcr 11058 0cc0 11059 1c1 11060 + caddc 11062 · cmul 11064 +∞cpnf 11199 < clt 11202 ≤ cle 11203 − cmin 11400 / cdiv 11830 ℕcn 12196 2c2 12258 3c3 12259 4c4 12260 8c8 12264 ℕ₀cn0 12467 ℤcz 12554 cdc 12674 ℤ_≥cuz 12825 ℝ⁺crp 12979 (,)cioo 13335 [,)cico 13337 [,]cicc 13338 ...cfz 13498 ..^cfzo 13645 ⌊cfl 13786 ↑cexp 14060 ♯chash 14329 √csqrt 15232 abscabs 15233 expce 16063 eceu 16064 logclog 26585 ψcchp 27123

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1805 ax-4 1819 ax-5 1920 ax-6 1977 ax-7 2018 ax-8 2134 ax-9 2142 ax-10 2165 ax-11 2181 ax-12 2202 ax-ext 2724 ax-rep 5217 ax-sep 5236 ax-nul 5246 ax-pow 5312 ax-pr 5380 ax-un 7703 ax-inf2 9582 ax-cnex 11115 ax-resscn 11116 ax-1cn 11117 ax-icn 11118 ax-addcl 11119 ax-addrcl 11120 ax-mulcl 11121 ax-mulrcl 11122 ax-mulcom 11123 ax-addass 11124 ax-mulass 11125 ax-distr 11126 ax-i2m1 11127 ax-1ne0 11128 ax-1rid 11129 ax-rnegex 11130 ax-rrecex 11131 ax-cnre 11132 ax-pre-lttri 11133 ax-pre-lttrn 11134 ax-pre-ltadd 11135 ax-pre-mulgt0 11136 ax-pre-sup 11137 ax-addf 11138

This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3or 1096 df-3an 1097 df-tru 1553 df-fal 1563 df-ex 1790 df-nf 1794 df-sb 2081 df-mo 2556 df-eu 2586 df-clab 2731 df-cleq 2744 df-clel 2827 df-nfc 2901 df-ne 2948 df-nel 3052 df-ral 3067 df-rex 3077 df-rmo 3357 df-reu 3358 df-rab 3405 df-v 3446 df-sbc 3736 df-csb 3844 df-dif 3898 df-un 3900 df-in 3902 df-ss 3912 df-pss 3915 df-nul 4277 df-if 4471 df-pw 4547 df-sn 4573 df-pr 4575 df-tp 4577 df-op 4579 df-uni 4856 df-int 4896 df-iun 4941 df-iin 4942 df-br 5091 df-opab 5153 df-mpt 5172 df-tr 5198 df-id 5531 df-eprel 5536 df-po 5544 df-so 5545 df-fr 5589 df-se 5590 df-we 5591 df-xp 5642 df-rel 5643 df-cnv 5644 df-co 5645 df-dm 5646 df-rn 5647 df-res 5648 df-ima 5649 df-pred 6273 df-ord 6334 df-on 6335 df-lim 6336 df-suc 6337 df-iota 6462 df-fun 6508 df-fn 6509 df-f 6510 df-f1 6511 df-fo 6512 df-f1o 6513 df-fv 6514 df-isom 6515 df-riota 7338 df-ov 7384 df-oprab 7385 df-mpo 7386 df-of 7645 df-om 7832 df-1st 7955 df-2nd 7956 df-supp 8125 df-frecs 8246 df-wrecs 8277 df-recs 8326 df-rdg 8365 df-1o 8421 df-2o 8422 df-er 8662 df-map 8794 df-pm 8795 df-ixp 8865 df-en 8913 df-dom 8914 df-sdom 8915 df-fin 8916 df-fsupp 9294 df-fi 9343 df-sup 9374 df-inf 9375 df-oi 9444 df-card 9883 df-pnf 11204 df-mnf 11205 df-xr 11206 df-ltxr 11207 df-le 11208 df-sub 11402 df-neg 11403 df-div 11831 df-nn 12197 df-2 12266 df-3 12267 df-4 12268 df-5 12269 df-6 12270 df-7 12271 df-8 12272 df-9 12273 df-n0 12468 df-z 12555 df-dec 12675 df-uz 12826 df-q 12936 df-rp 12980 df-xneg 13100 df-xadd 13101 df-xmul 13102 df-ioo 13339 df-ioc 13340 df-ico 13341 df-icc 13342 df-fz 13499 df-fzo 13646 df-fl 13788 df-mod 13866 df-seq 14001 df-exp 14061 df-fac 14273 df-bc 14302 df-hash 14330 df-shft 15066 df-cj 15098 df-re 15099 df-im 15100 df-sqrt 15234 df-abs 15235 df-limsup 15470 df-clim 15487 df-rlim 15488 df-sum 15686 df-ef 16069 df-e 16070 df-sin 16071 df-cos 16072 df-pi 16074 df-struct 17155 df-sets 17172 df-slot 17190 df-ndx 17202 df-base 17218 df-ress 17239 df-plusg 17271 df-mulr 17272 df-starv 17273 df-sca 17274 df-vsca 17275 df-ip 17276 df-tset 17277 df-ple 17278 df-ds 17280 df-unif 17281 df-hom 17282 df-cco 17283 df-rest 17423 df-topn 17424 df-0g 17442 df-gsum 17443 df-topgen 17444 df-pt 17445 df-prds 17448 df-xrs 17504 df-qtop 17509 df-imas 17510 df-xps 17512 df-mre 17586 df-mrc 17587 df-acs 17589 df-mgm 18646 df-sgrp 18725 df-mnd 18741 df-submnd 18790 df-mulg 19082 df-cntz 19329 df-cmn 19794 df-psmet 21385 df-xmet 21386 df-met 21387 df-bl 21388 df-mopn 21389 df-fbas 21390 df-fg 21391 df-cnfld 21394 df-top 22923 df-topon 22940 df-topsp 22962 df-bases 22975 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 24349 df-ms 24350 df-tms 24351 df-cncf 24909 df-limc 25897 df-dv 25898 df-log 26587

This theorem is referenced by: pntlemj 27633

W3C validator