Step | Hyp | Ref
| Expression |
1 | | idlimc.x |
. 2
⊢ (𝜑 → 𝑋 ∈ ℂ) |
2 | | simpr 471 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ+) |
3 | | simpr 471 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
4 | | idlimc.f |
. . . . . . . . . . . . . 14
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑥) |
5 | 4 | fvmpt2 6433 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝑥) |
6 | 3, 3, 5 | syl2anc 573 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝑥) |
7 | 6 | fvoveq1d 6815 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘((𝐹‘𝑥) − 𝑋)) = (abs‘(𝑥 − 𝑋))) |
8 | 7 | adantr 466 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) = (abs‘(𝑥 − 𝑋))) |
9 | | simpr 471 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘(𝑥 − 𝑋)) < 𝑤) |
10 | 8, 9 | eqbrtrd 4808 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) |
11 | 10 | adantrl 695 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤)) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) |
12 | 11 | ex 397 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤)) |
13 | 12 | adantlr 694 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐴) → ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤)) |
14 | 13 | ralrimiva 3115 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∀𝑥 ∈ 𝐴 ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤)) |
15 | | nfcv 2913 |
. . . . . . . . 9
⊢
Ⅎ𝑧𝑥 |
16 | | nfcv 2913 |
. . . . . . . . 9
⊢
Ⅎ𝑧𝑋 |
17 | 15, 16 | nfne 3043 |
. . . . . . . 8
⊢
Ⅎ𝑧 𝑥 ≠ 𝑋 |
18 | | nfv 1995 |
. . . . . . . 8
⊢
Ⅎ𝑧(abs‘(𝑥 − 𝑋)) < 𝑤 |
19 | 17, 18 | nfan 1980 |
. . . . . . 7
⊢
Ⅎ𝑧(𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) |
20 | | nfv 1995 |
. . . . . . 7
⊢
Ⅎ𝑧(abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤 |
21 | 19, 20 | nfim 1977 |
. . . . . 6
⊢
Ⅎ𝑧((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) |
22 | | nfv 1995 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) |
23 | | nfcv 2913 |
. . . . . . . . 9
⊢
Ⅎ𝑥abs |
24 | | nfmpt1 4881 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝑥) |
25 | 4, 24 | nfcxfr 2911 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐹 |
26 | | nfcv 2913 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑧 |
27 | 25, 26 | nffv 6339 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝐹‘𝑧) |
28 | | nfcv 2913 |
. . . . . . . . . 10
⊢
Ⅎ𝑥
− |
29 | | nfcv 2913 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑋 |
30 | 27, 28, 29 | nfov 6821 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝐹‘𝑧) − 𝑋) |
31 | 23, 30 | nffv 6339 |
. . . . . . . 8
⊢
Ⅎ𝑥(abs‘((𝐹‘𝑧) − 𝑋)) |
32 | | nfcv 2913 |
. . . . . . . 8
⊢
Ⅎ𝑥
< |
33 | | nfcv 2913 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑤 |
34 | 31, 32, 33 | nfbr 4833 |
. . . . . . 7
⊢
Ⅎ𝑥(abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤 |
35 | 22, 34 | nfim 1977 |
. . . . . 6
⊢
Ⅎ𝑥((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤) |
36 | | neeq1 3005 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 ≠ 𝑋 ↔ 𝑧 ≠ 𝑋)) |
37 | | fvoveq1 6816 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (abs‘(𝑥 − 𝑋)) = (abs‘(𝑧 − 𝑋))) |
38 | 37 | breq1d 4796 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → ((abs‘(𝑥 − 𝑋)) < 𝑤 ↔ (abs‘(𝑧 − 𝑋)) < 𝑤)) |
39 | 36, 38 | anbi12d 616 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) ↔ (𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤))) |
40 | | fveq2 6332 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
41 | 40 | fvoveq1d 6815 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (abs‘((𝐹‘𝑥) − 𝑋)) = (abs‘((𝐹‘𝑧) − 𝑋))) |
42 | 41 | breq1d 4796 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤 ↔ (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) |
43 | 39, 42 | imbi12d 333 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) ↔ ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤))) |
44 | 21, 35, 43 | cbvral 3316 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) |
45 | 14, 44 | sylib 208 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) |
46 | | breq2 4790 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → ((abs‘(𝑧 − 𝑋)) < 𝑦 ↔ (abs‘(𝑧 − 𝑋)) < 𝑤)) |
47 | 46 | anbi2d 614 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) ↔ (𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤))) |
48 | 47 | imbi1d 330 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤) ↔ ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤))) |
49 | 48 | ralbidv 3135 |
. . . . 5
⊢ (𝑦 = 𝑤 → (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤))) |
50 | 49 | rspcev 3460 |
. . . 4
⊢ ((𝑤 ∈ ℝ+
∧ ∀𝑧 ∈
𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) |
51 | 2, 45, 50 | syl2anc 573 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) |
52 | 51 | ralrimiva 3115 |
. 2
⊢ (𝜑 → ∀𝑤 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) |
53 | | idlimc.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
54 | 53 | sselda 3752 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ) |
55 | 54, 4 | fmptd 6527 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
56 | 55, 53, 1 | ellimc3 23863 |
. 2
⊢ (𝜑 → (𝑋 ∈ (𝐹 limℂ 𝑋) ↔ (𝑋 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)))) |
57 | 1, 52, 56 | mpbir2and 692 |
1
⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝑋)) |