Step |
Hyp |
Ref |
Expression |
1 |
|
idlimc.a |
⊢ ( 𝜑 → 𝐴 ⊆ ℂ ) |
2 |
|
idlimc.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) |
3 |
|
idlimc.x |
⊢ ( 𝜑 → 𝑋 ∈ ℂ ) |
4 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℝ+ ) |
5 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) |
6 |
2
|
fvmpt2 |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) |
7 |
5 5 6
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) |
8 |
7
|
fvoveq1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) = ( abs ‘ ( 𝑥 − 𝑋 ) ) ) |
9 |
8
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) = ( abs ‘ ( 𝑥 − 𝑋 ) ) ) |
10 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) |
11 |
9 10
|
eqbrtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 ) |
12 |
11
|
adantrl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 ) |
13 |
12
|
ex |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 ) ) |
14 |
13
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 ) ) |
15 |
14
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 ) ) |
16 |
|
nfcv |
⊢ Ⅎ 𝑧 𝑥 |
17 |
|
nfcv |
⊢ Ⅎ 𝑧 𝑋 |
18 |
16 17
|
nfne |
⊢ Ⅎ 𝑧 𝑥 ≠ 𝑋 |
19 |
|
nfv |
⊢ Ⅎ 𝑧 ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 |
20 |
18 19
|
nfan |
⊢ Ⅎ 𝑧 ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) |
21 |
|
nfv |
⊢ Ⅎ 𝑧 ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 |
22 |
20 21
|
nfim |
⊢ Ⅎ 𝑧 ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 ) |
23 |
|
nfv |
⊢ Ⅎ 𝑥 ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) |
24 |
|
nfcv |
⊢ Ⅎ 𝑥 abs |
25 |
|
nfmpt1 |
⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝑥 ) |
26 |
2 25
|
nfcxfr |
⊢ Ⅎ 𝑥 𝐹 |
27 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑧 |
28 |
26 27
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 ) |
29 |
|
nfcv |
⊢ Ⅎ 𝑥 − |
30 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑋 |
31 |
28 29 30
|
nfov |
⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) |
32 |
24 31
|
nffv |
⊢ Ⅎ 𝑥 ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) |
33 |
|
nfcv |
⊢ Ⅎ 𝑥 < |
34 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑤 |
35 |
32 33 34
|
nfbr |
⊢ Ⅎ 𝑥 ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 |
36 |
23 35
|
nfim |
⊢ Ⅎ 𝑥 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) |
37 |
|
neeq1 |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≠ 𝑋 ↔ 𝑧 ≠ 𝑋 ) ) |
38 |
|
fvoveq1 |
⊢ ( 𝑥 = 𝑧 → ( abs ‘ ( 𝑥 − 𝑋 ) ) = ( abs ‘ ( 𝑧 − 𝑋 ) ) ) |
39 |
38
|
breq1d |
⊢ ( 𝑥 = 𝑧 → ( ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ↔ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) ) |
40 |
37 39
|
anbi12d |
⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) ↔ ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) ) ) |
41 |
40
|
imbrov2fvoveq |
⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 ) ↔ ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) ) ) |
42 |
22 36 41
|
cbvralw |
⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝑥 ≠ 𝑋 ∧ ( abs ‘ ( 𝑥 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − 𝑋 ) ) < 𝑤 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) ) |
43 |
15 42
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) ) |
44 |
|
brimralrspcev |
⊢ ( ( 𝑤 ∈ ℝ+ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) ) |
45 |
4 43 44
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) ) |
46 |
45
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑤 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) ) |
47 |
1
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℂ ) |
48 |
47 2
|
fmptd |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ ) |
49 |
48 1 3
|
ellimc3 |
⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 limℂ 𝑋 ) ↔ ( 𝑋 ∈ ℂ ∧ ∀ 𝑤 ∈ ℝ+ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ≠ 𝑋 ∧ ( abs ‘ ( 𝑧 − 𝑋 ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝑋 ) ) < 𝑤 ) ) ) ) |
50 |
3 46 49
|
mpbir2and |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 limℂ 𝑋 ) ) |