Step | Hyp | Ref
| Expression |
1 | | ellimcabssub0.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℂ) |
2 | | 0cnd 9912 |
. . . 4
⊢ (𝜑 → 0 ∈
ℂ) |
3 | 1, 2 | 2thd 254 |
. . 3
⊢ (𝜑 → (𝐶 ∈ ℂ ↔ 0 ∈
ℂ)) |
4 | | ellimcabssub0.b |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
5 | 1 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
6 | 4, 5 | subcld 10271 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 − 𝐶) ∈ ℂ) |
7 | | ellimcabssub0.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) |
8 | 6, 7 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:𝐴⟶ℂ) |
9 | 8 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℂ) |
10 | 9 | subid1d 10260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) − 0) = (𝐺‘𝑧)) |
11 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
12 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
13 | | csbov1g 6588 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V →
⦋𝑧 / 𝑥⦌(𝐵 − 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 − 𝐶)) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
⦋𝑧 /
𝑥⦌(𝐵 − 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 − 𝐶) |
15 | 14 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ⦋𝑧 / 𝑥⦌(𝐵 − 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 − 𝐶)) |
16 | | sban 2387 |
. . . . . . . . . . . . . . . . 17
⊢ ([𝑧 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) ↔ ([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝑥 ∈ 𝐴)) |
17 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝜑 |
18 | 17 | sbf 2368 |
. . . . . . . . . . . . . . . . . 18
⊢ ([𝑧 / 𝑥]𝜑 ↔ 𝜑) |
19 | | clelsb3 2716 |
. . . . . . . . . . . . . . . . . 18
⊢ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) |
20 | 18, 19 | anbi12i 729 |
. . . . . . . . . . . . . . . . 17
⊢ (([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑧 ∈ 𝐴)) |
21 | 16, 20 | bitri 263 |
. . . . . . . . . . . . . . . 16
⊢ ([𝑧 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑧 ∈ 𝐴)) |
22 | 4 | nfth 1718 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
23 | 22 | sbf 2368 |
. . . . . . . . . . . . . . . . 17
⊢ ([𝑧 / 𝑥]((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)) |
24 | | sbim 2383 |
. . . . . . . . . . . . . . . . 17
⊢ ([𝑧 / 𝑥]((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) ↔ ([𝑧 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) → [𝑧 / 𝑥]𝐵 ∈ ℂ)) |
25 | 23, 24 | sylbb1 226 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) → ([𝑧 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) → [𝑧 / 𝑥]𝐵 ∈ ℂ)) |
26 | 21, 25 | syl5bir 232 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) → ((𝜑 ∧ 𝑧 ∈ 𝐴) → [𝑧 / 𝑥]𝐵 ∈ ℂ)) |
27 | 4, 26 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → [𝑧 / 𝑥]𝐵 ∈ ℂ) |
28 | | sbsbc 3406 |
. . . . . . . . . . . . . . 15
⊢ ([𝑧 / 𝑥]𝐵 ∈ ℂ ↔ [𝑧 / 𝑥]𝐵 ∈ ℂ) |
29 | | sbcel1g 3939 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥]𝐵 ∈ ℂ ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ ℂ)) |
30 | 12, 29 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
([𝑧 / 𝑥]𝐵 ∈ ℂ ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ ℂ) |
31 | 28, 30 | bitri 263 |
. . . . . . . . . . . . . 14
⊢ ([𝑧 / 𝑥]𝐵 ∈ ℂ ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ ℂ) |
32 | 27, 31 | sylib 207 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ⦋𝑧 / 𝑥⦌𝐵 ∈ ℂ) |
33 | 1 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ ℂ) |
34 | 32, 33 | subcld 10271 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (⦋𝑧 / 𝑥⦌𝐵 − 𝐶) ∈ ℂ) |
35 | 15, 34 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ⦋𝑧 / 𝑥⦌(𝐵 − 𝐶) ∈ ℂ) |
36 | 7 | fvmpts 6194 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐴 ∧ ⦋𝑧 / 𝑥⦌(𝐵 − 𝐶) ∈ ℂ) → (𝐺‘𝑧) = ⦋𝑧 / 𝑥⦌(𝐵 − 𝐶)) |
37 | 11, 35, 36 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) = ⦋𝑧 / 𝑥⦌(𝐵 − 𝐶)) |
38 | | ellimcabssub0.f |
. . . . . . . . . . . . . 14
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
39 | 38 | fvmpts 6194 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐴 ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ ℂ) → (𝐹‘𝑧) = ⦋𝑧 / 𝑥⦌𝐵) |
40 | 11, 32, 39 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = ⦋𝑧 / 𝑥⦌𝐵) |
41 | 40 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) − 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 − 𝐶)) |
42 | 41, 14 | syl6reqr 2663 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ⦋𝑧 / 𝑥⦌(𝐵 − 𝐶) = ((𝐹‘𝑧) − 𝐶)) |
43 | 10, 37, 42 | 3eqtrrd 2649 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) − 𝐶) = ((𝐺‘𝑧) − 0)) |
44 | 43 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (abs‘((𝐹‘𝑧) − 𝐶)) = (abs‘((𝐺‘𝑧) − 0))) |
45 | 44 | breq1d 4593 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦 ↔ (abs‘((𝐺‘𝑧) − 0)) < 𝑦)) |
46 | 45 | imbi2d 329 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦) ↔ ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑧) − 0)) < 𝑦))) |
47 | 46 | ralbidva 2968 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑧) − 0)) < 𝑦))) |
48 | 47 | rexbidv 3034 |
. . . 4
⊢ (𝜑 → (∃𝑤 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦) ↔ ∃𝑤 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑧) − 0)) < 𝑦))) |
49 | 48 | ralbidv 2969 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦) ↔ ∀𝑦 ∈ ℝ+ ∃𝑤 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑧) − 0)) < 𝑦))) |
50 | 3, 49 | anbi12d 743 |
. 2
⊢ (𝜑 → ((𝐶 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦)) ↔ (0 ∈ ℂ ∧
∀𝑦 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑧) − 0)) < 𝑦)))) |
51 | 4, 38 | fmptd 6292 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
52 | | ellimcabssub0.a |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
53 | | ellimcabssub0.p |
. . 3
⊢ (𝜑 → 𝐷 ∈ ℂ) |
54 | 51, 52, 53 | ellimc3 23449 |
. 2
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐷) ↔ (𝐶 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦)))) |
55 | 8, 52, 53 | ellimc3 23449 |
. 2
⊢ (𝜑 → (0 ∈ (𝐺 limℂ 𝐷) ↔ (0 ∈ ℂ ∧
∀𝑦 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑧) − 0)) < 𝑦)))) |
56 | 50, 54, 55 | 3bitr4d 299 |
1
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐷) ↔ 0 ∈ (𝐺 limℂ 𝐷))) |