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 ) ) ) ) |