Step | Hyp | Ref
| Expression |
1 | | limccl 25039 |
. . . 4
⊢ (𝐹 limℂ 𝐷) ⊆
ℂ |
2 | | neglimc.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐷)) |
3 | 1, 2 | sselid 3919 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℂ) |
4 | 3 | negcld 11319 |
. 2
⊢ (𝜑 → -𝐶 ∈ ℂ) |
5 | | neglimc.b |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
6 | | neglimc.f |
. . . . . . . . 9
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
7 | 5, 6 | fmptd 6988 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
8 | 6, 5, 2 | limcmptdm 43176 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
9 | | limcrcl 25038 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (𝐹 limℂ 𝐷) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ)) |
10 | 2, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ)) |
11 | 10 | simp3d 1143 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ℂ) |
12 | 7, 8, 11 | ellimc3 25043 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐷) ↔ (𝐶 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦)))) |
13 | 2, 12 | mpbid 231 |
. . . . . 6
⊢ (𝜑 → (𝐶 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦))) |
14 | 13 | simprd 496 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑤 ∈ ℝ+
∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦)) |
15 | 14 | r19.21bi 3134 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦)) |
16 | | simplll 772 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑤 ∈ ℝ+)
∧ 𝑣 ∈ 𝐴) → 𝜑) |
17 | 16 | 3ad2ant1 1132 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑤 ∈
ℝ+) ∧ 𝑣 ∈ 𝐴) ∧ ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) ∧ (𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤)) → 𝜑) |
18 | | simp1r 1197 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑤 ∈
ℝ+) ∧ 𝑣 ∈ 𝐴) ∧ ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) ∧ (𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤)) → 𝑣 ∈ 𝐴) |
19 | | simp3 1137 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑤 ∈
ℝ+) ∧ 𝑣 ∈ 𝐴) ∧ ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) ∧ (𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤)) → (𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤)) |
20 | | simp2 1136 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑤 ∈
ℝ+) ∧ 𝑣 ∈ 𝐴) ∧ ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) ∧ (𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤)) → ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦)) |
21 | 19, 20 | mpd 15 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑤 ∈
ℝ+) ∧ 𝑣 ∈ 𝐴) ∧ ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) ∧ (𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤)) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) |
22 | | nfv 1917 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝜑 ∧ 𝑣 ∈ 𝐴) |
23 | | neglimc.g |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ -𝐵) |
24 | | nfmpt1 5182 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ -𝐵) |
25 | 23, 24 | nfcxfr 2905 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥𝐺 |
26 | | nfcv 2907 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥𝑣 |
27 | 25, 26 | nffv 6784 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(𝐺‘𝑣) |
28 | | nfmpt1 5182 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
29 | 6, 28 | nfcxfr 2905 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝐹 |
30 | 29, 26 | nffv 6784 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥(𝐹‘𝑣) |
31 | 30 | nfneg 11217 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥-(𝐹‘𝑣) |
32 | 27, 31 | nfeq 2920 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝐺‘𝑣) = -(𝐹‘𝑣) |
33 | 22, 32 | nfim 1899 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) = -(𝐹‘𝑣)) |
34 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑣 → (𝑥 ∈ 𝐴 ↔ 𝑣 ∈ 𝐴)) |
35 | 34 | anbi2d 629 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑣 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑣 ∈ 𝐴))) |
36 | | fveq2 6774 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑣 → (𝐺‘𝑥) = (𝐺‘𝑣)) |
37 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣)) |
38 | 37 | negeqd 11215 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑣 → -(𝐹‘𝑥) = -(𝐹‘𝑣)) |
39 | 36, 38 | eqeq12d 2754 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑣 → ((𝐺‘𝑥) = -(𝐹‘𝑥) ↔ (𝐺‘𝑣) = -(𝐹‘𝑣))) |
40 | 35, 39 | imbi12d 345 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑣 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = -(𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) = -(𝐹‘𝑣)))) |
41 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
42 | 5 | negcld 11319 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -𝐵 ∈ ℂ) |
43 | 23 | fvmpt2 6886 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐴 ∧ -𝐵 ∈ ℂ) → (𝐺‘𝑥) = -𝐵) |
44 | 41, 42, 43 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = -𝐵) |
45 | 6 | fvmpt2 6886 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → (𝐹‘𝑥) = 𝐵) |
46 | 41, 5, 45 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) |
47 | 46 | negeqd 11215 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → -(𝐹‘𝑥) = -𝐵) |
48 | 44, 47 | eqtr4d 2781 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = -(𝐹‘𝑥)) |
49 | 33, 40, 48 | chvarfv 2233 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐺‘𝑣) = -(𝐹‘𝑣)) |
50 | 49 | oveq1d 7290 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐺‘𝑣) − -𝐶) = (-(𝐹‘𝑣) − -𝐶)) |
51 | 7 | ffvelrnda 6961 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ ℂ) |
52 | 3 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝐶 ∈ ℂ) |
53 | 51, 52 | negsubdi3d 42832 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → -((𝐹‘𝑣) − 𝐶) = (-(𝐹‘𝑣) − -𝐶)) |
54 | 50, 53 | eqtr4d 2781 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐺‘𝑣) − -𝐶) = -((𝐹‘𝑣) − 𝐶)) |
55 | 54 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐺‘𝑣) − -𝐶)) = (abs‘-((𝐹‘𝑣) − 𝐶))) |
56 | 51, 52 | subcld 11332 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝐹‘𝑣) − 𝐶) ∈ ℂ) |
57 | 56 | absnegd 15161 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘-((𝐹‘𝑣) − 𝐶)) = (abs‘((𝐹‘𝑣) − 𝐶))) |
58 | 55, 57 | eqtrd 2778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (abs‘((𝐺‘𝑣) − -𝐶)) = (abs‘((𝐹‘𝑣) − 𝐶))) |
59 | 58 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) → (abs‘((𝐺‘𝑣) − -𝐶)) = (abs‘((𝐹‘𝑣) − 𝐶))) |
60 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) |
61 | 59, 60 | eqbrtrd 5096 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) → (abs‘((𝐺‘𝑣) − -𝐶)) < 𝑦) |
62 | 17, 18, 21, 61 | syl21anc 835 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑦 ∈ ℝ+)
∧ 𝑤 ∈
ℝ+) ∧ 𝑣 ∈ 𝐴) ∧ ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) ∧ (𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤)) → (abs‘((𝐺‘𝑣) − -𝐶)) < 𝑦) |
63 | 62 | 3exp 1118 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑤 ∈ ℝ+)
∧ 𝑣 ∈ 𝐴) → (((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) → ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑣) − -𝐶)) < 𝑦))) |
64 | 63 | ralimdva 3108 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ 𝑤 ∈ ℝ+)
→ (∀𝑣 ∈
𝐴 ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) → ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑣) − -𝐶)) < 𝑦))) |
65 | 64 | reximdva 3203 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(∃𝑤 ∈
ℝ+ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑣) − 𝐶)) < 𝑦) → ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑣) − -𝐶)) < 𝑦))) |
66 | 15, 65 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑣) − -𝐶)) < 𝑦)) |
67 | 66 | ralrimiva 3103 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑤 ∈ ℝ+
∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑣) − -𝐶)) < 𝑦)) |
68 | 42, 23 | fmptd 6988 |
. . 3
⊢ (𝜑 → 𝐺:𝐴⟶ℂ) |
69 | 68, 8, 11 | ellimc3 25043 |
. 2
⊢ (𝜑 → (-𝐶 ∈ (𝐺 limℂ 𝐷) ↔ (-𝐶 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑣 ∈ 𝐴 ((𝑣 ≠ 𝐷 ∧ (abs‘(𝑣 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑣) − -𝐶)) < 𝑦)))) |
70 | 4, 67, 69 | mpbir2and 710 |
1
⊢ (𝜑 → -𝐶 ∈ (𝐺 limℂ 𝐷)) |