Theorem pntlemr

Description: Lemma for pntlemj . (Contributed by Mario Carneiro, 7-Jun-2016)

	Ref	Expression
Hypotheses	pntlem1.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
	pntlem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	pntlem1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	pntlem1.l	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
	pntlem1.d	⊢ 𝐷 = ( 𝐴 + 1 )
	pntlem1.f	⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
	pntlem1.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
	pntlem1.u2	⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
	pntlem1.e	⊢ 𝐸 = ( 𝑈 / 𝐷 )
	pntlem1.k	⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
	pntlem1.y	⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
	pntlem1.x	⊢ ( 𝜑 → ( 𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋 ) )
	pntlem1.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
	pntlem1.w	⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 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	pntlemr	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ ( ( ♯ ‘ 𝐼 ) · ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pntlem1.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		pntlem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3		pntlem1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
4		pntlem1.l	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
5		pntlem1.d	⊢ 𝐷 = ( 𝐴 + 1 )
6		pntlem1.f	⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
7		pntlem1.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
8		pntlem1.u2	⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
9		pntlem1.e	⊢ 𝐸 = ( 𝑈 / 𝐷 )
10		pntlem1.k	⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
11		pntlem1.y	⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
12		pntlem1.x	⊢ ( 𝜑 → ( 𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋 ) )
13		pntlem1.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
14		pntlem1.w	⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
15		pntlem1.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 [,) +∞ ) )
16		pntlem1.m	⊢ 𝑀 = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 )
17		pntlem1.n	⊢ 𝑁 = ( ⌊ ‘ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 2 ) )
18		pntlem1.U	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
19		pntlem1.K	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
20		pntlem1.o	⊢ 𝑂 = ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) )
21		pntlem1.v	⊢ ( 𝜑 → 𝑉 ∈ ℝ+ )
22		pntlem1.V	⊢ ( 𝜑 → ( ( ( 𝐾 ↑ 𝐽 ) < 𝑉 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑉 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
23		pntlem1.j	⊢ ( 𝜑 → 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) )
24		pntlem1.i	⊢ 𝐼 = ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) )
25	1 2 3 4 5 6	pntlemd	⊢ ( 𝜑 → ( 𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ∧ 𝐹 ∈ ℝ+ ) )
26	25	simp1d	⊢ ( 𝜑 → 𝐿 ∈ ℝ+ )
27	1 2 3 4 5 6 7 8 9 10	pntlemc	⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )
28	27	simp1d	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
29	26 28	rpmulcld	⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℝ+ )
30		4re	⊢ 4 ∈ ℝ
31		4pos	⊢ 0 < 4
32	30 31	elrpii	⊢ 4 ∈ ℝ+
33		rpdivcl	⊢ ( ( ( 𝐿 · 𝐸 ) ∈ ℝ+ ∧ 4 ∈ ℝ+ ) → ( ( 𝐿 · 𝐸 ) / 4 ) ∈ ℝ+ )
34	29 32 33	sylancl	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 4 ) ∈ ℝ+ )
35	34	rpred	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 4 ) ∈ ℝ )
36	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	pntlemb	⊢ ( 𝜑 → ( 𝑍 ∈ ℝ+ ∧ ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) ∧ ( ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) ∧ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) ) )
37	36	simp1d	⊢ ( 𝜑 → 𝑍 ∈ ℝ+ )
38	37 21	rpdivcld	⊢ ( 𝜑 → ( 𝑍 / 𝑉 ) ∈ ℝ+ )
39	38	rpred	⊢ ( 𝜑 → ( 𝑍 / 𝑉 ) ∈ ℝ )
40	35 39	remulcld	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) ∈ ℝ )
41		fzfid	⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) ∈ Fin )
42	24 41	eqeltrid	⊢ ( 𝜑 → 𝐼 ∈ Fin )
43		hashcl	⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
44	42 43	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
45	44	nn0red	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℝ )
46	40	recnd	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) ∈ ℂ )
47		1rp	⊢ 1 ∈ ℝ+
48		rpaddcl	⊢ ( ( 1 ∈ ℝ+ ∧ ( 𝐿 · 𝐸 ) ∈ ℝ+ ) → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
49	47 29 48	sylancr	⊢ ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
50	49 21	rpmulcld	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ∈ ℝ+ )
51	37 50	rpdivcld	⊢ ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ+ )
52	51	rpred	⊢ ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ )
53		reflcl	⊢ ( ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℝ )
54	52 53	syl	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℝ )
55	54	recnd	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℂ )
56		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
57	46 55 56	add32d	⊢ ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) + 1 ) = ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) )
58		peano2re	⊢ ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) ∈ ℝ → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ℝ )
59	40 58	syl	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ℝ )
60	59 54	readdcld	⊢ ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) ∈ ℝ )
61		reflcl	⊢ ( ( 𝑍 / 𝑉 ) ∈ ℝ → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℝ )
62	39 61	syl	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℝ )
63		peano2re	⊢ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ℝ )
64	62 63	syl	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ℝ )
65	29	rphalfcld	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 2 ) ∈ ℝ+ )
66	65 38	rpmulcld	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) ∈ ℝ+ )
67	66	rpred	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) ∈ ℝ )
68	67 52	readdcld	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℝ )
69		rpdivcl	⊢ ( ( 4 ∈ ℝ+ ∧ ( 𝐿 · 𝐸 ) ∈ ℝ+ ) → ( 4 / ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
70	32 29 69	sylancr	⊢ ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
71	70	rpred	⊢ ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ∈ ℝ )
72	37	rpsqrtcld	⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ∈ ℝ+ )
73	72	rpred	⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ∈ ℝ )
74	36	simp3d	⊢ ( 𝜑 → ( ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) ∧ ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) + 2 ) ≤ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ∧ ( ( 𝑈 · 3 ) + 𝐶 ) ≤ ( ( ( 𝑈 − 𝐸 ) · ( ( 𝐿 · ( 𝐸 ↑ 2 ) ) / ( ; 3 2 · 𝐵 ) ) ) · ( log ‘ 𝑍 ) ) ) )
75	74	simp1d	⊢ ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( √ ‘ 𝑍 ) )
76	50	rpred	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ∈ ℝ )
77	27	simp2d	⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
78		elfzoelz	⊢ ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
79	23 78	syl	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
80	79	peano2zd	⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ℤ )
81	77 80	rpexpcld	⊢ ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∈ ℝ+ )
82	81	rpred	⊢ ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∈ ℝ )
83	22	simplrd	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) )
84	77	rpcnd	⊢ ( 𝜑 → 𝐾 ∈ ℂ )
85	77 79	rpexpcld	⊢ ( 𝜑 → ( 𝐾 ↑ 𝐽 ) ∈ ℝ+ )
86	85	rpcnd	⊢ ( 𝜑 → ( 𝐾 ↑ 𝐽 ) ∈ ℂ )
87	84 86	mulcomd	⊢ ( 𝜑 → ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) = ( ( 𝐾 ↑ 𝐽 ) · 𝐾 ) )
88	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pntlemg	⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ≤ ( 𝑁 − 𝑀 ) ) )
89	88	simp1d	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
90		elfzouz	⊢ ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) )
91	23 90	syl	⊢ ( 𝜑 → 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) )
92		eluznn	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐽 ∈ ℕ )
93	89 91 92	syl2anc	⊢ ( 𝜑 → 𝐽 ∈ ℕ )
94	93	nnnn0d	⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
95	84 94	expp1d	⊢ ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) = ( ( 𝐾 ↑ 𝐽 ) · 𝐾 ) )
96	87 95	eqtr4d	⊢ ( 𝜑 → ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) = ( 𝐾 ↑ ( 𝐽 + 1 ) ) )
97	83 96	breqtrd	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 ↑ ( 𝐽 + 1 ) ) )
98	76 82 97	ltled	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ≤ ( 𝐾 ↑ ( 𝐽 + 1 ) ) )
99		fzofzp1	⊢ ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐽 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
100	23 99	syl	⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
101	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pntlemh	⊢ ( ( 𝜑 ∧ ( 𝐽 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑋 < ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∧ ( 𝐾 ↑ ( 𝐽 + 1 ) ) ≤ ( √ ‘ 𝑍 ) ) )
102	100 101	mpdan	⊢ ( 𝜑 → ( 𝑋 < ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∧ ( 𝐾 ↑ ( 𝐽 + 1 ) ) ≤ ( √ ‘ 𝑍 ) ) )
103	102	simprd	⊢ ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) ≤ ( √ ‘ 𝑍 ) )
104	76 82 73 98 103	letrd	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ≤ ( √ ‘ 𝑍 ) )
105	76 73 72	lemul2d	⊢ ( 𝜑 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ≤ ( √ ‘ 𝑍 ) ↔ ( ( √ ‘ 𝑍 ) · ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) ) )
106	104 105	mpbid	⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) · ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) )
107	37	rprege0d	⊢ ( 𝜑 → ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) )
108		remsqsqrt	⊢ ( ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) → ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) = 𝑍 )
109	107 108	syl	⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) = 𝑍 )
110	106 109	breqtrd	⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) · ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ 𝑍 )
111	37	rpred	⊢ ( 𝜑 → 𝑍 ∈ ℝ )
112	73 111 50	lemuldivd	⊢ ( 𝜑 → ( ( ( √ ‘ 𝑍 ) · ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ 𝑍 ↔ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) )
113	110 112	mpbid	⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
114	21	rpcnd	⊢ ( 𝜑 → 𝑉 ∈ ℂ )
115	114	mullidd	⊢ ( 𝜑 → ( 1 · 𝑉 ) = 𝑉 )
116		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
117	49	rpred	⊢ ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ )
118		1re	⊢ 1 ∈ ℝ
119		ltaddrp	⊢ ( ( 1 ∈ ℝ ∧ ( 𝐿 · 𝐸 ) ∈ ℝ+ ) → 1 < ( 1 + ( 𝐿 · 𝐸 ) ) )
120	118 29 119	sylancr	⊢ ( 𝜑 → 1 < ( 1 + ( 𝐿 · 𝐸 ) ) )
121	116 117 21 120	ltmul1dd	⊢ ( 𝜑 → ( 1 · 𝑉 ) < ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) )
122	115 121	eqbrtrrd	⊢ ( 𝜑 → 𝑉 < ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) )
123	21 50 37	ltdiv2d	⊢ ( 𝜑 → ( 𝑉 < ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ↔ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) < ( 𝑍 / 𝑉 ) ) )
124	122 123	mpbid	⊢ ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) < ( 𝑍 / 𝑉 ) )
125	52 39 124	ltled	⊢ ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ ( 𝑍 / 𝑉 ) )
126	73 52 39 113 125	letrd	⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑉 ) )
127	71 73 39 75 126	letrd	⊢ ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ≤ ( 𝑍 / 𝑉 ) )
128	71 39 39 127	leadd2dd	⊢ ( 𝜑 → ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ≤ ( ( 𝑍 / 𝑉 ) + ( 𝑍 / 𝑉 ) ) )
129	38	rpcnd	⊢ ( 𝜑 → ( 𝑍 / 𝑉 ) ∈ ℂ )
130	129	2timesd	⊢ ( 𝜑 → ( 2 · ( 𝑍 / 𝑉 ) ) = ( ( 𝑍 / 𝑉 ) + ( 𝑍 / 𝑉 ) ) )
131	128 130	breqtrrd	⊢ ( 𝜑 → ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ≤ ( 2 · ( 𝑍 / 𝑉 ) ) )
132	39 71	readdcld	⊢ ( 𝜑 → ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ∈ ℝ )
133		2re	⊢ 2 ∈ ℝ
134		remulcl	⊢ ( ( 2 ∈ ℝ ∧ ( 𝑍 / 𝑉 ) ∈ ℝ ) → ( 2 · ( 𝑍 / 𝑉 ) ) ∈ ℝ )
135	133 39 134	sylancr	⊢ ( 𝜑 → ( 2 · ( 𝑍 / 𝑉 ) ) ∈ ℝ )
136	132 135 34	lemul2d	⊢ ( 𝜑 → ( ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ≤ ( 2 · ( 𝑍 / 𝑉 ) ) ↔ ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ) ≤ ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 2 · ( 𝑍 / 𝑉 ) ) ) ) )
137	131 136	mpbid	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ) ≤ ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 2 · ( 𝑍 / 𝑉 ) ) ) )
138	34	rpcnd	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 4 ) ∈ ℂ )
139	70	rpcnd	⊢ ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ∈ ℂ )
140	138 129 139	adddid	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ) = ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 4 / ( 𝐿 · 𝐸 ) ) ) ) )
141	29	rpcnne0d	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) ∈ ℂ ∧ ( 𝐿 · 𝐸 ) ≠ 0 ) )
142		rpcnne0	⊢ ( 4 ∈ ℝ+ → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
143	32 142	mp1i	⊢ ( 𝜑 → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
144		divcan6	⊢ ( ( ( ( 𝐿 · 𝐸 ) ∈ ℂ ∧ ( 𝐿 · 𝐸 ) ≠ 0 ) ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 4 / ( 𝐿 · 𝐸 ) ) ) = 1 )
145	141 143 144	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 4 / ( 𝐿 · 𝐸 ) ) ) = 1 )
146	145	oveq2d	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 4 / ( 𝐿 · 𝐸 ) ) ) ) = ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) )
147	140 146	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( 𝑍 / 𝑉 ) + ( 4 / ( 𝐿 · 𝐸 ) ) ) ) = ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) )
148		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
149	138 148 129	mulassd	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · 2 ) · ( 𝑍 / 𝑉 ) ) = ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 2 · ( 𝑍 / 𝑉 ) ) ) )
150	29	rpcnd	⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℂ )
151		2rp	⊢ 2 ∈ ℝ+
152		rpcnne0	⊢ ( 2 ∈ ℝ+ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
153	151 152	mp1i	⊢ ( 𝜑 → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
154		divdiv1	⊢ ( ( ( 𝐿 · 𝐸 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 𝐿 · 𝐸 ) / 2 ) / 2 ) = ( ( 𝐿 · 𝐸 ) / ( 2 · 2 ) ) )
155	150 153 153 154	syl3anc	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 2 ) / 2 ) = ( ( 𝐿 · 𝐸 ) / ( 2 · 2 ) ) )
156		2t2e4	⊢ ( 2 · 2 ) = 4
157	156	oveq2i	⊢ ( ( 𝐿 · 𝐸 ) / ( 2 · 2 ) ) = ( ( 𝐿 · 𝐸 ) / 4 )
158	155 157	eqtr2di	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 4 ) = ( ( ( 𝐿 · 𝐸 ) / 2 ) / 2 ) )
159	158	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · 2 ) = ( ( ( ( 𝐿 · 𝐸 ) / 2 ) / 2 ) · 2 ) )
160	150	halfcld	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 2 ) ∈ ℂ )
161	153	simprd	⊢ ( 𝜑 → 2 ≠ 0 )
162	160 148 161	divcan1d	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) / 2 ) · 2 ) = ( ( 𝐿 · 𝐸 ) / 2 ) )
163	159 162	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · 2 ) = ( ( 𝐿 · 𝐸 ) / 2 ) )
164	163	oveq1d	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · 2 ) · ( 𝑍 / 𝑉 ) ) = ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) )
165	149 164	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 2 · ( 𝑍 / 𝑉 ) ) ) = ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) )
166	137 147 165	3brtr3d	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) ≤ ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) )
167		flle	⊢ ( ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
168	52 167	syl	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
169	59 54 67 52 166 168	le2addd	⊢ ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) ≤ ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) )
170	65	rpred	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 2 ) ∈ ℝ )
171	49	rprecred	⊢ ( 𝜑 → ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ∈ ℝ )
172	170 171	readdcld	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 2 ) + ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) ∈ ℝ )
173	29	rpred	⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℝ )
174	28	rpred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
175	26	rpred	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
176		eliooord	⊢ ( 𝐿 ∈ ( 0 (,) 1 ) → ( 0 < 𝐿 ∧ 𝐿 < 1 ) )
177	4 176	syl	⊢ ( 𝜑 → ( 0 < 𝐿 ∧ 𝐿 < 1 ) )
178	177	simprd	⊢ ( 𝜑 → 𝐿 < 1 )
179	175 116 28 178	ltmul1dd	⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) < ( 1 · 𝐸 ) )
180	28	rpcnd	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
181	180	mullidd	⊢ ( 𝜑 → ( 1 · 𝐸 ) = 𝐸 )
182	179 181	breqtrd	⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) < 𝐸 )
183	27	simp3d	⊢ ( 𝜑 → ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
184	183	simp1d	⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
185		eliooord	⊢ ( 𝐸 ∈ ( 0 (,) 1 ) → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
186	184 185	syl	⊢ ( 𝜑 → ( 0 < 𝐸 ∧ 𝐸 < 1 ) )
187	186	simprd	⊢ ( 𝜑 → 𝐸 < 1 )
188	173 174 116 182 187	lttrd	⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) < 1 )
189	173 116 116 188	ltadd2dd	⊢ ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) < ( 1 + 1 ) )
190		df-2	⊢ 2 = ( 1 + 1 )
191	189 190	breqtrrdi	⊢ ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) < 2 )
192	49	rpregt0d	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ ∧ 0 < ( 1 + ( 𝐿 · 𝐸 ) ) ) )
193	133	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
194		2pos	⊢ 0 < 2
195	194	a1i	⊢ ( 𝜑 → 0 < 2 )
196	29	rpregt0d	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) ∈ ℝ ∧ 0 < ( 𝐿 · 𝐸 ) ) )
197		ltdiv2	⊢ ( ( ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ ∧ 0 < ( 1 + ( 𝐿 · 𝐸 ) ) ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ∧ ( ( 𝐿 · 𝐸 ) ∈ ℝ ∧ 0 < ( 𝐿 · 𝐸 ) ) ) → ( ( 1 + ( 𝐿 · 𝐸 ) ) < 2 ↔ ( ( 𝐿 · 𝐸 ) / 2 ) < ( ( 𝐿 · 𝐸 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
198	192 193 195 196 197	syl121anc	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) < 2 ↔ ( ( 𝐿 · 𝐸 ) / 2 ) < ( ( 𝐿 · 𝐸 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
199	191 198	mpbid	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 2 ) < ( ( 𝐿 · 𝐸 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) )
200	49	rpcnd	⊢ ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ )
201	49	rpcnne0d	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ ∧ ( 1 + ( 𝐿 · 𝐸 ) ) ≠ 0 ) )
202		divsubdir	⊢ ( ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ ∧ ( 1 + ( 𝐿 · 𝐸 ) ) ≠ 0 ) ) → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) − 1 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( ( ( 1 + ( 𝐿 · 𝐸 ) ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
203	200 56 201 202	syl3anc	⊢ ( 𝜑 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) − 1 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( ( ( 1 + ( 𝐿 · 𝐸 ) ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
204		ax-1cn	⊢ 1 ∈ ℂ
205		pncan2	⊢ ( ( 1 ∈ ℂ ∧ ( 𝐿 · 𝐸 ) ∈ ℂ ) → ( ( 1 + ( 𝐿 · 𝐸 ) ) − 1 ) = ( 𝐿 · 𝐸 ) )
206	204 150 205	sylancr	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) − 1 ) = ( 𝐿 · 𝐸 ) )
207	206	oveq1d	⊢ ( 𝜑 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) − 1 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( ( 𝐿 · 𝐸 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) )
208		divid	⊢ ( ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ ∧ ( 1 + ( 𝐿 · 𝐸 ) ) ≠ 0 ) → ( ( 1 + ( 𝐿 · 𝐸 ) ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = 1 )
209	201 208	syl	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = 1 )
210	209	oveq1d	⊢ ( 𝜑 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) = ( 1 − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
211	203 207 210	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( 1 − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
212	199 211	breqtrd	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 2 ) < ( 1 − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
213	170 171 116	ltaddsubd	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) + ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) < 1 ↔ ( ( 𝐿 · 𝐸 ) / 2 ) < ( 1 − ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) ) )
214	212 213	mpbird	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 2 ) + ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) < 1 )
215	172 116 38 214	ltmul1dd	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) + ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) · ( 𝑍 / 𝑉 ) ) < ( 1 · ( 𝑍 / 𝑉 ) ) )
216		reccl	⊢ ( ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ ∧ ( 1 + ( 𝐿 · 𝐸 ) ) ≠ 0 ) → ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ∈ ℂ )
217	201 216	syl	⊢ ( 𝜑 → ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ∈ ℂ )
218	160 217 129	adddird	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) + ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) · ( 𝑍 / 𝑉 ) ) = ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) · ( 𝑍 / 𝑉 ) ) ) )
219	200 114	mulcomd	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) = ( 𝑉 · ( 1 + ( 𝐿 · 𝐸 ) ) ) )
220	219	oveq2d	⊢ ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) = ( 𝑍 / ( 𝑉 · ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
221	37	rpcnd	⊢ ( 𝜑 → 𝑍 ∈ ℂ )
222	21	rpcnne0d	⊢ ( 𝜑 → ( 𝑉 ∈ ℂ ∧ 𝑉 ≠ 0 ) )
223		divdiv1	⊢ ( ( 𝑍 ∈ ℂ ∧ ( 𝑉 ∈ ℂ ∧ 𝑉 ≠ 0 ) ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℂ ∧ ( 1 + ( 𝐿 · 𝐸 ) ) ≠ 0 ) ) → ( ( 𝑍 / 𝑉 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( 𝑍 / ( 𝑉 · ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
224	221 222 201 223	syl3anc	⊢ ( 𝜑 → ( ( 𝑍 / 𝑉 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( 𝑍 / ( 𝑉 · ( 1 + ( 𝐿 · 𝐸 ) ) ) ) )
225	49	rpne0d	⊢ ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) ≠ 0 )
226	129 200 225	divrec2d	⊢ ( 𝜑 → ( ( 𝑍 / 𝑉 ) / ( 1 + ( 𝐿 · 𝐸 ) ) ) = ( ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) · ( 𝑍 / 𝑉 ) ) )
227	220 224 226	3eqtr2d	⊢ ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) = ( ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) · ( 𝑍 / 𝑉 ) ) )
228	227	oveq2d	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) = ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) · ( 𝑍 / 𝑉 ) ) ) )
229	218 228	eqtr4d	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) + ( 1 / ( 1 + ( 𝐿 · 𝐸 ) ) ) ) · ( 𝑍 / 𝑉 ) ) = ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) )
230	129	mullidd	⊢ ( 𝜑 → ( 1 · ( 𝑍 / 𝑉 ) ) = ( 𝑍 / 𝑉 ) )
231	215 229 230	3brtr3d	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 2 ) · ( 𝑍 / 𝑉 ) ) + ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) < ( 𝑍 / 𝑉 ) )
232	60 68 39 169 231	lelttrd	⊢ ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) < ( 𝑍 / 𝑉 ) )
233		fllep1	⊢ ( ( 𝑍 / 𝑉 ) ∈ ℝ → ( 𝑍 / 𝑉 ) ≤ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) )
234	39 233	syl	⊢ ( 𝜑 → ( 𝑍 / 𝑉 ) ≤ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) )
235	60 39 64 232 234	ltletrd	⊢ ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + 1 ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) < ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) )
236	57 235	eqbrtrd	⊢ ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) + 1 ) < ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) )
237	40 54	readdcld	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) ∈ ℝ )
238	237 62 116	ltadd1d	⊢ ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) < ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ↔ ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) + 1 ) < ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) )
239	236 238	mpbird	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) < ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) )
240	40 54 62	ltaddsubd	⊢ ( 𝜑 → ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) + ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) < ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ↔ ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) < ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) − ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) ) )
241	239 240	mpbid	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) < ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) − ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) )
242	39	flcld	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℤ )
243		fzval3	⊢ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℤ → ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ..^ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) )
244	242 243	syl	⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ..^ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) )
245	24 244	eqtrid	⊢ ( 𝜑 → 𝐼 = ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ..^ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) )
246	245	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) = ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ..^ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) ) )
247		flword2	⊢ ( ( ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ ∧ ( 𝑍 / 𝑉 ) ∈ ℝ ∧ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ ( 𝑍 / 𝑉 ) ) → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) )
248	52 39 125 247	syl3anc	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) )
249		eluzp1p1	⊢ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) → ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) )
250	248 249	syl	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) )
251		hashfzo	⊢ ( ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) → ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ..^ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) − ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) )
252	250 251	syl	⊢ ( 𝜑 → ( ♯ ‘ ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ..^ ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) − ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) )
253	62	recnd	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ∈ ℂ )
254	253 55 56	pnpcan2d	⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) + 1 ) − ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) = ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) − ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) )
255	246 252 254	3eqtrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) = ( ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) − ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ) )
256	241 255	breqtrrd	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) < ( ♯ ‘ 𝐼 ) )
257	40 45 256	ltled	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) ≤ ( ♯ ‘ 𝐼 ) )
258	35 45 38	lemuldivd	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( 𝑍 / 𝑉 ) ) ≤ ( ♯ ‘ 𝐼 ) ↔ ( ( 𝐿 · 𝐸 ) / 4 ) ≤ ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) ) )
259	257 258	mpbid	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 4 ) ≤ ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) )
260	21	rpred	⊢ ( 𝜑 → 𝑉 ∈ ℝ )
261	76 82 73 97 103	ltletrd	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( √ ‘ 𝑍 ) )
262	260 76 73 122 261	lttrd	⊢ ( 𝜑 → 𝑉 < ( √ ‘ 𝑍 ) )
263	260 73 262	ltled	⊢ ( 𝜑 → 𝑉 ≤ ( √ ‘ 𝑍 ) )
264	21	rprege0d	⊢ ( 𝜑 → ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) )
265	72	rprege0d	⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑍 ) ) )
266		le2sq	⊢ ( ( ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ∧ ( ( √ ‘ 𝑍 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑍 ) ) ) → ( 𝑉 ≤ ( √ ‘ 𝑍 ) ↔ ( 𝑉 ↑ 2 ) ≤ ( ( √ ‘ 𝑍 ) ↑ 2 ) ) )
267	264 265 266	syl2anc	⊢ ( 𝜑 → ( 𝑉 ≤ ( √ ‘ 𝑍 ) ↔ ( 𝑉 ↑ 2 ) ≤ ( ( √ ‘ 𝑍 ) ↑ 2 ) ) )
268	263 267	mpbid	⊢ ( 𝜑 → ( 𝑉 ↑ 2 ) ≤ ( ( √ ‘ 𝑍 ) ↑ 2 ) )
269		resqrtth	⊢ ( ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) → ( ( √ ‘ 𝑍 ) ↑ 2 ) = 𝑍 )
270	107 269	syl	⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) ↑ 2 ) = 𝑍 )
271	268 270	breqtrd	⊢ ( 𝜑 → ( 𝑉 ↑ 2 ) ≤ 𝑍 )
272		2z	⊢ 2 ∈ ℤ
273		rpexpcl	⊢ ( ( 𝑉 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝑉 ↑ 2 ) ∈ ℝ+ )
274	21 272 273	sylancl	⊢ ( 𝜑 → ( 𝑉 ↑ 2 ) ∈ ℝ+ )
275	274	rpred	⊢ ( 𝜑 → ( 𝑉 ↑ 2 ) ∈ ℝ )
276	275 111 37	lemul2d	⊢ ( 𝜑 → ( ( 𝑉 ↑ 2 ) ≤ 𝑍 ↔ ( 𝑍 · ( 𝑉 ↑ 2 ) ) ≤ ( 𝑍 · 𝑍 ) ) )
277	271 276	mpbid	⊢ ( 𝜑 → ( 𝑍 · ( 𝑉 ↑ 2 ) ) ≤ ( 𝑍 · 𝑍 ) )
278	221	sqvald	⊢ ( 𝜑 → ( 𝑍 ↑ 2 ) = ( 𝑍 · 𝑍 ) )
279	277 278	breqtrrd	⊢ ( 𝜑 → ( 𝑍 · ( 𝑉 ↑ 2 ) ) ≤ ( 𝑍 ↑ 2 ) )
280	111	resqcld	⊢ ( 𝜑 → ( 𝑍 ↑ 2 ) ∈ ℝ )
281	111 280 274	lemuldivd	⊢ ( 𝜑 → ( ( 𝑍 · ( 𝑉 ↑ 2 ) ) ≤ ( 𝑍 ↑ 2 ) ↔ 𝑍 ≤ ( ( 𝑍 ↑ 2 ) / ( 𝑉 ↑ 2 ) ) ) )
282	279 281	mpbid	⊢ ( 𝜑 → 𝑍 ≤ ( ( 𝑍 ↑ 2 ) / ( 𝑉 ↑ 2 ) ) )
283	21	rpne0d	⊢ ( 𝜑 → 𝑉 ≠ 0 )
284	221 114 283	sqdivd	⊢ ( 𝜑 → ( ( 𝑍 / 𝑉 ) ↑ 2 ) = ( ( 𝑍 ↑ 2 ) / ( 𝑉 ↑ 2 ) ) )
285	282 284	breqtrrd	⊢ ( 𝜑 → 𝑍 ≤ ( ( 𝑍 / 𝑉 ) ↑ 2 ) )
286		rpexpcl	⊢ ( ( ( 𝑍 / 𝑉 ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( 𝑍 / 𝑉 ) ↑ 2 ) ∈ ℝ+ )
287	38 272 286	sylancl	⊢ ( 𝜑 → ( ( 𝑍 / 𝑉 ) ↑ 2 ) ∈ ℝ+ )
288	37 287	logled	⊢ ( 𝜑 → ( 𝑍 ≤ ( ( 𝑍 / 𝑉 ) ↑ 2 ) ↔ ( log ‘ 𝑍 ) ≤ ( log ‘ ( ( 𝑍 / 𝑉 ) ↑ 2 ) ) ) )
289	285 288	mpbid	⊢ ( 𝜑 → ( log ‘ 𝑍 ) ≤ ( log ‘ ( ( 𝑍 / 𝑉 ) ↑ 2 ) ) )
290		relogexp	⊢ ( ( ( 𝑍 / 𝑉 ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( log ‘ ( ( 𝑍 / 𝑉 ) ↑ 2 ) ) = ( 2 · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
291	38 272 290	sylancl	⊢ ( 𝜑 → ( log ‘ ( ( 𝑍 / 𝑉 ) ↑ 2 ) ) = ( 2 · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
292	289 291	breqtrd	⊢ ( 𝜑 → ( log ‘ 𝑍 ) ≤ ( 2 · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
293	37	relogcld	⊢ ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℝ )
294	38	relogcld	⊢ ( 𝜑 → ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℝ )
295		ledivmul	⊢ ( ( ( log ‘ 𝑍 ) ∈ ℝ ∧ ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( log ‘ 𝑍 ) / 2 ) ≤ ( log ‘ ( 𝑍 / 𝑉 ) ) ↔ ( log ‘ 𝑍 ) ≤ ( 2 · ( log ‘ ( 𝑍 / 𝑉 ) ) ) ) )
296	293 294 193 195 295	syl112anc	⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) / 2 ) ≤ ( log ‘ ( 𝑍 / 𝑉 ) ) ↔ ( log ‘ 𝑍 ) ≤ ( 2 · ( log ‘ ( 𝑍 / 𝑉 ) ) ) ) )
297	292 296	mpbird	⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) / 2 ) ≤ ( log ‘ ( 𝑍 / 𝑉 ) ) )
298	34	rprege0d	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐿 · 𝐸 ) / 4 ) ) )
299	45 38	rerpdivcld	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) ∈ ℝ )
300	36	simp2d	⊢ ( 𝜑 → ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) )
301	300	simp1d	⊢ ( 𝜑 → 1 < 𝑍 )
302	111 301	rplogcld	⊢ ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℝ+ )
303	302	rphalfcld	⊢ ( 𝜑 → ( ( log ‘ 𝑍 ) / 2 ) ∈ ℝ+ )
304	303	rprege0d	⊢ ( 𝜑 → ( ( ( log ‘ 𝑍 ) / 2 ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ 𝑍 ) / 2 ) ) )
305		lemul12a	⊢ ( ( ( ( ( ( 𝐿 · 𝐸 ) / 4 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐿 · 𝐸 ) / 4 ) ) ∧ ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) ∈ ℝ ) ∧ ( ( ( ( log ‘ 𝑍 ) / 2 ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ 𝑍 ) / 2 ) ) ∧ ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℝ ) ) → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) ≤ ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) ∧ ( ( log ‘ 𝑍 ) / 2 ) ≤ ( log ‘ ( 𝑍 / 𝑉 ) ) ) → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) ≤ ( ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) ) )
306	298 299 304 294 305	syl22anc	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 4 ) ≤ ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) ∧ ( ( log ‘ 𝑍 ) / 2 ) ≤ ( log ‘ ( 𝑍 / 𝑉 ) ) ) → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) ≤ ( ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) ) )
307	259 297 306	mp2and	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) ≤ ( ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
308	302	rpcnd	⊢ ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℂ )
309		8nn	⊢ 8 ∈ ℕ
310		nnrp	⊢ ( 8 ∈ ℕ → 8 ∈ ℝ+ )
311	309 310	ax-mp	⊢ 8 ∈ ℝ+
312		rpcnne0	⊢ ( 8 ∈ ℝ+ → ( 8 ∈ ℂ ∧ 8 ≠ 0 ) )
313	311 312	mp1i	⊢ ( 𝜑 → ( 8 ∈ ℂ ∧ 8 ≠ 0 ) )
314		div23	⊢ ( ( ( 𝐿 · 𝐸 ) ∈ ℂ ∧ ( log ‘ 𝑍 ) ∈ ℂ ∧ ( 8 ∈ ℂ ∧ 8 ≠ 0 ) ) → ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / 8 ) = ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) )
315	150 308 313 314	syl3anc	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / 8 ) = ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) )
316		divmuldiv	⊢ ( ( ( ( 𝐿 · 𝐸 ) ∈ ℂ ∧ ( log ‘ 𝑍 ) ∈ ℂ ) ∧ ( ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) ) → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) = ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / ( 4 · 2 ) ) )
317	150 308 143 153 316	syl22anc	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) = ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / ( 4 · 2 ) ) )
318		4t2e8	⊢ ( 4 · 2 ) = 8
319	318	oveq2i	⊢ ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / ( 4 · 2 ) ) = ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / 8 )
320	317 319	eqtr2di	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) · ( log ‘ 𝑍 ) ) / 8 ) = ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) )
321	315 320	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) = ( ( ( 𝐿 · 𝐸 ) / 4 ) · ( ( log ‘ 𝑍 ) / 2 ) ) )
322	45	recnd	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℂ )
323	294	recnd	⊢ ( 𝜑 → ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℂ )
324	38	rpcnne0d	⊢ ( 𝜑 → ( ( 𝑍 / 𝑉 ) ∈ ℂ ∧ ( 𝑍 / 𝑉 ) ≠ 0 ) )
325		divass	⊢ ( ( ( ♯ ‘ 𝐼 ) ∈ ℂ ∧ ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℂ ∧ ( ( 𝑍 / 𝑉 ) ∈ ℂ ∧ ( 𝑍 / 𝑉 ) ≠ 0 ) ) → ( ( ( ♯ ‘ 𝐼 ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) / ( 𝑍 / 𝑉 ) ) = ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) )
326		div23	⊢ ( ( ( ♯ ‘ 𝐼 ) ∈ ℂ ∧ ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℂ ∧ ( ( 𝑍 / 𝑉 ) ∈ ℂ ∧ ( 𝑍 / 𝑉 ) ≠ 0 ) ) → ( ( ( ♯ ‘ 𝐼 ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) / ( 𝑍 / 𝑉 ) ) = ( ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
327	325 326	eqtr3d	⊢ ( ( ( ♯ ‘ 𝐼 ) ∈ ℂ ∧ ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℂ ∧ ( ( 𝑍 / 𝑉 ) ∈ ℂ ∧ ( 𝑍 / 𝑉 ) ≠ 0 ) ) → ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) = ( ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
328	322 323 324 327	syl3anc	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) = ( ( ( ♯ ‘ 𝐼 ) / ( 𝑍 / 𝑉 ) ) · ( log ‘ ( 𝑍 / 𝑉 ) ) ) )
329	307 321 328	3brtr4d	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ≤ ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) )
330		rpdivcl	⊢ ( ( ( 𝐿 · 𝐸 ) ∈ ℝ+ ∧ 8 ∈ ℝ+ ) → ( ( 𝐿 · 𝐸 ) / 8 ) ∈ ℝ+ )
331	29 311 330	sylancl	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 8 ) ∈ ℝ+ )
332	331 302	rpmulcld	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ∈ ℝ+ )
333	332	rpred	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ∈ ℝ )
334	294 38	rerpdivcld	⊢ ( 𝜑 → ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ∈ ℝ )
335	45 334	remulcld	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ∈ ℝ )
336	183	simp3d	⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) ∈ ℝ+ )
337	333 335 336	lemul2d	⊢ ( 𝜑 → ( ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ≤ ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ↔ ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ ( ( 𝑈 − 𝐸 ) · ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) ) )
338	329 337	mpbid	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ ( ( 𝑈 − 𝐸 ) · ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) )
339	336	rpcnd	⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) ∈ ℂ )
340	334	recnd	⊢ ( 𝜑 → ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ∈ ℂ )
341	339 322 340	mul12d	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( ♯ ‘ 𝐼 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) = ( ( ♯ ‘ 𝐼 ) · ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) )
342	338 341	breqtrd	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ ( ( ♯ ‘ 𝐼 ) · ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) )