Metamath Proof Explorer

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 ffvelrni ⊢ ( ( 𝑍 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) ∈ ℝ )
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 ‘ 𝑛 ) ) )