Step | Hyp | Ref
| Expression |
1 | | rlimclim.1 |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | rlimclim.2 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | 2 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝐴) → 𝑀 ∈ ℤ) |
4 | | simpr 476 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝐴) → 𝐹 ⇝𝑟 𝐴) |
5 | | rlimclim.3 |
. . . . 5
⊢ (𝜑 → 𝐹:𝑍⟶ℂ) |
6 | | fdm 5964 |
. . . . 5
⊢ (𝐹:𝑍⟶ℂ → dom 𝐹 = 𝑍) |
7 | | eqimss2 3621 |
. . . . 5
⊢ (dom
𝐹 = 𝑍 → 𝑍 ⊆ dom 𝐹) |
8 | 5, 6, 7 | 3syl 18 |
. . . 4
⊢ (𝜑 → 𝑍 ⊆ dom 𝐹) |
9 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝐴) → 𝑍 ⊆ dom 𝐹) |
10 | 1, 3, 4, 9 | rlimclim1 14124 |
. 2
⊢ ((𝜑 ∧ 𝐹 ⇝𝑟 𝐴) → 𝐹 ⇝ 𝐴) |
11 | | climcl 14078 |
. . . 4
⊢ (𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ) |
12 | 11 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ⇝ 𝐴) → 𝐴 ∈ ℂ) |
13 | 2 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) → 𝑀 ∈
ℤ) |
14 | | simpr 476 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ+) |
15 | | eqidd 2611 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
16 | | simplr 788 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) → 𝐹 ⇝ 𝐴) |
17 | 1, 13, 14, 15, 16 | climi2 14090 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) →
∃𝑧 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦) |
18 | | uzssz 11583 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
19 | 1, 18 | eqsstri 3598 |
. . . . . . . . . . . . 13
⊢ 𝑍 ⊆
ℤ |
20 | | simplrl 796 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦)) ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤)) → 𝑧 ∈ 𝑍) |
21 | 19, 20 | sseldi 3566 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦)) ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤)) → 𝑧 ∈ ℤ) |
22 | | simprl 790 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦)) ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤)) → 𝑤 ∈ 𝑍) |
23 | 19, 22 | sseldi 3566 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦)) ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤)) → 𝑤 ∈ ℤ) |
24 | | simprr 792 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦)) ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤)) → 𝑧 ≤ 𝑤) |
25 | | eluz2 11569 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈
(ℤ≥‘𝑧) ↔ (𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ∧ 𝑧 ≤ 𝑤)) |
26 | 21, 23, 24, 25 | syl3anbrc 1239 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦)) ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤)) → 𝑤 ∈ (ℤ≥‘𝑧)) |
27 | | simplrr 797 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦)) ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤)) → ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦) |
28 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑤 → (𝐹‘𝑘) = (𝐹‘𝑤)) |
29 | 28 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑤 → ((𝐹‘𝑘) − 𝐴) = ((𝐹‘𝑤) − 𝐴)) |
30 | 29 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑤 → (abs‘((𝐹‘𝑘) − 𝐴)) = (abs‘((𝐹‘𝑤) − 𝐴))) |
31 | 30 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑤 → ((abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦 ↔ (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦)) |
32 | 31 | rspcv 3278 |
. . . . . . . . . . 11
⊢ (𝑤 ∈
(ℤ≥‘𝑧) → (∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦)) |
33 | 26, 27, 32 | sylc 63 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦)) ∧ (𝑤 ∈ 𝑍 ∧ 𝑧 ≤ 𝑤)) → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦) |
34 | 33 | expr 641 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦)) ∧ 𝑤 ∈ 𝑍) → (𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦)) |
35 | 34 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦)) → ∀𝑤 ∈ 𝑍 (𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦)) |
36 | 35 | expr 641 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦 → ∀𝑤 ∈ 𝑍 (𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) |
37 | 36 | reximdva 3000 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) →
(∃𝑧 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦 → ∃𝑧 ∈ 𝑍 ∀𝑤 ∈ 𝑍 (𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) |
38 | | zssre 11261 |
. . . . . . . 8
⊢ ℤ
⊆ ℝ |
39 | 19, 38 | sstri 3577 |
. . . . . . 7
⊢ 𝑍 ⊆
ℝ |
40 | | ssrexv 3630 |
. . . . . . 7
⊢ (𝑍 ⊆ ℝ →
(∃𝑧 ∈ 𝑍 ∀𝑤 ∈ 𝑍 (𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑍 (𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) |
41 | 39, 40 | ax-mp 5 |
. . . . . 6
⊢
(∃𝑧 ∈
𝑍 ∀𝑤 ∈ 𝑍 (𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑍 (𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦)) |
42 | 37, 41 | syl6 34 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) →
(∃𝑧 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑧)(abs‘((𝐹‘𝑘) − 𝐴)) < 𝑦 → ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑍 (𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦))) |
43 | 17, 42 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑦 ∈ ℝ+) →
∃𝑧 ∈ ℝ
∀𝑤 ∈ 𝑍 (𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦)) |
44 | 43 | ralrimiva 2949 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ⇝ 𝐴) → ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑍 (𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦)) |
45 | 5 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ⇝ 𝐴) → 𝐹:𝑍⟶ℂ) |
46 | 39 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ⇝ 𝐴) → 𝑍 ⊆ ℝ) |
47 | | eqidd 2611 |
. . . 4
⊢ (((𝜑 ∧ 𝐹 ⇝ 𝐴) ∧ 𝑤 ∈ 𝑍) → (𝐹‘𝑤) = (𝐹‘𝑤)) |
48 | 45, 46, 47 | rlim 14074 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ⇝ 𝐴) → (𝐹 ⇝𝑟 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑧 ∈ ℝ
∀𝑤 ∈ 𝑍 (𝑧 ≤ 𝑤 → (abs‘((𝐹‘𝑤) − 𝐴)) < 𝑦)))) |
49 | 12, 44, 48 | mpbir2and 959 |
. 2
⊢ ((𝜑 ∧ 𝐹 ⇝ 𝐴) → 𝐹 ⇝𝑟 𝐴) |
50 | 10, 49 | impbida 873 |
1
⊢ (𝜑 → (𝐹 ⇝𝑟 𝐴 ↔ 𝐹 ⇝ 𝐴)) |