| Step | Hyp | Ref
| Expression |
| 1 | | ellimcabssub0.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 2 | | 0cnd 11254 |
. . . 4
⊢ (𝜑 → 0 ∈
ℂ) |
| 3 | 1, 2 | 2thd 265 |
. . 3
⊢ (𝜑 → (𝐶 ∈ ℂ ↔ 0 ∈
ℂ)) |
| 4 | | ellimcabssub0.b |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 5 | 1 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
| 6 | 4, 5 | subcld 11620 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 − 𝐶) ∈ ℂ) |
| 7 | | ellimcabssub0.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) |
| 8 | 6, 7 | fmptd 7134 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:𝐴⟶ℂ) |
| 9 | 8 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ ℂ) |
| 10 | 9 | subid1d 11609 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐺‘𝑧) − 0) = (𝐺‘𝑧)) |
| 11 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
| 12 | | csbov1g 7478 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ V →
⦋𝑧 / 𝑥⦌(𝐵 − 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 − 𝐶)) |
| 13 | 12 | elv 3485 |
. . . . . . . . . . . 12
⊢
⦋𝑧 /
𝑥⦌(𝐵 − 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 − 𝐶) |
| 14 | | sban 2080 |
. . . . . . . . . . . . . . . . 17
⊢ ([𝑧 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) ↔ ([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝑥 ∈ 𝐴)) |
| 15 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝜑 |
| 16 | 15 | sbf 2271 |
. . . . . . . . . . . . . . . . . 18
⊢ ([𝑧 / 𝑥]𝜑 ↔ 𝜑) |
| 17 | | clelsb1 2868 |
. . . . . . . . . . . . . . . . . 18
⊢ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴) |
| 18 | 16, 17 | anbi12i 628 |
. . . . . . . . . . . . . . . . 17
⊢ (([𝑧 / 𝑥]𝜑 ∧ [𝑧 / 𝑥]𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑧 ∈ 𝐴)) |
| 19 | 14, 18 | bitri 275 |
. . . . . . . . . . . . . . . 16
⊢ ([𝑧 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑧 ∈ 𝐴)) |
| 20 | 4 | nfth 1801 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) |
| 21 | 20 | sbf 2271 |
. . . . . . . . . . . . . . . . 17
⊢ ([𝑧 / 𝑥]((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)) |
| 22 | | sbim 2303 |
. . . . . . . . . . . . . . . . 17
⊢ ([𝑧 / 𝑥]((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) ↔ ([𝑧 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) → [𝑧 / 𝑥]𝐵 ∈ ℂ)) |
| 23 | 21, 22 | sylbb1 237 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) → ([𝑧 / 𝑥](𝜑 ∧ 𝑥 ∈ 𝐴) → [𝑧 / 𝑥]𝐵 ∈ ℂ)) |
| 24 | 19, 23 | biimtrrid 243 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ) → ((𝜑 ∧ 𝑧 ∈ 𝐴) → [𝑧 / 𝑥]𝐵 ∈ ℂ)) |
| 25 | 4, 24 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → [𝑧 / 𝑥]𝐵 ∈ ℂ) |
| 26 | | sbsbc 3792 |
. . . . . . . . . . . . . . 15
⊢ ([𝑧 / 𝑥]𝐵 ∈ ℂ ↔ [𝑧 / 𝑥]𝐵 ∈ ℂ) |
| 27 | | sbcel1g 4416 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥]𝐵 ∈ ℂ ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ ℂ)) |
| 28 | 27 | elv 3485 |
. . . . . . . . . . . . . . 15
⊢
([𝑧 / 𝑥]𝐵 ∈ ℂ ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ ℂ) |
| 29 | 26, 28 | bitri 275 |
. . . . . . . . . . . . . 14
⊢ ([𝑧 / 𝑥]𝐵 ∈ ℂ ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ ℂ) |
| 30 | 25, 29 | sylib 218 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ⦋𝑧 / 𝑥⦌𝐵 ∈ ℂ) |
| 31 | 1 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐶 ∈ ℂ) |
| 32 | 30, 31 | subcld 11620 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (⦋𝑧 / 𝑥⦌𝐵 − 𝐶) ∈ ℂ) |
| 33 | 13, 32 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ⦋𝑧 / 𝑥⦌(𝐵 − 𝐶) ∈ ℂ) |
| 34 | 7 | fvmpts 7019 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐴 ∧ ⦋𝑧 / 𝑥⦌(𝐵 − 𝐶) ∈ ℂ) → (𝐺‘𝑧) = ⦋𝑧 / 𝑥⦌(𝐵 − 𝐶)) |
| 35 | 11, 33, 34 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) = ⦋𝑧 / 𝑥⦌(𝐵 − 𝐶)) |
| 36 | | ellimcabssub0.f |
. . . . . . . . . . . . . 14
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 37 | 36 | fvmpts 7019 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐴 ∧ ⦋𝑧 / 𝑥⦌𝐵 ∈ ℂ) → (𝐹‘𝑧) = ⦋𝑧 / 𝑥⦌𝐵) |
| 38 | 11, 30, 37 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = ⦋𝑧 / 𝑥⦌𝐵) |
| 39 | 38 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) − 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 − 𝐶)) |
| 40 | 13, 39 | eqtr4id 2796 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ⦋𝑧 / 𝑥⦌(𝐵 − 𝐶) = ((𝐹‘𝑧) − 𝐶)) |
| 41 | 10, 35, 40 | 3eqtrrd 2782 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) − 𝐶) = ((𝐺‘𝑧) − 0)) |
| 42 | 41 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (abs‘((𝐹‘𝑧) − 𝐶)) = (abs‘((𝐺‘𝑧) − 0))) |
| 43 | 42 | breq1d 5153 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦 ↔ (abs‘((𝐺‘𝑧) − 0)) < 𝑦)) |
| 44 | 43 | imbi2d 340 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦) ↔ ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑧) − 0)) < 𝑦))) |
| 45 | 44 | ralbidva 3176 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦) ↔ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑧) − 0)) < 𝑦))) |
| 46 | 45 | rexbidv 3179 |
. . . 4
⊢ (𝜑 → (∃𝑤 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦) ↔ ∃𝑤 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑧) − 0)) < 𝑦))) |
| 47 | 46 | ralbidv 3178 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦) ↔ ∀𝑦 ∈ ℝ+ ∃𝑤 ∈ ℝ+
∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑧) − 0)) < 𝑦))) |
| 48 | 3, 47 | anbi12d 632 |
. 2
⊢ (𝜑 → ((𝐶 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦)) ↔ (0 ∈ ℂ ∧
∀𝑦 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑧) − 0)) < 𝑦)))) |
| 49 | 4, 36 | fmptd 7134 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
| 50 | | ellimcabssub0.a |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
| 51 | | ellimcabssub0.p |
. . 3
⊢ (𝜑 → 𝐷 ∈ ℂ) |
| 52 | 49, 50, 51 | ellimc3 25914 |
. 2
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐷) ↔ (𝐶 ∈ ℂ ∧ ∀𝑦 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑦)))) |
| 53 | 8, 50, 51 | ellimc3 25914 |
. 2
⊢ (𝜑 → (0 ∈ (𝐺 limℂ 𝐷) ↔ (0 ∈ ℂ ∧
∀𝑦 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐷 ∧ (abs‘(𝑧 − 𝐷)) < 𝑤) → (abs‘((𝐺‘𝑧) − 0)) < 𝑦)))) |
| 54 | 48, 52, 53 | 3bitr4d 311 |
1
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐷) ↔ 0 ∈ (𝐺 limℂ 𝐷))) |