Step | Hyp | Ref
| Expression |
1 | | idlimc.x |
. 2
⊢ (𝜑 → 𝑋 ∈ ℂ) |
2 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈
ℝ+) |
3 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
4 | | idlimc.f |
. . . . . . . . . . . . . . 15
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑥) |
5 | 4 | fvmpt2 6200 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝑥) |
6 | 3, 3, 5 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝑥) |
7 | 6 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) − 𝑋) = (𝑥 − 𝑋)) |
8 | 7 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘((𝐹‘𝑥) − 𝑋)) = (abs‘(𝑥 − 𝑋))) |
9 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) = (abs‘(𝑥 − 𝑋))) |
10 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘(𝑥 − 𝑋)) < 𝑤) |
11 | 9, 10 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) |
12 | 11 | adantrl 748 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ (𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤)) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) |
13 | 12 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤)) |
14 | 13 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑥 ∈ 𝐴) → ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤)) |
15 | 14 | ralrimiva 2949 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∀𝑥 ∈ 𝐴 ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤)) |
16 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑧𝑥 |
17 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑧𝑋 |
18 | 16, 17 | nfne 2882 |
. . . . . . . 8
⊢
Ⅎ𝑧 𝑥 ≠ 𝑋 |
19 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑧(abs‘(𝑥 − 𝑋)) < 𝑤 |
20 | 18, 19 | nfan 1816 |
. . . . . . 7
⊢
Ⅎ𝑧(𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) |
21 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑧(abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤 |
22 | 20, 21 | nfim 1813 |
. . . . . 6
⊢
Ⅎ𝑧((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) |
23 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) |
24 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑥abs |
25 | | nfmpt1 4675 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝑥) |
26 | 4, 25 | nfcxfr 2749 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐹 |
27 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑧 |
28 | 26, 27 | nffv 6110 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝐹‘𝑧) |
29 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑥
− |
30 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑋 |
31 | 28, 29, 30 | nfov 6575 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝐹‘𝑧) − 𝑋) |
32 | 24, 31 | nffv 6110 |
. . . . . . . 8
⊢
Ⅎ𝑥(abs‘((𝐹‘𝑧) − 𝑋)) |
33 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑥
< |
34 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑤 |
35 | 32, 33, 34 | nfbr 4629 |
. . . . . . 7
⊢
Ⅎ𝑥(abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤 |
36 | 23, 35 | nfim 1813 |
. . . . . 6
⊢
Ⅎ𝑥((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤) |
37 | | neeq1 2844 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 ≠ 𝑋 ↔ 𝑧 ≠ 𝑋)) |
38 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥 − 𝑋) = (𝑧 − 𝑋)) |
39 | 38 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (abs‘(𝑥 − 𝑋)) = (abs‘(𝑧 − 𝑋))) |
40 | 39 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → ((abs‘(𝑥 − 𝑋)) < 𝑤 ↔ (abs‘(𝑧 − 𝑋)) < 𝑤)) |
41 | 37, 40 | anbi12d 743 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) ↔ (𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤))) |
42 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
43 | 42 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) − 𝑋) = ((𝐹‘𝑧) − 𝑋)) |
44 | 43 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (abs‘((𝐹‘𝑥) − 𝑋)) = (abs‘((𝐹‘𝑧) − 𝑋))) |
45 | 44 | breq1d 4593 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤 ↔ (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) |
46 | 41, 45 | imbi12d 333 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) ↔ ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤))) |
47 | 22, 36, 46 | cbvral 3143 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ((𝑥 ≠ 𝑋 ∧ (abs‘(𝑥 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑥) − 𝑋)) < 𝑤) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) |
48 | 15, 47 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) |
49 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → ((abs‘(𝑧 − 𝑋)) < 𝑦 ↔ (abs‘(𝑧 − 𝑋)) < 𝑤)) |
50 | 49 | anbi2d 736 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) ↔ (𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤))) |
51 | 50 | imbi1d 330 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤) ↔ ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤))) |
52 | 51 | ralbidv 2969 |
. . . . 5
⊢ (𝑦 = 𝑤 → (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤))) |
53 | 52 | rspcev 3282 |
. . . 4
⊢ ((𝑤 ∈ ℝ+
∧ ∀𝑧 ∈
𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) |
54 | 2, 48, 53 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) |
55 | 54 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑤 ∈ ℝ+ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)) |
56 | | idlimc.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
57 | 56 | sselda 3568 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ) |
58 | 57, 4 | fmptd 6292 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
59 | 58, 56, 1 | ellimc3 23449 |
. 2
⊢ (𝜑 → (𝑋 ∈ (𝐹 limℂ 𝑋) ↔ (𝑋 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝑋 ∧ (abs‘(𝑧 − 𝑋)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝑋)) < 𝑤)))) |
60 | 1, 55, 59 | mpbir2and 959 |
1
⊢ (𝜑 → 𝑋 ∈ (𝐹 limℂ 𝑋)) |