Metamath Proof Explorer

Theorem pntlemp

Description: Lemma for pnt . Wrapping up more quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016)

Ref Expression
Hypotheses pntlem3.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
pntlem3.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
pntlem3.A ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
pntlemp.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
pntlemp.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
pntlemp.d ⊢ 𝐷 = ( 𝐴 + 1 )
pntlemp.f ⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
pntlemp.K ⊢ ( 𝜑 → ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
pntlemp.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
pntlemp.u2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
pntlemp.e ⊢ 𝐸 = ( 𝑈 / 𝐷 )
pntlemp.k ⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
pntlemp.y ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
pntlemp.U ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
Assertion pntlemp ( 𝜑 → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )

Proof

Step Hyp Ref Expression
1 pntlem3.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2 pntlem3.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3 pntlem3.A ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝐴 )
4 pntlemp.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
5 pntlemp.l ⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
6 pntlemp.d ⊢ 𝐷 = ( 𝐴 + 1 )
7 pntlemp.f ⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
8 pntlemp.K ⊢ ( 𝜑 → ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) )
9 pntlemp.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
10 pntlemp.u2 ⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
11 pntlemp.e ⊢ 𝐸 = ( 𝑈 / 𝐷 )
12 pntlemp.k ⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
13 pntlemp.y ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
14 pntlemp.U ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
15 oveq2 ⊢ ( 𝑒 = 𝐸 → ( 𝐵 / 𝑒 ) = ( 𝐵 / 𝐸 ) )
16 15 fveq2d ⊢ ( 𝑒 = 𝐸 → ( exp ‘ ( 𝐵 / 𝑒 ) ) = ( exp ‘ ( 𝐵 / 𝐸 ) ) )
17 16 12 eqtr4di ⊢ ( 𝑒 = 𝐸 → ( exp ‘ ( 𝐵 / 𝑒 ) ) = 𝐾 )
18 17 oveq1d ⊢ ( 𝑒 = 𝐸 → ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) = ( 𝐾 [,) +∞ ) )
19 oveq2 ⊢ ( 𝑒 = 𝐸 → ( 𝐿 · 𝑒 ) = ( 𝐿 · 𝐸 ) )
20 19 oveq2d ⊢ ( 𝑒 = 𝐸 → ( 1 + ( 𝐿 · 𝑒 ) ) = ( 1 + ( 𝐿 · 𝐸 ) ) )
21 20 oveq1d ⊢ ( 𝑒 = 𝐸 → ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) = ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) )
22 21 breq1d ⊢ ( 𝑒 = 𝐸 → ( ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ↔ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) )
23 22 anbi2d ⊢ ( 𝑒 = 𝐸 → ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ↔ ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ) )
24 21 oveq2d ⊢ ( 𝑒 = 𝐸 → ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) = ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) )
25 breq2 ⊢ ( 𝑒 = 𝐸 → ( ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
26 24 25 raleqbidv ⊢ ( 𝑒 = 𝐸 → ( ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ↔ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
27 23 26 anbi12d ⊢ ( 𝑒 = 𝐸 → ( ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
28 27 rexbidv ⊢ ( 𝑒 = 𝐸 → ( ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
29 28 ralbidv ⊢ ( 𝑒 = 𝐸 → ( ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
30 18 29 raleqbidv ⊢ ( 𝑒 = 𝐸 → ( ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
31 30 rexbidv ⊢ ( 𝑒 = 𝐸 → ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
32 oveq1 ⊢ ( 𝑥 = 𝑡 → ( 𝑥 (,) +∞ ) = ( 𝑡 (,) +∞ ) )
33 32 raleqdv ⊢ ( 𝑥 = 𝑡 → ( ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
34 33 ralbidv ⊢ ( 𝑥 = 𝑡 → ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
35 34 cbvrexvw ⊢ ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ∃ 𝑡 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
36 31 35 bitrdi ⊢ ( 𝑒 = 𝐸 → ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝐵 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∃ 𝑡 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
37 1 2 4 5 6 7 9 10 11 12 pntlemc ⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )
38 37 simp3d ⊢ ( 𝜑 → ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
39 38 simp1d ⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
40 36 8 39 rspcdva ⊢ ( 𝜑 → ∃ 𝑡 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
41 13 simpld ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
42 41 rpred ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
43 13 simprd ⊢ ( 𝜑 → 1 ≤ 𝑌 )
44 1 pntrlog2bnd ⊢ ( ( 𝑌 ∈ ℝ ∧ 1 ≤ 𝑌 ) → ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 )
45 42 43 44 syl2anc ⊢ ( 𝜑 → ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 )
46 reeanv ⊢ ( ∃ 𝑡 ∈ ℝ+ ∃ 𝑐 ∈ ℝ+ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ↔ ( ∃ 𝑡 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) )
47 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → 𝐴 ∈ ℝ+ )
48 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → 𝐵 ∈ ℝ+ )
49 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → 𝐿 ∈ ( 0 (,) 1 ) )
50 9 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → 𝑈 ∈ ℝ+ )
51 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → 𝑈 ≤ 𝐴 )
52 13 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ( 𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌 ) )
53 simpl ⊢ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) → 𝑡 ∈ ℝ+ )
54 rpaddcl ⊢ ( ( 𝑌 ∈ ℝ+ ∧ 𝑡 ∈ ℝ+ ) → ( 𝑌 + 𝑡 ) ∈ ℝ+ )
55 41 53 54 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → ( 𝑌 + 𝑡 ) ∈ ℝ+ )
56 ltaddrp ⊢ ( ( 𝑌 ∈ ℝ ∧ 𝑡 ∈ ℝ+ ) → 𝑌 < ( 𝑌 + 𝑡 ) )
57 42 53 56 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → 𝑌 < ( 𝑌 + 𝑡 ) )
58 55 57 jca ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → ( ( 𝑌 + 𝑡 ) ∈ ℝ+ ∧ 𝑌 < ( 𝑌 + 𝑡 ) ) )
59 58 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ( ( 𝑌 + 𝑡 ) ∈ ℝ+ ∧ 𝑌 < ( 𝑌 + 𝑡 ) ) )
60 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → 𝑐 ∈ ℝ+ )
61 eqid ⊢ ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( ( 𝑌 + 𝑡 ) · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝑐 ) ) ) ) ) = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( ( 𝑌 + 𝑡 ) · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝑐 ) ) ) ) )
62 14 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
63 rpxr ⊢ ( 𝑡 ∈ ℝ+ → 𝑡 ∈ ℝ* )
64 63 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → 𝑡 ∈ ℝ* )
65 rpre ⊢ ( 𝑡 ∈ ℝ+ → 𝑡 ∈ ℝ )
66 65 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → 𝑡 ∈ ℝ )
67 55 rpred ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → ( 𝑌 + 𝑡 ) ∈ ℝ )
68 41 adantr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → 𝑌 ∈ ℝ+ )
69 66 68 ltaddrp2d ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → 𝑡 < ( 𝑌 + 𝑡 ) )
70 66 67 69 ltled ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → 𝑡 ≤ ( 𝑌 + 𝑡 ) )
71 iooss1 ⊢ ( ( 𝑡 ∈ ℝ* ∧ 𝑡 ≤ ( 𝑌 + 𝑡 ) ) → ( ( 𝑌 + 𝑡 ) (,) +∞ ) ⊆ ( 𝑡 (,) +∞ ) )
72 64 70 71 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → ( ( 𝑌 + 𝑡 ) (,) +∞ ) ⊆ ( 𝑡 (,) +∞ ) )
73 72 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ( ( 𝑌 + 𝑡 ) (,) +∞ ) ⊆ ( 𝑡 (,) +∞ ) )
74 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
75 ssralv ⊢ ( ( ( 𝑌 + 𝑡 ) (,) +∞ ) ⊆ ( 𝑡 (,) +∞ ) → ( ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) → ∀ 𝑦 ∈ ( ( 𝑌 + 𝑡 ) (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
76 75 ralimdv ⊢ ( ( ( 𝑌 + 𝑡 ) (,) +∞ ) ⊆ ( 𝑡 (,) +∞ ) → ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) → ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( ( 𝑌 + 𝑡 ) (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
77 73 74 76 sylc ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( ( 𝑌 + 𝑡 ) (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
78 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 )
79 1 47 48 49 6 7 50 51 11 12 52 59 60 61 62 77 78 pntleme ⊢ ( ( 𝜑 ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ∧ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )
80 79 expr ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑐 ∈ ℝ+ ) ) → ( ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) ) )
81 80 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ℝ+ ∃ 𝑐 ∈ ℝ+ ( ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) ) )
82 46 81 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑡 ∈ ℝ+ ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∃ 𝑐 ∈ ℝ+ ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) ) )
83 40 45 82 mp2and ⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )