Metamath Proof Explorer

Theorem pntlemi

Description: Lemma for pnt . Eliminate some assumptions from pntlemj . (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 ) ... ( ⌊ ‘ ( 𝑍 / ( 𝐾 ↑ 𝐽 ) ) ) )
Assertion pntlemi ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 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 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑦 < 𝑧 ↔ 𝑦 < 𝑥 ) )
22 oveq2 ⊢ ( 𝑧 = 𝑥 → ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) = ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) )
23 22 breq1d ⊢ ( 𝑧 = 𝑥 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ↔ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · 𝑦 ) ) )
24 21 23 anbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ↔ ( 𝑦 < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · 𝑦 ) ) ) )
25 id ⊢ ( 𝑧 = 𝑥 → 𝑧 = 𝑥 )
26 25 22 oveq12d ⊢ ( 𝑧 = 𝑥 → ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) = ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) )
27 26 raleqdv ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ↔ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
28 24 27 anbi12d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ( ( 𝑦 < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
29 28 cbvrexvw ⊢ ( ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ∃ 𝑥 ∈ ℝ+ ( ( 𝑦 < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
30 breq1 ⊢ ( 𝑦 = ( 𝐾 ↑ 𝐽 ) → ( 𝑦 < 𝑥 ↔ ( 𝐾 ↑ 𝐽 ) < 𝑥 ) )
31 oveq2 ⊢ ( 𝑦 = ( 𝐾 ↑ 𝐽 ) → ( 𝐾 · 𝑦 ) = ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) )
32 31 breq2d ⊢ ( 𝑦 = ( 𝐾 ↑ 𝐽 ) → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · 𝑦 ) ↔ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) )
33 30 32 anbi12d ⊢ ( 𝑦 = ( 𝐾 ↑ 𝐽 ) → ( ( 𝑦 < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · 𝑦 ) ) ↔ ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ) )
34 33 anbi1d ⊢ ( 𝑦 = ( 𝐾 ↑ 𝐽 ) → ( ( ( 𝑦 < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
35 34 rexbidv ⊢ ( 𝑦 = ( 𝐾 ↑ 𝐽 ) → ( ∃ 𝑥 ∈ ℝ+ ( ( 𝑦 < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ∃ 𝑥 ∈ ℝ+ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
36 29 35 syl5bb ⊢ ( 𝑦 = ( 𝐾 ↑ 𝐽 ) → ( ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ∃ 𝑥 ∈ ℝ+ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
37 19 adantr ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
38 1 2 3 4 5 6 7 8 9 10 pntlemc ⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )
39 38 simp2d ⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
40 elfzoelz ⊢ ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
41 rpexpcl ⊢ ( ( 𝐾 ∈ ℝ+ ∧ 𝐽 ∈ ℤ ) → ( 𝐾 ↑ 𝐽 ) ∈ ℝ+ )
42 39 40 41 syl2an ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐾 ↑ 𝐽 ) ∈ ℝ+ )
43 42 rpred ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐾 ↑ 𝐽 ) ∈ ℝ )
44 elfzofz ⊢ ( 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐽 ∈ ( 𝑀 ... 𝑁 ) )
45 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemh ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑋 < ( 𝐾 ↑ 𝐽 ) ∧ ( 𝐾 ↑ 𝐽 ) ≤ ( √ ‘ 𝑍 ) ) )
46 44 45 sylan2 ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑋 < ( 𝐾 ↑ 𝐽 ) ∧ ( 𝐾 ↑ 𝐽 ) ≤ ( √ ‘ 𝑍 ) ) )
47 46 simpld ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 < ( 𝐾 ↑ 𝐽 ) )
48 12 simpld ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 ∈ ℝ+ )
50 rpxr ⊢ ( 𝑋 ∈ ℝ+ → 𝑋 ∈ ℝ* )
51 elioopnf ⊢ ( 𝑋 ∈ ℝ* → ( ( 𝐾 ↑ 𝐽 ) ∈ ( 𝑋 (,) +∞ ) ↔ ( ( 𝐾 ↑ 𝐽 ) ∈ ℝ ∧ 𝑋 < ( 𝐾 ↑ 𝐽 ) ) ) )
52 49 50 51 3syl ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐾 ↑ 𝐽 ) ∈ ( 𝑋 (,) +∞ ) ↔ ( ( 𝐾 ↑ 𝐽 ) ∈ ℝ ∧ 𝑋 < ( 𝐾 ↑ 𝐽 ) ) ) )
53 43 47 52 mpbir2and ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐾 ↑ 𝐽 ) ∈ ( 𝑋 (,) +∞ ) )
54 36 37 53 rspcdva ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∃ 𝑥 ∈ ℝ+ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
55 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → 𝐴 ∈ ℝ+ )
56 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → 𝐵 ∈ ℝ+ )
57 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → 𝐿 ∈ ( 0 (,) 1 ) )
58 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → 𝑈 ∈ ℝ+ )
59 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → 𝑈 ≤ 𝐴 )
60 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
61 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → ( 𝑋 ∈ ℝ+ ∧ 𝑌 < 𝑋 ) )
62 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → 𝐶 ∈ ℝ+ )
63 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → 𝑍 ∈ ( 𝑊 [,) +∞ ) )
64 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
65 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
66 simprl ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → 𝑥 ∈ ℝ+ )
67 simprr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
68 simplr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) )
69 eqid ⊢ ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑥 ) ) ) = ( ( ( ⌊ ‘ ( 𝑍 / ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ) + 1 ) ... ( ⌊ ‘ ( 𝑍 / 𝑥 ) ) )
70 1 55 56 57 5 6 58 59 9 10 60 61 62 14 63 16 17 64 65 20 66 67 68 69 pntlemj ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( 𝑥 ∈ ℝ+ ∧ ( ( ( 𝐾 ↑ 𝐽 ) < 𝑥 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) < ( 𝐾 · ( 𝐾 ↑ 𝐽 ) ) ) ∧ ∀ 𝑢 ∈ ( 𝑥 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) ) → ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ Σ 𝑛 ∈ 𝑂 ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )
71 54 70 rexlimddv ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑈 − 𝐸 ) · ( ( ( 𝐿 · 𝐸 ) / 8 ) · ( log ‘ 𝑍 ) ) ) ≤ Σ 𝑛 ∈ 𝑂 ( ( ( 𝑈 / 𝑛 ) − ( abs ‘ ( ( 𝑅 ‘ ( 𝑍 / 𝑛 ) ) / 𝑍 ) ) ) · ( log ‘ 𝑛 ) ) )