Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . . . 7
⊢ (𝐹‘𝑤) ∈ V |
2 | 1 | rgenw 2908 |
. . . . . 6
⊢
∀𝑤 ∈ dom
𝐹(𝐹‘𝑤) ∈ V |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∀𝑤 ∈ dom 𝐹(𝐹‘𝑤) ∈ V) |
4 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ+) |
5 | | rlimclim1.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ⇝𝑟 𝐴) |
6 | | rlimf 14080 |
. . . . . . . . 9
⊢ (𝐹 ⇝𝑟
𝐴 → 𝐹:dom 𝐹⟶ℂ) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐹:dom 𝐹⟶ℂ) |
9 | 8 | feqmptd 6159 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐹 = (𝑤 ∈ dom 𝐹 ↦ (𝐹‘𝑤))) |
10 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝐹 ⇝𝑟
𝐴) |
11 | 9, 10 | eqbrtrrd 4607 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑤 ∈ dom 𝐹 ↦ (𝐹‘𝑤)) ⇝𝑟 𝐴) |
12 | 3, 4, 11 | rlimi 14092 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑧 ∈ ℝ
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦)) |
13 | | rlimclim1.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
14 | 13 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) → 𝑀 ∈ ℤ) |
15 | | flcl 12458 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ →
(⌊‘𝑧) ∈
ℤ) |
16 | 15 | peano2zd 11361 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℝ →
((⌊‘𝑧) + 1)
∈ ℤ) |
17 | 16 | ad2antrl 760 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) → ((⌊‘𝑧) + 1) ∈ ℤ) |
18 | 17, 14 | ifcld 4081 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) → if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀) ∈ ℤ) |
19 | 14 | zred 11358 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) → 𝑀 ∈ ℝ) |
20 | 17 | zred 11358 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) → ((⌊‘𝑧) + 1) ∈ ℝ) |
21 | | max1 11890 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘𝑧) + 1)
∈ ℝ) → 𝑀
≤ if(𝑀 ≤
((⌊‘𝑧) + 1),
((⌊‘𝑧) + 1),
𝑀)) |
22 | 19, 20, 21 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀)) |
23 | | eluz2 11569 |
. . . . . . 7
⊢ (if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀) ∈ ℤ ∧ 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) |
24 | 14, 18, 22, 23 | syl3anbrc 1239 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) → if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀) ∈ (ℤ≥‘𝑀)) |
25 | | rlimclim1.1 |
. . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) |
26 | 24, 25 | syl6eleqr 2699 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) → if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀) ∈ 𝑍) |
27 | | rlimclim1.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ⊆ dom 𝐹) |
28 | 27 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → 𝑍 ⊆ dom 𝐹) |
29 | 25 | uztrn2 11581 |
. . . . . . . . 9
⊢
((if(𝑀 ≤
((⌊‘𝑧) + 1),
((⌊‘𝑧) + 1),
𝑀) ∈ 𝑍 ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → 𝑘 ∈ 𝑍) |
30 | 26, 29 | sylan 487 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → 𝑘 ∈ 𝑍) |
31 | 28, 30 | sseldd 3569 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → 𝑘 ∈ dom 𝐹) |
32 | | simplrr 797 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → ∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦)) |
33 | | simplrl 796 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → 𝑧 ∈ ℝ) |
34 | 16 | zred 11358 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ →
((⌊‘𝑧) + 1)
∈ ℝ) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → ((⌊‘𝑧) + 1) ∈
ℝ) |
36 | 19 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → 𝑀 ∈ ℝ) |
37 | 35, 36 | ifcld 4081 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀) ∈ ℝ) |
38 | | eluzelre 11574 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀)) → 𝑘 ∈ ℝ) |
39 | 38 | adantl 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → 𝑘 ∈ ℝ) |
40 | | fllep1 12464 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ → 𝑧 ≤ ((⌊‘𝑧) + 1)) |
41 | 33, 40 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → 𝑧 ≤ ((⌊‘𝑧) + 1)) |
42 | | max2 11892 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘𝑧) + 1)
∈ ℝ) → ((⌊‘𝑧) + 1) ≤ if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀)) |
43 | 36, 35, 42 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → ((⌊‘𝑧) + 1) ≤ if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀)) |
44 | 33, 35, 37, 41, 43 | letrd 10073 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → 𝑧 ≤ if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀)) |
45 | | eluzle 11576 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀)) → if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀) ≤ 𝑘) |
46 | 45 | adantl 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀) ≤ 𝑘) |
47 | 33, 37, 39, 44, 46 | letrd 10073 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → 𝑧 ≤ 𝑘) |
48 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑤 = 𝑘 → (𝑧 ≤ 𝑤 ↔ 𝑧 ≤ 𝑘)) |
49 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑘 → (𝐹‘𝑤) = (𝐹‘𝑘)) |
50 | 49 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑘 → ((𝐹‘𝑤) − 𝐴) = ((𝐹‘𝑘) − 𝐴)) |
51 | 50 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑘 → (abs‘((𝐹‘𝑤) − 𝐴)) = (abs‘((𝐹‘𝑘) − 𝐴))) |
52 | 51 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑤 = 𝑘 → ((abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦 ↔ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦)) |
53 | 48, 52 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑤 = 𝑘 → ((𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦) ↔ (𝑧 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦))) |
54 | 53 | rspcv 3278 |
. . . . . . 7
⊢ (𝑘 ∈ dom 𝐹 → (∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦) → (𝑧 ≤ 𝑘 → (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦))) |
55 | 31, 32, 47, 54 | syl3c 64 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) ∧ 𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) → (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦) |
56 | 55 | ralrimiva 2949 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) → ∀𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦) |
57 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑗 = if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀) → (ℤ≥‘𝑗) =
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))) |
58 | 57 | raleqdv 3121 |
. . . . . 6
⊢ (𝑗 = if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀) → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦 ↔ ∀𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦)) |
59 | 58 | rspcev 3282 |
. . . . 5
⊢
((if(𝑀 ≤
((⌊‘𝑧) + 1),
((⌊‘𝑧) + 1),
𝑀) ∈ 𝑍 ∧ ∀𝑘 ∈
(ℤ≥‘if(𝑀 ≤ ((⌊‘𝑧) + 1), ((⌊‘𝑧) + 1), 𝑀))(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦) |
60 | 26, 56, 59 | syl2anc 691 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ ℝ ∧
∀𝑤 ∈ dom 𝐹(𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦) |
61 | 12, 60 | rexlimddv 3017 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦) |
62 | 61 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦) |
63 | | rlimpm 14079 |
. . . 4
⊢ (𝐹 ⇝𝑟
𝐴 → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
64 | 5, 63 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
65 | | eqidd 2611 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
66 | | rlimcl 14082 |
. . . 4
⊢ (𝐹 ⇝𝑟
𝐴 → 𝐴 ∈ ℂ) |
67 | 5, 66 | syl 17 |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℂ) |
68 | 27 | sselda 3568 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ dom 𝐹) |
69 | 7 | ffvelrnda 6267 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ dom 𝐹) → (𝐹‘𝑘) ∈ ℂ) |
70 | 68, 69 | syldan 486 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
71 | 25, 13, 64, 65, 67, 70 | clim2c 14084 |
. 2
⊢ (𝜑 → (𝐹 ⇝ 𝐴 ↔ ∀𝑦 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦)) |
72 | 62, 71 | mpbird 246 |
1
⊢ (𝜑 → 𝐹 ⇝ 𝐴) |