Step |
Hyp |
Ref |
Expression |
1 |
|
rlim.1 |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ ) |
2 |
|
rlim.2 |
⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) |
3 |
|
rlim.4 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = 𝐵 ) |
4 |
|
rlimrel |
⊢ Rel ⇝𝑟 |
5 |
4
|
brrelex2i |
⊢ ( 𝐹 ⇝𝑟 𝐶 → 𝐶 ∈ V ) |
6 |
5
|
a1i |
⊢ ( 𝜑 → ( 𝐹 ⇝𝑟 𝐶 → 𝐶 ∈ V ) ) |
7 |
|
elex |
⊢ ( 𝐶 ∈ ℂ → 𝐶 ∈ V ) |
8 |
7
|
ad2antrl |
⊢ ( ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) → 𝐶 ∈ V ) |
9 |
8
|
a1i |
⊢ ( 𝜑 → ( ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) → 𝐶 ∈ V ) ) |
10 |
|
cnex |
⊢ ℂ ∈ V |
11 |
|
reex |
⊢ ℝ ∈ V |
12 |
|
elpm2r |
⊢ ( ( ( ℂ ∈ V ∧ ℝ ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) ) |
13 |
10 11 12
|
mpanl12 |
⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) ) |
14 |
1 2 13
|
syl2anc |
⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm ℝ ) ) |
15 |
|
eleq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ ( ℂ ↑pm ℝ ) ↔ 𝐹 ∈ ( ℂ ↑pm ℝ ) ) ) |
16 |
|
eleq1 |
⊢ ( 𝑤 = 𝐶 → ( 𝑤 ∈ ℂ ↔ 𝐶 ∈ ℂ ) ) |
17 |
15 16
|
bi2anan9 |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ( 𝑓 ∈ ( ℂ ↑pm ℝ ) ∧ 𝑤 ∈ ℂ ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ 𝐶 ∈ ℂ ) ) ) |
18 |
|
simpl |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → 𝑓 = 𝐹 ) |
19 |
18
|
dmeqd |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → dom 𝑓 = dom 𝐹 ) |
20 |
|
fveq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) ) |
21 |
|
oveq12 |
⊢ ( ( ( 𝑓 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 = 𝐶 ) → ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) = ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) |
22 |
20 21
|
sylan |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) = ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) |
23 |
22
|
fveq2d |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) ) |
24 |
23
|
breq1d |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) |
25 |
24
|
imbi2d |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ) ↔ ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) |
26 |
19 25
|
raleqbidv |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ∀ 𝑧 ∈ dom 𝑓 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) |
27 |
26
|
rexbidv |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝑓 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) |
28 |
27
|
ralbidv |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝑓 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) |
29 |
17 28
|
anbi12d |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝐶 ) → ( ( ( 𝑓 ∈ ( ℂ ↑pm ℝ ) ∧ 𝑤 ∈ ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝑓 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ) ) ↔ ( ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ 𝐶 ∈ ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) ) |
30 |
|
df-rlim |
⊢ ⇝𝑟 = { 〈 𝑓 , 𝑤 〉 ∣ ( ( 𝑓 ∈ ( ℂ ↑pm ℝ ) ∧ 𝑤 ∈ ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝑓 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑧 ) − 𝑤 ) ) < 𝑥 ) ) } |
31 |
29 30
|
brabga |
⊢ ( ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ 𝐶 ∈ V ) → ( 𝐹 ⇝𝑟 𝐶 ↔ ( ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ 𝐶 ∈ ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) ) |
32 |
|
anass |
⊢ ( ( ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ 𝐶 ∈ ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) ) |
33 |
31 32
|
bitrdi |
⊢ ( ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ 𝐶 ∈ V ) → ( 𝐹 ⇝𝑟 𝐶 ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) ) ) |
34 |
33
|
ex |
⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) → ( 𝐶 ∈ V → ( 𝐹 ⇝𝑟 𝐶 ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) ) ) ) |
35 |
14 34
|
syl |
⊢ ( 𝜑 → ( 𝐶 ∈ V → ( 𝐹 ⇝𝑟 𝐶 ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) ) ) ) |
36 |
6 9 35
|
pm5.21ndd |
⊢ ( 𝜑 → ( 𝐹 ⇝𝑟 𝐶 ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) ) ) |
37 |
14
|
biantrurd |
⊢ ( 𝜑 → ( ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) ) ) |
38 |
1
|
fdmd |
⊢ ( 𝜑 → dom 𝐹 = 𝐴 ) |
39 |
38
|
raleqdv |
⊢ ( 𝜑 → ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ) |
40 |
3
|
fvoveq1d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) = ( abs ‘ ( 𝐵 − 𝐶 ) ) ) |
41 |
40
|
breq1d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ↔ ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) |
42 |
41
|
imbi2d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
43 |
42
|
ralbidva |
⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
44 |
39 43
|
bitrd |
⊢ ( 𝜑 → ( ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
45 |
44
|
rexbidv |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
46 |
45
|
ralbidv |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) |
47 |
46
|
anbi2d |
⊢ ( 𝜑 → ( ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ dom 𝐹 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − 𝐶 ) ) < 𝑥 ) ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) ) |
48 |
36 37 47
|
3bitr2d |
⊢ ( 𝜑 → ( 𝐹 ⇝𝑟 𝐶 ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( 𝐵 − 𝐶 ) ) < 𝑥 ) ) ) ) |