| Step | Hyp | Ref
| Expression |
| 1 | | pntlem1.r |
. . 3
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
| 2 | 1 | pntrmax 27608 |
. 2
⊢
∃𝑑 ∈
ℝ+ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑 |
| 3 | 1 | pntpbnd 27632 |
. 2
⊢
∃𝑏 ∈
ℝ+ ∀𝑓 ∈ (0(,)1)∃𝑔 ∈ ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓) |
| 4 | | reeanv 3229 |
. . 3
⊢
(∃𝑑 ∈
ℝ+ ∃𝑏 ∈ ℝ+ (∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑 ∧ ∀𝑓 ∈ (0(,)1)∃𝑔 ∈ ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓)) ↔ (∃𝑑 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑 ∧ ∃𝑏 ∈ ℝ+ ∀𝑓 ∈ (0(,)1)∃𝑔 ∈ ℝ+
∀𝑚 ∈
((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓))) |
| 5 | | 2rp 13039 |
. . . . . . . . 9
⊢ 2 ∈
ℝ+ |
| 6 | | rpmulcl 13058 |
. . . . . . . . 9
⊢ ((2
∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → (2
· 𝑏) ∈
ℝ+) |
| 7 | 5, 6 | mpan 690 |
. . . . . . . 8
⊢ (𝑏 ∈ ℝ+
→ (2 · 𝑏)
∈ ℝ+) |
| 8 | | 2re 12340 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
| 9 | | 1lt2 12437 |
. . . . . . . . 9
⊢ 1 <
2 |
| 10 | | rplogcl 26646 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ 1 < 2) → (log‘2) ∈
ℝ+) |
| 11 | 8, 9, 10 | mp2an 692 |
. . . . . . . 8
⊢
(log‘2) ∈ ℝ+ |
| 12 | | rpaddcl 13057 |
. . . . . . . 8
⊢ (((2
· 𝑏) ∈
ℝ+ ∧ (log‘2) ∈ ℝ+) → ((2
· 𝑏) +
(log‘2)) ∈ ℝ+) |
| 13 | 7, 11, 12 | sylancl 586 |
. . . . . . 7
⊢ (𝑏 ∈ ℝ+
→ ((2 · 𝑏) +
(log‘2)) ∈ ℝ+) |
| 14 | 13 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑑 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ (∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑 ∧ ∀𝑓 ∈ (0(,)1)∃𝑔 ∈ ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓))) → ((2 · 𝑏) + (log‘2)) ∈
ℝ+) |
| 15 | | id 22 |
. . . . . . . 8
⊢ (𝑑 ∈ ℝ+
→ 𝑑 ∈
ℝ+) |
| 16 | | eqid 2737 |
. . . . . . . 8
⊢ ((1 / 4)
/ (𝑑 + 3)) = ((1 / 4) /
(𝑑 + 3)) |
| 17 | 1, 15, 16 | pntibndlem1 27633 |
. . . . . . 7
⊢ (𝑑 ∈ ℝ+
→ ((1 / 4) / (𝑑 + 3))
∈ (0(,)1)) |
| 18 | 17 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑑 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ (∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑 ∧ ∀𝑓 ∈ (0(,)1)∃𝑔 ∈ ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓))) → ((1 / 4) / (𝑑 + 3)) ∈ (0(,)1)) |
| 19 | | elioore 13417 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 ∈ (0(,)1) → 𝑒 ∈
ℝ) |
| 20 | | eliooord 13446 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 ∈ (0(,)1) → (0 <
𝑒 ∧ 𝑒 < 1)) |
| 21 | 20 | simpld 494 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 ∈ (0(,)1) → 0 <
𝑒) |
| 22 | 19, 21 | elrpd 13074 |
. . . . . . . . . . . . . 14
⊢ (𝑒 ∈ (0(,)1) → 𝑒 ∈
ℝ+) |
| 23 | 22 | rphalfcld 13089 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ (0(,)1) → (𝑒 / 2) ∈
ℝ+) |
| 24 | 23 | rpred 13077 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ (0(,)1) → (𝑒 / 2) ∈
ℝ) |
| 25 | 23 | rpgt0d 13080 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ (0(,)1) → 0 <
(𝑒 / 2)) |
| 26 | | 1red 11262 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ (0(,)1) → 1 ∈
ℝ) |
| 27 | | rphalflt 13064 |
. . . . . . . . . . . . . 14
⊢ (𝑒 ∈ ℝ+
→ (𝑒 / 2) < 𝑒) |
| 28 | 22, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ (0(,)1) → (𝑒 / 2) < 𝑒) |
| 29 | 20 | simprd 495 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ (0(,)1) → 𝑒 < 1) |
| 30 | 24, 19, 26, 28, 29 | lttrd 11422 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ (0(,)1) → (𝑒 / 2) < 1) |
| 31 | | 0xr 11308 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ* |
| 32 | | 1xr 11320 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ* |
| 33 | | elioo2 13428 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ*) → ((𝑒 / 2) ∈ (0(,)1) ↔
((𝑒 / 2) ∈ ℝ
∧ 0 < (𝑒 / 2) ∧
(𝑒 / 2) <
1))) |
| 34 | 31, 32, 33 | mp2an 692 |
. . . . . . . . . . . 12
⊢ ((𝑒 / 2) ∈ (0(,)1) ↔
((𝑒 / 2) ∈ ℝ
∧ 0 < (𝑒 / 2) ∧
(𝑒 / 2) <
1)) |
| 35 | 24, 25, 30, 34 | syl3anbrc 1344 |
. . . . . . . . . . 11
⊢ (𝑒 ∈ (0(,)1) → (𝑒 / 2) ∈
(0(,)1)) |
| 36 | 35 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝑑 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) ∧ 𝑒 ∈ (0(,)1)) → (𝑒 / 2) ∈ (0(,)1)) |
| 37 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑒 / 2) → (𝑏 / 𝑓) = (𝑏 / (𝑒 / 2))) |
| 38 | 37 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑒 / 2) → (exp‘(𝑏 / 𝑓)) = (exp‘(𝑏 / (𝑒 / 2)))) |
| 39 | 38 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑒 / 2) → ((exp‘(𝑏 / 𝑓))[,)+∞) = ((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)) |
| 40 | | breq2 5147 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑒 / 2) → ((abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓 ↔ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2))) |
| 41 | 40 | anbi2d 630 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑒 / 2) → (((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓) ↔ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) |
| 42 | 41 | rexbidv 3179 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑒 / 2) → (∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓) ↔ ∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) |
| 43 | 42 | ralbidv 3178 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑒 / 2) → (∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓) ↔ ∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) |
| 44 | 39, 43 | raleqbidv 3346 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑒 / 2) → (∀𝑚 ∈ ((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓) ↔ ∀𝑚 ∈ ((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) |
| 45 | 44 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑒 / 2) → (∃𝑔 ∈ ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓) ↔ ∃𝑔 ∈ ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) |
| 46 | 45 | rspcv 3618 |
. . . . . . . . . 10
⊢ ((𝑒 / 2) ∈ (0(,)1) →
(∀𝑓 ∈
(0(,)1)∃𝑔 ∈
ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓) → ∃𝑔 ∈ ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) |
| 47 | 36, 46 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑑 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) ∧ 𝑒 ∈ (0(,)1)) → (∀𝑓 ∈ (0(,)1)∃𝑔 ∈ ℝ+
∀𝑚 ∈
((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓) → ∃𝑔 ∈ ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) |
| 48 | | simp-4l 783 |
. . . . . . . . . . 11
⊢
(((((𝑑 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) ∧ 𝑒 ∈ (0(,)1)) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑚 ∈
((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) → 𝑑 ∈ ℝ+) |
| 49 | | simpllr 776 |
. . . . . . . . . . 11
⊢
(((((𝑑 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) ∧ 𝑒 ∈ (0(,)1)) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑚 ∈
((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) → ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) |
| 50 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝑑 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) → 𝑏 ∈ ℝ+) |
| 51 | 50 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((𝑑 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) ∧ 𝑒 ∈ (0(,)1)) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑚 ∈
((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) → 𝑏 ∈ ℝ+) |
| 52 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(exp‘(𝑏 /
(𝑒 / 2))) =
(exp‘(𝑏 / (𝑒 / 2))) |
| 53 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ((2
· 𝑏) +
(log‘2)) = ((2 · 𝑏) + (log‘2)) |
| 54 | | simplr 769 |
. . . . . . . . . . 11
⊢
(((((𝑑 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) ∧ 𝑒 ∈ (0(,)1)) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑚 ∈
((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) → 𝑒 ∈ (0(,)1)) |
| 55 | | simprl 771 |
. . . . . . . . . . 11
⊢
(((((𝑑 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) ∧ 𝑒 ∈ (0(,)1)) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑚 ∈
((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) → 𝑔 ∈ ℝ+) |
| 56 | | simprr 773 |
. . . . . . . . . . 11
⊢
(((((𝑑 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) ∧ 𝑒 ∈ (0(,)1)) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑚 ∈
((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) → ∀𝑚 ∈ ((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2))) |
| 57 | 1, 48, 16, 49, 51, 52, 53, 54, 55, 56 | pntibndlem3 27636 |
. . . . . . . . . 10
⊢
(((((𝑑 ∈
ℝ+ ∧ 𝑏
∈ ℝ+) ∧ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) ∧ 𝑒 ∈ (0(,)1)) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑚 ∈
((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)))) → ∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(((2
· 𝑏) +
(log‘2)) / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒)) |
| 58 | 57 | rexlimdvaa 3156 |
. . . . . . . . 9
⊢ ((((𝑑 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) ∧ 𝑒 ∈ (0(,)1)) → (∃𝑔 ∈ ℝ+
∀𝑚 ∈
((exp‘(𝑏 / (𝑒 / 2)))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ (𝑒 / 2)) → ∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(((2
· 𝑏) +
(log‘2)) / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒))) |
| 59 | 47, 58 | syld 47 |
. . . . . . . 8
⊢ ((((𝑑 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) ∧ 𝑒 ∈ (0(,)1)) → (∀𝑓 ∈ (0(,)1)∃𝑔 ∈ ℝ+
∀𝑚 ∈
((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓) → ∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(((2
· 𝑏) +
(log‘2)) / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒))) |
| 60 | 59 | ralrimdva 3154 |
. . . . . . 7
⊢ (((𝑑 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑) → (∀𝑓 ∈ (0(,)1)∃𝑔 ∈ ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓) → ∀𝑒 ∈ (0(,)1)∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(((2
· 𝑏) +
(log‘2)) / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒))) |
| 61 | 60 | impr 454 |
. . . . . 6
⊢ (((𝑑 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ (∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑 ∧ ∀𝑓 ∈ (0(,)1)∃𝑔 ∈ ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓))) → ∀𝑒 ∈ (0(,)1)∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(((2
· 𝑏) +
(log‘2)) / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒)) |
| 62 | | fvoveq1 7454 |
. . . . . . . . . . 11
⊢ (𝑐 = ((2 · 𝑏) + (log‘2)) →
(exp‘(𝑐 / 𝑒)) = (exp‘(((2 ·
𝑏) + (log‘2)) / 𝑒))) |
| 63 | 62 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑐 = ((2 · 𝑏) + (log‘2)) →
((exp‘(𝑐 / 𝑒))[,)+∞) =
((exp‘(((2 · 𝑏) + (log‘2)) / 𝑒))[,)+∞)) |
| 64 | 63 | raleqdv 3326 |
. . . . . . . . 9
⊢ (𝑐 = ((2 · 𝑏) + (log‘2)) →
(∀𝑘 ∈
((exp‘(𝑐 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒) ↔ ∀𝑘 ∈ ((exp‘(((2 · 𝑏) + (log‘2)) / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒))) |
| 65 | 64 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑐 = ((2 · 𝑏) + (log‘2)) →
(∃𝑥 ∈
ℝ+ ∀𝑘 ∈ ((exp‘(𝑐 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒) ↔ ∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(((2
· 𝑏) +
(log‘2)) / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒))) |
| 66 | 65 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑐 = ((2 · 𝑏) + (log‘2)) →
(∀𝑒 ∈
(0(,)1)∃𝑥 ∈
ℝ+ ∀𝑘 ∈ ((exp‘(𝑐 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒) ↔ ∀𝑒 ∈ (0(,)1)∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(((2
· 𝑏) +
(log‘2)) / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒))) |
| 67 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = ((1 / 4) / (𝑑 + 3)) → (𝑙 · 𝑒) = (((1 / 4) / (𝑑 + 3)) · 𝑒)) |
| 68 | 67 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = ((1 / 4) / (𝑑 + 3)) → (1 + (𝑙 · 𝑒)) = (1 + (((1 / 4) / (𝑑 + 3)) · 𝑒))) |
| 69 | 68 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = ((1 / 4) / (𝑑 + 3)) → ((1 + (𝑙 · 𝑒)) · 𝑧) = ((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧)) |
| 70 | 69 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ (𝑙 = ((1 / 4) / (𝑑 + 3)) → (((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦) ↔ ((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧) < (𝑘 · 𝑦))) |
| 71 | 70 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (𝑙 = ((1 / 4) / (𝑑 + 3)) → ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ↔ (𝑦 < 𝑧 ∧ ((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧) < (𝑘 · 𝑦)))) |
| 72 | 69 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑙 = ((1 / 4) / (𝑑 + 3)) → (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧)) = (𝑧[,]((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧))) |
| 73 | 72 | raleqdv 3326 |
. . . . . . . . . . . 12
⊢ (𝑙 = ((1 / 4) / (𝑑 + 3)) → (∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒 ↔ ∀𝑢 ∈ (𝑧[,]((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒)) |
| 74 | 71, 73 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑙 = ((1 / 4) / (𝑑 + 3)) → (((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒) ↔ ((𝑦 < 𝑧 ∧ ((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒))) |
| 75 | 74 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑙 = ((1 / 4) / (𝑑 + 3)) → (∃𝑧 ∈ ℝ+
((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒) ↔ ∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒))) |
| 76 | 75 | ralbidv 3178 |
. . . . . . . . 9
⊢ (𝑙 = ((1 / 4) / (𝑑 + 3)) → (∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒) ↔ ∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (((1 / 4) / (𝑑 + 3)) · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒))) |
| 77 | 76 | rexralbidv 3223 |
. . . . . . . 8
⊢ (𝑙 = ((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 3178 |
. . . . . . 7
⊢ (𝑙 = ((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 3635 |
. . . . . 6
⊢ ((((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 1373 |
. . . . 5
⊢ (((𝑑 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) ∧ (∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑 ∧ ∀𝑓 ∈ (0(,)1)∃𝑔 ∈ ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓))) → ∃𝑐 ∈ ℝ+ ∃𝑙 ∈ (0(,)1)∀𝑒 ∈ (0(,)1)∃𝑥 ∈ ℝ+
∀𝑘 ∈
((exp‘(𝑐 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒)) |
| 81 | 80 | ex 412 |
. . . 4
⊢ ((𝑑 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → ((∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑 ∧ ∀𝑓 ∈ (0(,)1)∃𝑔 ∈ ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓)) → ∃𝑐 ∈ ℝ+ ∃𝑙 ∈ (0(,)1)∀𝑒 ∈ (0(,)1)∃𝑥 ∈ ℝ+
∀𝑘 ∈
((exp‘(𝑐 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒))) |
| 82 | 81 | rexlimivv 3201 |
. . 3
⊢
(∃𝑑 ∈
ℝ+ ∃𝑏 ∈ ℝ+ (∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑 ∧ ∀𝑓 ∈ (0(,)1)∃𝑔 ∈ ℝ+ ∀𝑚 ∈ ((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓)) → ∃𝑐 ∈ ℝ+ ∃𝑙 ∈ (0(,)1)∀𝑒 ∈ (0(,)1)∃𝑥 ∈ ℝ+
∀𝑘 ∈
((exp‘(𝑐 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒)) |
| 83 | 4, 82 | sylbir 235 |
. 2
⊢
((∃𝑑 ∈
ℝ+ ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑑 ∧ ∃𝑏 ∈ ℝ+ ∀𝑓 ∈ (0(,)1)∃𝑔 ∈ ℝ+
∀𝑚 ∈
((exp‘(𝑏 / 𝑓))[,)+∞)∀𝑣 ∈ (𝑔(,)+∞)∃𝑛 ∈ ℕ ((𝑣 < 𝑛 ∧ 𝑛 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑓)) → ∃𝑐 ∈ ℝ+ ∃𝑙 ∈ (0(,)1)∀𝑒 ∈ (0(,)1)∃𝑥 ∈ ℝ+
∀𝑘 ∈
((exp‘(𝑐 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒)) |
| 84 | 2, 3, 83 | mp2an 692 |
1
⊢
∃𝑐 ∈
ℝ+ ∃𝑙 ∈ (0(,)1)∀𝑒 ∈ (0(,)1)∃𝑥 ∈ ℝ+ ∀𝑘 ∈ ((exp‘(𝑐 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒) |