Theorem pntlemj

Description: Lemma for pnt . The induction step. Using pntibnd , we find an interval in K ^ J ... K ^ ( J + 1 ) which is sufficiently large and has a much smaller value, R ( z ) / z <_ E (instead of our original bound R ( z ) / z <_ U ). (Contributed by Mario Carneiro, 13-Apr-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	pntlemj	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ Σ 𝑛 ∈ 𝑂 ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( 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 7 8 9 10	pntlemc	⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )
26	25	simp3d	⊢ ( 𝜑 → ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
27	26	simp3d	⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) ∈ ℝ+ )
28	1 2 3 4 5 6	pntlemd	⊢ ( 𝜑 → ( 𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ∧ 𝐹 ∈ ℝ+ ) )
29	28	simp1d	⊢ ( 𝜑 → 𝐿 ∈ ℝ+ )
30	25	simp1d	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
31	29 30	rpmulcld	⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℝ+ )
32		8nn	⊢ 8 ∈ ℕ
33		nnrp	⊢ ( 8 ∈ ℕ → 8 ∈ ℝ+ )
34	32 33	ax-mp	⊢ 8 ∈ ℝ+
35		rpdivcl	⊢ ( ( ( 𝐿 · 𝐸 ) ∈ ℝ+ ∧ 8 ∈ ℝ+ ) → ( ( 𝐿 · 𝐸 ) / 8 ) ∈ ℝ+ )
36	31 34 35	sylancl	⊢ ( 𝜑 → ( ( 𝐿 · 𝐸 ) / 8 ) ∈ ℝ+ )
37	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 ‘ 𝑍 ) ) ) ) )
38	37	simp1d	⊢ ( 𝜑 → 𝑍 ∈ ℝ+ )
39	38	rpred	⊢ ( 𝜑 → 𝑍 ∈ ℝ )
40	37	simp2d	⊢ ( 𝜑 → ( 1 < 𝑍 ∧ e ≤ ( √ ‘ 𝑍 ) ∧ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / 𝑌 ) ) )
41	40	simp1d	⊢ ( 𝜑 → 1 < 𝑍 )
42	39 41	rplogcld	⊢ ( 𝜑 → ( log ‘ 𝑍 ) ∈ ℝ+ )
43	36 42	rpmulcld	⊢ ( 𝜑 → ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ∈ ℝ+ )
44	27 43	rpmulcld	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ∈ ℝ+ )
45	44	rpred	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ∈ ℝ )
46		fzfid	⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) ∈ Fin )
47	24 46	eqeltrid	⊢ ( 𝜑 → 𝐼 ∈ Fin )
48		hashcl	⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
49	47 48	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
50	49	nn0red	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℝ )
51	27	rpred	⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) ∈ ℝ )
52	38 21	rpdivcld	⊢ ( 𝜑 → ( 𝑍 / 𝑉 ) ∈ ℝ+ )
53	52	relogcld	⊢ ( 𝜑 → ( log ‘ ( 𝑍 / 𝑉 ) ) ∈ ℝ )
54	53 52	rerpdivcld	⊢ ( 𝜑 → ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ∈ ℝ )
55	51 54	remulcld	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ∈ ℝ )
56	50 55	remulcld	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) · ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) ∈ ℝ )
57		fzfid	⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ) ∈ Fin )
58	20 57	eqeltrid	⊢ ( 𝜑 → 𝑂 ∈ Fin )
59	7	rpred	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
60	59	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → 𝑈 ∈ ℝ )
61	25	simp2d	⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
62		elfzoelz	⊢ ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
63	23 62	syl	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
64	63	peano2zd	⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ℤ )
65	61 64	rpexpcld	⊢ ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∈ ℝ+ )
66	38 65	rpdivcld	⊢ ( 𝜑 → ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ∈ ℝ+ )
67	66	rprege0d	⊢ ( 𝜑 → ( ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) )
68		flge0nn0	⊢ ( ( ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) → ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) ∈ ℕ0 )
69		nn0p1nn	⊢ ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ∈ ℕ )
70	67 68 69	3syl	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ∈ ℕ )
71		elfzuz	⊢ ( 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ) )
72	71 20	eleq2s	⊢ ( 𝑛 ∈ 𝑂 → 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ) )
73		eluznn	⊢ ( ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ∈ ℕ ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ) ) → 𝑛 ∈ ℕ )
74	70 72 73	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → 𝑛 ∈ ℕ )
75	60 74	nndivred	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( 𝑈 / 𝑛 ) ∈ ℝ )
76	38	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → 𝑍 ∈ ℝ+ )
77	74	nnrpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → 𝑛 ∈ ℝ+ )
78	76 77	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( 𝑍 / 𝑛 ) ∈ ℝ+ )
79	1	pntrf	⊢ 𝑅 : ℝ+ ⟶ ℝ
80	79	ffvelcdmi	⊢ ( ( 𝑍 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℝ )
81	78 80	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℝ )
82	81 76	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ∈ ℝ )
83	82	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ∈ ℂ )
84	83	abscld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ∈ ℝ )
85	75 84	resubcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) ∈ ℝ )
86	77	relogcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( log ‘ 𝑛 ) ∈ ℝ )
87	85 86	remulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
88	58 87	fsumrecl	⊢ ( 𝜑 → Σ 𝑛 ∈ 𝑂 ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
89	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24	pntlemr	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ ( ( ♯ ‘ 𝐼 ) · ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) )
90	55	recnd	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ∈ ℂ )
91		fsumconst	⊢ ( ( 𝐼 ∈ Fin ∧ ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ∈ ℂ ) → Σ 𝑛 ∈ 𝐼 ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) = ( ( ♯ ‘ 𝐼 ) · ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) )
92	47 90 91	syl2anc	⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐼 ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) = ( ( ♯ ‘ 𝐼 ) · ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) )
93	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24	pntlemq	⊢ ( 𝜑 → 𝐼 ⊆ 𝑂 )
94	90	ralrimivw	⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝐼 ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ∈ ℂ )
95	58	olcd	⊢ ( 𝜑 → ( 𝑂 ⊆ ( ℤ≥ ‘ 1 ) ∨ 𝑂 ∈ Fin ) )
96		sumss2	⊢ ( ( ( 𝐼 ⊆ 𝑂 ∧ ∀ 𝑛 ∈ 𝐼 ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ∈ ℂ ) ∧ ( 𝑂 ⊆ ( ℤ≥ ‘ 1 ) ∨ 𝑂 ∈ Fin ) ) → Σ 𝑛 ∈ 𝐼 ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) = Σ 𝑛 ∈ 𝑂 if ( 𝑛 ∈ 𝐼 , ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) , 0 ) )
97	93 94 95 96	syl21anc	⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐼 ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) = Σ 𝑛 ∈ 𝑂 if ( 𝑛 ∈ 𝐼 , ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) , 0 ) )
98	92 97	eqtr3d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) · ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) = Σ 𝑛 ∈ 𝑂 if ( 𝑛 ∈ 𝐼 , ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) , 0 ) )
99	55	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ∈ ℝ )
100	99	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ∈ ℝ )
101		0red	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) ∧ ¬ 𝑛 ∈ 𝐼 ) → 0 ∈ ℝ )
102	100 101	ifclda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → if ( 𝑛 ∈ 𝐼 , ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) , 0 ) ∈ ℝ )
103		breq1	⊢ ( ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) = if ( 𝑛 ∈ 𝐼 , ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) , 0 ) → ( ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ↔ if ( 𝑛 ∈ 𝐼 , ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) , 0 ) ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) )
104		breq1	⊢ ( 0 = if ( 𝑛 ∈ 𝐼 , ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) , 0 ) → ( 0 ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ↔ if ( 𝑛 ∈ 𝐼 , ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) , 0 ) ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ) )
105	27	rpregt0d	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) ∈ ℝ ∧ 0 < ( 𝑈 − 𝐸 ) ) )
106	105	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑈 − 𝐸 ) ∈ ℝ ∧ 0 < ( 𝑈 − 𝐸 ) ) )
107	106	simpld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑈 − 𝐸 ) ∈ ℝ )
108		1rp	⊢ 1 ∈ ℝ+
109		rpaddcl	⊢ ( ( 1 ∈ ℝ+ ∧ ( 𝐿 · 𝐸 ) ∈ ℝ+ ) → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
110	108 31 109	sylancr	⊢ ( 𝜑 → ( 1 + ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
111	110 21	rpmulcld	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ∈ ℝ+ )
112	38 111	rpdivcld	⊢ ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ+ )
113	112	rprege0d	⊢ ( 𝜑 → ( ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) )
114		flge0nn0	⊢ ( ( ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℕ0 )
115		nn0p1nn	⊢ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ∈ ℕ )
116	113 114 115	3syl	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ∈ ℕ )
117		elfzuz	⊢ ( 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) )
118	117 24	eleq2s	⊢ ( 𝑛 ∈ 𝐼 → 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) )
119		eluznn	⊢ ( ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ∈ ℕ ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ) ) → 𝑛 ∈ ℕ )
120	116 118 119	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑛 ∈ ℕ )
121	120	nnrpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑛 ∈ ℝ+ )
122	121	relogcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( log ‘ 𝑛 ) ∈ ℝ )
123	122 120	nndivred	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
124	107 123	remulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑈 − 𝐸 ) · ( ( log ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
125	93	sselda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑛 ∈ 𝑂 )
126	125 87	syldan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
127		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑛 ∈ 𝐼 )
128	127 24	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) )
129		elfzle2	⊢ ( 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) → 𝑛 ≤ ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) )
130	128 129	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑛 ≤ ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) )
131	52	rpred	⊢ ( 𝜑 → ( 𝑍 / 𝑉 ) ∈ ℝ )
132	131	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑍 / 𝑉 ) ∈ ℝ )
133	128	elfzelzd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑛 ∈ ℤ )
134		flge	⊢ ( ( ( 𝑍 / 𝑉 ) ∈ ℝ ∧ 𝑛 ∈ ℤ ) → ( 𝑛 ≤ ( 𝑍 / 𝑉 ) ↔ 𝑛 ≤ ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) )
135	132 133 134	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑛 ≤ ( 𝑍 / 𝑉 ) ↔ 𝑛 ≤ ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) )
136	130 135	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑛 ≤ ( 𝑍 / 𝑉 ) )
137	120	nnred	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑛 ∈ ℝ )
138		ere	⊢ e ∈ ℝ
139	138	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → e ∈ ℝ )
140	112	rpred	⊢ ( 𝜑 → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ )
141	140	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ )
142	138	a1i	⊢ ( 𝜑 → e ∈ ℝ )
143	38	rpsqrtcld	⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ∈ ℝ+ )
144	143	rpred	⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ∈ ℝ )
145	40	simp2d	⊢ ( 𝜑 → e ≤ ( √ ‘ 𝑍 ) )
146	111	rpred	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ∈ ℝ )
147	65	rpred	⊢ ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∈ ℝ )
148	22	simpld	⊢ ( 𝜑 → ( ( 𝐾 ↑ 𝐽 ) < 𝑉 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) )
149	148	simprd	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) )
150	61	rpcnd	⊢ ( 𝜑 → 𝐾 ∈ ℂ )
151	61 63	rpexpcld	⊢ ( 𝜑 → ( 𝐾 ↑ 𝐽 ) ∈ ℝ+ )
152	151	rpcnd	⊢ ( 𝜑 → ( 𝐾 ↑ 𝐽 ) ∈ ℂ )
153	150 152	mulcomd	⊢ ( 𝜑 → ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) = ( ( 𝐾 ↑ 𝐽 ) · 𝐾 ) )
154	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pntlemg	⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ( ( log ‘ 𝑍 ) / ( log ‘ 𝐾 ) ) / 4 ) ≤ ( 𝑁 − 𝑀 ) ) )
155	154	simp1d	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
156		elfzouz	⊢ ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) )
157	23 156	syl	⊢ ( 𝜑 → 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) )
158		eluznn	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝐽 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐽 ∈ ℕ )
159	155 157 158	syl2anc	⊢ ( 𝜑 → 𝐽 ∈ ℕ )
160	159	nnnn0d	⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
161	150 160	expp1d	⊢ ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) = ( ( 𝐾 ↑ 𝐽 ) · 𝐾 ) )
162	153 161	eqtr4d	⊢ ( 𝜑 → ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) = ( 𝐾 ↑ ( 𝐽 + 1 ) ) )
163	149 162	breqtrd	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) < ( 𝐾 ↑ ( 𝐽 + 1 ) ) )
164	146 147 163	ltled	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ≤ ( 𝐾 ↑ ( 𝐽 + 1 ) ) )
165		fzofzp1	⊢ ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐽 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
166	23 165	syl	⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
167	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pntlemh	⊢ ( ( 𝜑 ∧ ( 𝐽 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑋 < ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∧ ( 𝐾 ↑ ( 𝐽 + 1 ) ) ≤ ( √ ‘ 𝑍 ) ) )
168	166 167	mpdan	⊢ ( 𝜑 → ( 𝑋 < ( 𝐾 ↑ ( 𝐽 + 1 ) ) ∧ ( 𝐾 ↑ ( 𝐽 + 1 ) ) ≤ ( √ ‘ 𝑍 ) ) )
169	168	simprd	⊢ ( 𝜑 → ( 𝐾 ↑ ( 𝐽 + 1 ) ) ≤ ( √ ‘ 𝑍 ) )
170	146 147 144 164 169	letrd	⊢ ( 𝜑 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ≤ ( √ ‘ 𝑍 ) )
171	146 144 143	lemul2d	⊢ ( 𝜑 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ≤ ( √ ‘ 𝑍 ) ↔ ( ( √ ‘ 𝑍 ) · ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) ) )
172	170 171	mpbid	⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) · ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) )
173	38	rprege0d	⊢ ( 𝜑 → ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) )
174		remsqsqrt	⊢ ( ( 𝑍 ∈ ℝ ∧ 0 ≤ 𝑍 ) → ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) = 𝑍 )
175	173 174	syl	⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) · ( √ ‘ 𝑍 ) ) = 𝑍 )
176	172 175	breqtrd	⊢ ( 𝜑 → ( ( √ ‘ 𝑍 ) · ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ 𝑍 )
177	144 39 111	lemuldivd	⊢ ( 𝜑 → ( ( ( √ ‘ 𝑍 ) · ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ 𝑍 ↔ ( √ ‘ 𝑍 ) ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) )
178	176 177	mpbid	⊢ ( 𝜑 → ( √ ‘ 𝑍 ) ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
179	142 144 140 145 178	letrd	⊢ ( 𝜑 → e ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
180	179	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → e ≤ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
181		reflcl	⊢ ( ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℝ )
182		peano2re	⊢ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ∈ ℝ )
183	140 181 182	3syl	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ∈ ℝ )
184	183	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ∈ ℝ )
185		fllep1	⊢ ( ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∈ ℝ → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) )
186	141 185	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) )
187		elfzle1	⊢ ( 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑉 ) ) ) → ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ≤ 𝑛 )
188	128 187	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) + 1 ) ≤ 𝑛 )
189	141 184 137 186 188	letrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ 𝑛 )
190	139 141 137 180 189	letrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → e ≤ 𝑛 )
191	139 137 132 190 136	letrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → e ≤ ( 𝑍 / 𝑉 ) )
192		logdivle	⊢ ( ( ( 𝑛 ∈ ℝ ∧ e ≤ 𝑛 ) ∧ ( ( 𝑍 / 𝑉 ) ∈ ℝ ∧ e ≤ ( 𝑍 / 𝑉 ) ) ) → ( 𝑛 ≤ ( 𝑍 / 𝑉 ) ↔ ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ≤ ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
193	137 190 132 191 192	syl22anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑛 ≤ ( 𝑍 / 𝑉 ) ↔ ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ≤ ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
194	136 193	mpbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ≤ ( ( log ‘ 𝑛 ) / 𝑛 ) )
195	54	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ∈ ℝ )
196		lemul2	⊢ ( ( ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ∈ ℝ ∧ ( ( log ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ∧ ( ( 𝑈 − 𝐸 ) ∈ ℝ ∧ 0 < ( 𝑈 − 𝐸 ) ) ) → ( ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ≤ ( ( log ‘ 𝑛 ) / 𝑛 ) ↔ ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ≤ ( ( 𝑈 − 𝐸 ) · ( ( log ‘ 𝑛 ) / 𝑛 ) ) ) )
197	195 123 106 196	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ≤ ( ( log ‘ 𝑛 ) / 𝑛 ) ↔ ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ≤ ( ( 𝑈 − 𝐸 ) · ( ( log ‘ 𝑛 ) / 𝑛 ) ) ) )
198	194 197	mpbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ≤ ( ( 𝑈 − 𝐸 ) · ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
199	27	rpcnd	⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) ∈ ℂ )
200	199	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑈 − 𝐸 ) ∈ ℂ )
201	122	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( log ‘ 𝑛 ) ∈ ℂ )
202	121	rpcnne0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
203		div23	⊢ ( ( ( 𝑈 − 𝐸 ) ∈ ℂ ∧ ( log ‘ 𝑛 ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( ( 𝑈 − 𝐸 ) · ( log ‘ 𝑛 ) ) / 𝑛 ) = ( ( ( 𝑈 − 𝐸 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) )
204	200 201 202 203	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( ( 𝑈 − 𝐸 ) · ( log ‘ 𝑛 ) ) / 𝑛 ) = ( ( ( 𝑈 − 𝐸 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) )
205		divass	⊢ ( ( ( 𝑈 − 𝐸 ) ∈ ℂ ∧ ( log ‘ 𝑛 ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( ( 𝑈 − 𝐸 ) · ( log ‘ 𝑛 ) ) / 𝑛 ) = ( ( 𝑈 − 𝐸 ) · ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
206	200 201 202 205	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( ( 𝑈 − 𝐸 ) · ( log ‘ 𝑛 ) ) / 𝑛 ) = ( ( 𝑈 − 𝐸 ) · ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
207	204 206	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( ( 𝑈 − 𝐸 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) = ( ( 𝑈 − 𝐸 ) · ( ( log ‘ 𝑛 ) / 𝑛 ) ) )
208	51	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑈 − 𝐸 ) ∈ ℝ )
209	208 120	nndivred	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑈 − 𝐸 ) / 𝑛 ) ∈ ℝ )
210	125 85	syldan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) ∈ ℝ )
211		log1	⊢ ( log ‘ 1 ) = 0
212	120	nnge1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 1 ≤ 𝑛 )
213		logleb	⊢ ( ( 1 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 1 ≤ 𝑛 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑛 ) ) )
214	108 121 213	sylancr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 1 ≤ 𝑛 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑛 ) ) )
215	212 214	mpbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( log ‘ 1 ) ≤ ( log ‘ 𝑛 ) )
216	211 215	eqbrtrrid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 0 ≤ ( log ‘ 𝑛 ) )
217	7	rpcnd	⊢ ( 𝜑 → 𝑈 ∈ ℂ )
218	217	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑈 ∈ ℂ )
219	30	rpred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
220	219	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝐸 ∈ ℝ )
221	220	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝐸 ∈ ℂ )
222		divsubdir	⊢ ( ( 𝑈 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( 𝑈 − 𝐸 ) / 𝑛 ) = ( ( 𝑈 / 𝑛 ) − ( 𝐸 / 𝑛 ) ) )
223	218 221 202 222	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑈 − 𝐸 ) / 𝑛 ) = ( ( 𝑈 / 𝑛 ) − ( 𝐸 / 𝑛 ) ) )
224	125 84	syldan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ∈ ℝ )
225	220 120	nndivred	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝐸 / 𝑛 ) ∈ ℝ )
226	125 75	syldan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑈 / 𝑛 ) ∈ ℝ )
227	125 81	syldan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℝ )
228	227	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℂ )
229	38	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑍 ∈ ℝ+ )
230	229	rpcnne0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑍 ∈ ℂ ∧ 𝑍 ≠ 0 ) )
231		divdiv2	⊢ ( ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℂ ∧ ( 𝑍 ∈ ℂ ∧ 𝑍 ≠ 0 ) ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / ( 𝑍 / 𝑛 ) ) = ( ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) · 𝑛 ) / 𝑍 ) )
232	228 230 202 231	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / ( 𝑍 / 𝑛 ) ) = ( ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) · 𝑛 ) / 𝑍 ) )
233	121	rpcnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑛 ∈ ℂ )
234		div23	⊢ ( ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ ( 𝑍 ∈ ℂ ∧ 𝑍 ≠ 0 ) ) → ( ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) · 𝑛 ) / 𝑍 ) = ( ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) · 𝑛 ) )
235	228 233 230 234	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) · 𝑛 ) / 𝑍 ) = ( ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) · 𝑛 ) )
236	232 235	eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / ( 𝑍 / 𝑛 ) ) = ( ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) · 𝑛 ) )
237	236	fveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / ( 𝑍 / 𝑛 ) ) ) = ( abs ‘ ( ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) · 𝑛 ) ) )
238	125 83	syldan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ∈ ℂ )
239	238 233	absmuld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( abs ‘ ( ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) · 𝑛 ) ) = ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( abs ‘ 𝑛 ) ) )
240	121	rprege0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) )
241		absid	⊢ ( ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) → ( abs ‘ 𝑛 ) = 𝑛 )
242	240 241	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( abs ‘ 𝑛 ) = 𝑛 )
243	242	oveq2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · ( abs ‘ 𝑛 ) ) = ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · 𝑛 ) )
244	237 239 243	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / ( 𝑍 / 𝑛 ) ) ) = ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · 𝑛 ) )
245		fveq2	⊢ ( 𝑢 = ( 𝑍 / 𝑛 ) → ( 𝑅 ‘ 𝑢 ) = ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) )
246		id	⊢ ( 𝑢 = ( 𝑍 / 𝑛 ) → 𝑢 = ( 𝑍 / 𝑛 ) )
247	245 246	oveq12d	⊢ ( 𝑢 = ( 𝑍 / 𝑛 ) → ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) = ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / ( 𝑍 / 𝑛 ) ) )
248	247	fveq2d	⊢ ( 𝑢 = ( 𝑍 / 𝑛 ) → ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) = ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / ( 𝑍 / 𝑛 ) ) ) )
249	248	breq1d	⊢ ( 𝑢 = ( 𝑍 / 𝑛 ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ↔ ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / ( 𝑍 / 𝑛 ) ) ) ≤ 𝐸 ) )
250	22	simprd	⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 𝑉 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 )
251	250	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ∀ 𝑢 ∈ ( 𝑉 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 )
252	39	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑍 ∈ ℝ )
253	252 120	nndivred	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑍 / 𝑛 ) ∈ ℝ )
254	21	rpregt0d	⊢ ( 𝜑 → ( 𝑉 ∈ ℝ ∧ 0 < 𝑉 ) )
255	254	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑉 ∈ ℝ ∧ 0 < 𝑉 ) )
256		lemuldiv2	⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑍 ∈ ℝ ∧ ( 𝑉 ∈ ℝ ∧ 0 < 𝑉 ) ) → ( ( 𝑉 · 𝑛 ) ≤ 𝑍 ↔ 𝑛 ≤ ( 𝑍 / 𝑉 ) ) )
257	137 252 255 256	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑉 · 𝑛 ) ≤ 𝑍 ↔ 𝑛 ≤ ( 𝑍 / 𝑉 ) ) )
258	136 257	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑉 · 𝑛 ) ≤ 𝑍 )
259	255	simpld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑉 ∈ ℝ )
260	259 252 121	lemuldivd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑉 · 𝑛 ) ≤ 𝑍 ↔ 𝑉 ≤ ( 𝑍 / 𝑛 ) ) )
261	258 260	mpbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑉 ≤ ( 𝑍 / 𝑛 ) )
262	111	rpregt0d	⊢ ( 𝜑 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ∈ ℝ ∧ 0 < ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
263	262	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ∈ ℝ ∧ 0 < ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
264	121	rpregt0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) )
265		lediv23	⊢ ( ( 𝑍 ∈ ℝ ∧ ( ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ∈ ℝ ∧ 0 < ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → ( ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ 𝑛 ↔ ( 𝑍 / 𝑛 ) ≤ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
266	252 263 264 265	syl3anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ≤ 𝑛 ↔ ( 𝑍 / 𝑛 ) ≤ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
267	189 266	mpbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑍 / 𝑛 ) ≤ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) )
268	21	rpred	⊢ ( 𝜑 → 𝑉 ∈ ℝ )
269	268	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝑉 ∈ ℝ )
270	146	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ∈ ℝ )
271		elicc2	⊢ ( ( 𝑉 ∈ ℝ ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ∈ ℝ ) → ( ( 𝑍 / 𝑛 ) ∈ ( 𝑉 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ↔ ( ( 𝑍 / 𝑛 ) ∈ ℝ ∧ 𝑉 ≤ ( 𝑍 / 𝑛 ) ∧ ( 𝑍 / 𝑛 ) ≤ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) )
272	269 270 271	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑍 / 𝑛 ) ∈ ( 𝑉 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ↔ ( ( 𝑍 / 𝑛 ) ∈ ℝ ∧ 𝑉 ≤ ( 𝑍 / 𝑛 ) ∧ ( 𝑍 / 𝑛 ) ≤ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) ) )
273	253 261 267 272	mpbir3and	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑍 / 𝑛 ) ∈ ( 𝑉 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑉 ) ) )
274	249 251 273	rspcdva	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / ( 𝑍 / 𝑛 ) ) ) ≤ 𝐸 )
275	244 274	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · 𝑛 ) ≤ 𝐸 )
276	224 220 121	lemuldivd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) · 𝑛 ) ≤ 𝐸 ↔ ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ≤ ( 𝐸 / 𝑛 ) ) )
277	275 276	mpbid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ≤ ( 𝐸 / 𝑛 ) )
278	224 225 226 277	lesub2dd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑈 / 𝑛 ) − ( 𝐸 / 𝑛 ) ) ≤ ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) )
279	223 278	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑈 − 𝐸 ) / 𝑛 ) ≤ ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) )
280	209 210 122 216 279	lemul1ad	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( ( 𝑈 − 𝐸 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
281	207 280	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑈 − 𝐸 ) · ( ( log ‘ 𝑛 ) / 𝑛 ) ) ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
282	99 124 126 198 281	letrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
283	282	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
284	74	nnred	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → 𝑛 ∈ ℝ )
285	38 151	rpdivcld	⊢ ( 𝜑 → ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ∈ ℝ+ )
286	285	rpred	⊢ ( 𝜑 → ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ∈ ℝ )
287	286	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ∈ ℝ )
288	11	simpld	⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
289	38 288	rpdivcld	⊢ ( 𝜑 → ( 𝑍 / 𝑌 ) ∈ ℝ+ )
290	289	rpred	⊢ ( 𝜑 → ( 𝑍 / 𝑌 ) ∈ ℝ )
291	290	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( 𝑍 / 𝑌 ) ∈ ℝ )
292		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → 𝑛 ∈ 𝑂 )
293	292 20	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ) )
294		elfzle2	⊢ ( 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ ( 𝐽 + 1 ) ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ) → 𝑛 ≤ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) )
295	293 294	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → 𝑛 ≤ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) )
296	74	nnzd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → 𝑛 ∈ ℤ )
297		flge	⊢ ( ( ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ∈ ℝ ∧ 𝑛 ∈ ℤ ) → ( 𝑛 ≤ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ↔ 𝑛 ≤ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ) )
298	287 296 297	syl2anc	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( 𝑛 ≤ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ↔ 𝑛 ≤ ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) ) )
299	295 298	mpbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → 𝑛 ≤ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) )
300	288	rpred	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
301	12	simpld	⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
302	301	rpred	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
303	151	rpred	⊢ ( 𝜑 → ( 𝐾 ↑ 𝐽 ) ∈ ℝ )
304	12	simprd	⊢ ( 𝜑 → 𝑌 < 𝑋 )
305	300 302 304	ltled	⊢ ( 𝜑 → 𝑌 ≤ 𝑋 )
306		elfzofz	⊢ ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐽 ∈ ( 𝑀 ... 𝑁 ) )
307	23 306	syl	⊢ ( 𝜑 → 𝐽 ∈ ( 𝑀 ... 𝑁 ) )
308	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pntlemh	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑋 < ( 𝐾 ↑ 𝐽 ) ∧ ( 𝐾 ↑ 𝐽 ) ≤ ( √ ‘ 𝑍 ) ) )
309	307 308	mpdan	⊢ ( 𝜑 → ( 𝑋 < ( 𝐾 ↑ 𝐽 ) ∧ ( 𝐾 ↑ 𝐽 ) ≤ ( √ ‘ 𝑍 ) ) )
310	309	simpld	⊢ ( 𝜑 → 𝑋 < ( 𝐾 ↑ 𝐽 ) )
311	302 303 310	ltled	⊢ ( 𝜑 → 𝑋 ≤ ( 𝐾 ↑ 𝐽 ) )
312	300 302 303 305 311	letrd	⊢ ( 𝜑 → 𝑌 ≤ ( 𝐾 ↑ 𝐽 ) )
313	288 151 38	lediv2d	⊢ ( 𝜑 → ( 𝑌 ≤ ( 𝐾 ↑ 𝐽 ) ↔ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ≤ ( 𝑍 / 𝑌 ) ) )
314	312 313	mpbid	⊢ ( 𝜑 → ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ≤ ( 𝑍 / 𝑌 ) )
315	314	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ≤ ( 𝑍 / 𝑌 ) )
316	284 287 291 299 315	letrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → 𝑛 ≤ ( 𝑍 / 𝑌 ) )
317	74 316	jca	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ ( 𝑍 / 𝑌 ) ) )
318	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	pntlemn	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ ( 𝑍 / 𝑌 ) ) ) → 0 ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
319	317 318	syldan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → 0 ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
320	319	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) ∧ ¬ 𝑛 ∈ 𝐼 ) → 0 ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
321	103 104 283 320	ifbothda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑂 ) → if ( 𝑛 ∈ 𝐼 , ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) , 0 ) ≤ ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
322	58 102 87 321	fsumle	⊢ ( 𝜑 → Σ 𝑛 ∈ 𝑂 if ( 𝑛 ∈ 𝐼 , ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) , 0 ) ≤ Σ 𝑛 ∈ 𝑂 ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
323	98 322	eqbrtrd	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) · ( ( 𝑈 − 𝐸 ) · ( ( log ‘ ( 𝑍 / 𝑉 ) ) / ( 𝑍 / 𝑉 ) ) ) ) ≤ Σ 𝑛 ∈ 𝑂 ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
324	45 56 88 89 323	letrd	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ Σ 𝑛 ∈ 𝑂 ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )