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 syl5bir ( 𝜑 → ( ( ∃ 𝑡 ∈ ℝ+𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑡 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ∧ ∃ 𝑐 ∈ ℝ+𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑧 ) ≤ 𝑐 ) → ∃ 𝑤 ∈ ℝ+𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) ) )
83 40 45 82 mp2and ( 𝜑 → ∃ 𝑤 ∈ ℝ+𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )