| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pntlem1.r |
⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) ) |
| 2 |
1
|
pntrmax |
⊢ ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 |
| 3 |
1
|
pntpbnd |
⊢ ∃ 𝑏 ∈ ℝ+ ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) |
| 4 |
|
reeanv |
⊢ ( ∃ 𝑑 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ∧ ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ) ↔ ( ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ∧ ∃ 𝑏 ∈ ℝ+ ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ) ) |
| 5 |
|
2rp |
⊢ 2 ∈ ℝ+ |
| 6 |
|
rpmulcl |
⊢ ( ( 2 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → ( 2 · 𝑏 ) ∈ ℝ+ ) |
| 7 |
5 6
|
mpan |
⊢ ( 𝑏 ∈ ℝ+ → ( 2 · 𝑏 ) ∈ ℝ+ ) |
| 8 |
|
2re |
⊢ 2 ∈ ℝ |
| 9 |
|
1lt2 |
⊢ 1 < 2 |
| 10 |
|
rplogcl |
⊢ ( ( 2 ∈ ℝ ∧ 1 < 2 ) → ( log ‘ 2 ) ∈ ℝ+ ) |
| 11 |
8 9 10
|
mp2an |
⊢ ( log ‘ 2 ) ∈ ℝ+ |
| 12 |
|
rpaddcl |
⊢ ( ( ( 2 · 𝑏 ) ∈ ℝ+ ∧ ( log ‘ 2 ) ∈ ℝ+ ) → ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) ∈ ℝ+ ) |
| 13 |
7 11 12
|
sylancl |
⊢ ( 𝑏 ∈ ℝ+ → ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) ∈ ℝ+ ) |
| 14 |
13
|
ad2antlr |
⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ∧ ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ) ) → ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) ∈ ℝ+ ) |
| 15 |
|
id |
⊢ ( 𝑑 ∈ ℝ+ → 𝑑 ∈ ℝ+ ) |
| 16 |
|
eqid |
⊢ ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) = ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) |
| 17 |
1 15 16
|
pntibndlem1 |
⊢ ( 𝑑 ∈ ℝ+ → ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) ∈ ( 0 (,) 1 ) ) |
| 18 |
17
|
ad2antrr |
⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ∧ ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ) ) → ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) ∈ ( 0 (,) 1 ) ) |
| 19 |
|
elioore |
⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → 𝑒 ∈ ℝ ) |
| 20 |
|
eliooord |
⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → ( 0 < 𝑒 ∧ 𝑒 < 1 ) ) |
| 21 |
20
|
simpld |
⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → 0 < 𝑒 ) |
| 22 |
19 21
|
elrpd |
⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → 𝑒 ∈ ℝ+ ) |
| 23 |
22
|
rphalfcld |
⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → ( 𝑒 / 2 ) ∈ ℝ+ ) |
| 24 |
23
|
rpred |
⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → ( 𝑒 / 2 ) ∈ ℝ ) |
| 25 |
23
|
rpgt0d |
⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → 0 < ( 𝑒 / 2 ) ) |
| 26 |
|
1red |
⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → 1 ∈ ℝ ) |
| 27 |
|
rphalflt |
⊢ ( 𝑒 ∈ ℝ+ → ( 𝑒 / 2 ) < 𝑒 ) |
| 28 |
22 27
|
syl |
⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → ( 𝑒 / 2 ) < 𝑒 ) |
| 29 |
20
|
simprd |
⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → 𝑒 < 1 ) |
| 30 |
24 19 26 28 29
|
lttrd |
⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → ( 𝑒 / 2 ) < 1 ) |
| 31 |
|
0xr |
⊢ 0 ∈ ℝ* |
| 32 |
|
1xr |
⊢ 1 ∈ ℝ* |
| 33 |
|
elioo2 |
⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( 𝑒 / 2 ) ∈ ( 0 (,) 1 ) ↔ ( ( 𝑒 / 2 ) ∈ ℝ ∧ 0 < ( 𝑒 / 2 ) ∧ ( 𝑒 / 2 ) < 1 ) ) ) |
| 34 |
31 32 33
|
mp2an |
⊢ ( ( 𝑒 / 2 ) ∈ ( 0 (,) 1 ) ↔ ( ( 𝑒 / 2 ) ∈ ℝ ∧ 0 < ( 𝑒 / 2 ) ∧ ( 𝑒 / 2 ) < 1 ) ) |
| 35 |
24 25 30 34
|
syl3anbrc |
⊢ ( 𝑒 ∈ ( 0 (,) 1 ) → ( 𝑒 / 2 ) ∈ ( 0 (,) 1 ) ) |
| 36 |
35
|
adantl |
⊢ ( ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) → ( 𝑒 / 2 ) ∈ ( 0 (,) 1 ) ) |
| 37 |
|
oveq2 |
⊢ ( 𝑓 = ( 𝑒 / 2 ) → ( 𝑏 / 𝑓 ) = ( 𝑏 / ( 𝑒 / 2 ) ) ) |
| 38 |
37
|
fveq2d |
⊢ ( 𝑓 = ( 𝑒 / 2 ) → ( exp ‘ ( 𝑏 / 𝑓 ) ) = ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) ) |
| 39 |
38
|
oveq1d |
⊢ ( 𝑓 = ( 𝑒 / 2 ) → ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) = ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ) |
| 40 |
|
breq2 |
⊢ ( 𝑓 = ( 𝑒 / 2 ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ↔ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) |
| 41 |
40
|
anbi2d |
⊢ ( 𝑓 = ( 𝑒 / 2 ) → ( ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ↔ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) |
| 42 |
41
|
rexbidv |
⊢ ( 𝑓 = ( 𝑒 / 2 ) → ( ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) |
| 43 |
42
|
ralbidv |
⊢ ( 𝑓 = ( 𝑒 / 2 ) → ( ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ↔ ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) |
| 44 |
39 43
|
raleqbidv |
⊢ ( 𝑓 = ( 𝑒 / 2 ) → ( ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ↔ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) |
| 45 |
44
|
rexbidv |
⊢ ( 𝑓 = ( 𝑒 / 2 ) → ( ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ↔ ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) |
| 46 |
45
|
rspcv |
⊢ ( ( 𝑒 / 2 ) ∈ ( 0 (,) 1 ) → ( ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) → ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) |
| 47 |
36 46
|
syl |
⊢ ( ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) → ( ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) → ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) |
| 48 |
|
simp-4l |
⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑔 ∈ ℝ+ ∧ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) → 𝑑 ∈ ℝ+ ) |
| 49 |
|
simpllr |
⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑔 ∈ ℝ+ ∧ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) → ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) |
| 50 |
|
simplr |
⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) → 𝑏 ∈ ℝ+ ) |
| 51 |
50
|
ad2antrr |
⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑔 ∈ ℝ+ ∧ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) → 𝑏 ∈ ℝ+ ) |
| 52 |
|
eqid |
⊢ ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) = ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) |
| 53 |
|
eqid |
⊢ ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) = ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) |
| 54 |
|
simplr |
⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑔 ∈ ℝ+ ∧ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) → 𝑒 ∈ ( 0 (,) 1 ) ) |
| 55 |
|
simprl |
⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑔 ∈ ℝ+ ∧ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) → 𝑔 ∈ ℝ+ ) |
| 56 |
|
simprr |
⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑔 ∈ ℝ+ ∧ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) → ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) |
| 57 |
1 48 16 49 51 52 53 54 55 56
|
pntibndlem3 |
⊢ ( ( ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑔 ∈ ℝ+ ∧ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) |
| 58 |
57
|
rexlimdvaa |
⊢ ( ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) → ( ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / ( 𝑒 / 2 ) ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ ( 𝑒 / 2 ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) |
| 59 |
47 58
|
syld |
⊢ ( ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) ∧ 𝑒 ∈ ( 0 (,) 1 ) ) → ( ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) |
| 60 |
59
|
ralrimdva |
⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ) → ( ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) → ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) |
| 61 |
60
|
impr |
⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ∧ ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ) ) → ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) |
| 62 |
|
fvoveq1 |
⊢ ( 𝑐 = ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) → ( exp ‘ ( 𝑐 / 𝑒 ) ) = ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) ) |
| 63 |
62
|
oveq1d |
⊢ ( 𝑐 = ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) → ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) = ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ) |
| 64 |
63
|
raleqdv |
⊢ ( 𝑐 = ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) → ( ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∀ 𝑘 ∈ ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) |
| 65 |
64
|
rexbidv |
⊢ ( 𝑐 = ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) → ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) |
| 66 |
65
|
ralbidv |
⊢ ( 𝑐 = ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) → ( ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) |
| 67 |
|
oveq1 |
⊢ ( 𝑙 = ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) → ( 𝑙 · 𝑒 ) = ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) |
| 68 |
67
|
oveq2d |
⊢ ( 𝑙 = ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) → ( 1 + ( 𝑙 · 𝑒 ) ) = ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) ) |
| 69 |
68
|
oveq1d |
⊢ ( 𝑙 = ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) → ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) = ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) |
| 70 |
69
|
breq1d |
⊢ ( 𝑙 = ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) → ( ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ↔ ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ) |
| 71 |
70
|
anbi2d |
⊢ ( 𝑙 = ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) → ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ↔ ( 𝑦 < 𝑧 ∧ ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ) ) |
| 72 |
69
|
oveq2d |
⊢ ( 𝑙 = ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) → ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) = ( 𝑧 [,] ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) ) |
| 73 |
72
|
raleqdv |
⊢ ( 𝑙 = ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) → ( ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ↔ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) |
| 74 |
71 73
|
anbi12d |
⊢ ( 𝑙 = ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) → ( ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) |
| 75 |
74
|
rexbidv |
⊢ ( 𝑙 = ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) → ( ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) |
| 76 |
75
|
ralbidv |
⊢ ( 𝑙 = ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) → ( ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) |
| 77 |
76
|
rexralbidv |
⊢ ( 𝑙 = ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) → ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) |
| 78 |
77
|
ralbidv |
⊢ ( 𝑙 = ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) → ( ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ↔ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) |
| 79 |
66 78
|
rspc2ev |
⊢ ( ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) ∈ ℝ+ ∧ ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) ∈ ( 0 (,) 1 ) ∧ ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( ( ( 2 · 𝑏 ) + ( log ‘ 2 ) ) / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( ( ( 1 / 4 ) / ( 𝑑 + 3 ) ) · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) → ∃ 𝑐 ∈ ℝ+ ∃ 𝑙 ∈ ( 0 (,) 1 ) ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) |
| 80 |
14 18 61 79
|
syl3anc |
⊢ ( ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ∧ ( ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ∧ ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ) ) → ∃ 𝑐 ∈ ℝ+ ∃ 𝑙 ∈ ( 0 (,) 1 ) ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) |
| 81 |
80
|
ex |
⊢ ( ( 𝑑 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → ( ( ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ∧ ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ) → ∃ 𝑐 ∈ ℝ+ ∃ 𝑙 ∈ ( 0 (,) 1 ) ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) ) |
| 82 |
81
|
rexlimivv |
⊢ ( ∃ 𝑑 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ∧ ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ) → ∃ 𝑐 ∈ ℝ+ ∃ 𝑙 ∈ ( 0 (,) 1 ) ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) |
| 83 |
4 82
|
sylbir |
⊢ ( ( ∃ 𝑑 ∈ ℝ+ ∀ 𝑥 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑥 ) / 𝑥 ) ) ≤ 𝑑 ∧ ∃ 𝑏 ∈ ℝ+ ∀ 𝑓 ∈ ( 0 (,) 1 ) ∃ 𝑔 ∈ ℝ+ ∀ 𝑚 ∈ ( ( exp ‘ ( 𝑏 / 𝑓 ) ) [,) +∞ ) ∀ 𝑣 ∈ ( 𝑔 (,) +∞ ) ∃ 𝑛 ∈ ℕ ( ( 𝑣 < 𝑛 ∧ 𝑛 ≤ ( 𝑚 · 𝑣 ) ) ∧ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / 𝑛 ) ) ≤ 𝑓 ) ) → ∃ 𝑐 ∈ ℝ+ ∃ 𝑙 ∈ ( 0 (,) 1 ) ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) ) |
| 84 |
2 3 83
|
mp2an |
⊢ ∃ 𝑐 ∈ ℝ+ ∃ 𝑙 ∈ ( 0 (,) 1 ) ∀ 𝑒 ∈ ( 0 (,) 1 ) ∃ 𝑥 ∈ ℝ+ ∀ 𝑘 ∈ ( ( exp ‘ ( 𝑐 / 𝑒 ) ) [,) +∞ ) ∀ 𝑦 ∈ ( 𝑥 (,) +∞ ) ∃ 𝑧 ∈ ℝ+ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝑙 · 𝑒 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝑒 ) |