Metamath Proof Explorer

Theorem ellimcabssub0

Description: An equivalent condition for being a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ellimcabssub0.f ⊢ F = x ∈ A ⟼ B
ellimcabssub0.g ⊢ G = x ∈ A ⟼ B − C
ellimcabssub0.a ⊢ φ → A ⊆ ℂ
ellimcabssub0.b ⊢ φ ∧ x ∈ A → B ∈ ℂ
ellimcabssub0.p ⊢ φ → D ∈ ℂ
ellimcabssub0.c ⊢ φ → C ∈ ℂ
Assertion ellimcabssub0 ⊢ φ → C ∈ F lim ℂ D ↔ 0 ∈ G lim ℂ D

Proof

Step Hyp Ref Expression
1 ellimcabssub0.f ⊢ F = x ∈ A ⟼ B
2 ellimcabssub0.g ⊢ G = x ∈ A ⟼ B − C
3 ellimcabssub0.a ⊢ φ → A ⊆ ℂ
4 ellimcabssub0.b ⊢ φ ∧ x ∈ A → B ∈ ℂ
5 ellimcabssub0.p ⊢ φ → D ∈ ℂ
6 ellimcabssub0.c ⊢ φ → C ∈ ℂ
7 0cnd ⊢ φ → 0 ∈ ℂ
8 6 7 2thd ⊢ φ → C ∈ ℂ ↔ 0 ∈ ℂ
9 6 adantr ⊢ φ ∧ x ∈ A → C ∈ ℂ
10 4 9 subcld ⊢ φ ∧ x ∈ A → B − C ∈ ℂ
11 10 2 fmptd ⊢ φ → G : A ⟶ ℂ
12 11 ffvelrnda ⊢ φ ∧ z ∈ A → G ⁡ z ∈ ℂ
13 12 subid1d ⊢ φ ∧ z ∈ A → G ⁡ z − 0 = G ⁡ z
14 simpr ⊢ φ ∧ z ∈ A → z ∈ A
15 csbov1g ⊢ z ∈ V → ⦋ z / x⦌ B − C = ⦋ z / x⦌ B − C
16 15 elv ⊢ ⦋ z / x⦌ B − C = ⦋ z / x⦌ B − C
17 sban ⊢ z x φ ∧ x ∈ A ↔ z x φ ∧ z x x ∈ A
18 nfv ⊢ Ⅎ x φ
19 18 sbf ⊢ z x φ ↔ φ
20 clelsb3 ⊢ z x x ∈ A ↔ z ∈ A
21 19 20 anbi12i ⊢ z x φ ∧ z x x ∈ A ↔ φ ∧ z ∈ A
22 17 21 bitri ⊢ z x φ ∧ x ∈ A ↔ φ ∧ z ∈ A
23 4 nfth ⊢ Ⅎ x φ ∧ x ∈ A → B ∈ ℂ
24 23 sbf ⊢ z x φ ∧ x ∈ A → B ∈ ℂ ↔ φ ∧ x ∈ A → B ∈ ℂ
25 sbim ⊢ z x φ ∧ x ∈ A → B ∈ ℂ ↔ z x φ ∧ x ∈ A → z x B ∈ ℂ
26 24 25 sylbb1 ⊢ φ ∧ x ∈ A → B ∈ ℂ → z x φ ∧ x ∈ A → z x B ∈ ℂ
27 22 26 syl5bir ⊢ φ ∧ x ∈ A → B ∈ ℂ → φ ∧ z ∈ A → z x B ∈ ℂ
28 4 27 ax-mp ⊢ φ ∧ z ∈ A → z x B ∈ ℂ
29 sbsbc ⊢ z x B ∈ ℂ ↔ [˙z / x]˙ B ∈ ℂ
30 sbcel1g ⊢ z ∈ V → [˙z / x]˙ B ∈ ℂ ↔ ⦋ z / x⦌ B ∈ ℂ
31 30 elv ⊢ [˙z / x]˙ B ∈ ℂ ↔ ⦋ z / x⦌ B ∈ ℂ
32 29 31 bitri ⊢ z x B ∈ ℂ ↔ ⦋ z / x⦌ B ∈ ℂ
33 28 32 sylib ⊢ φ ∧ z ∈ A → ⦋ z / x⦌ B ∈ ℂ
34 6 adantr ⊢ φ ∧ z ∈ A → C ∈ ℂ
35 33 34 subcld ⊢ φ ∧ z ∈ A → ⦋ z / x⦌ B − C ∈ ℂ
36 16 35 eqeltrid ⊢ φ ∧ z ∈ A → ⦋ z / x⦌ B − C ∈ ℂ
37 2 fvmpts ⊢ z ∈ A ∧ ⦋ z / x⦌ B − C ∈ ℂ → G ⁡ z = ⦋ z / x⦌ B − C
38 14 36 37 syl2anc ⊢ φ ∧ z ∈ A → G ⁡ z = ⦋ z / x⦌ B − C
39 1 fvmpts ⊢ z ∈ A ∧ ⦋ z / x⦌ B ∈ ℂ → F ⁡ z = ⦋ z / x⦌ B
40 14 33 39 syl2anc ⊢ φ ∧ z ∈ A → F ⁡ z = ⦋ z / x⦌ B
41 40 oveq1d ⊢ φ ∧ z ∈ A → F ⁡ z − C = ⦋ z / x⦌ B − C
42 16 41 eqtr4id ⊢ φ ∧ z ∈ A → ⦋ z / x⦌ B − C = F ⁡ z − C
43 13 38 42 3eqtrrd ⊢ φ ∧ z ∈ A → F ⁡ z − C = G ⁡ z − 0
44 43 fveq2d ⊢ φ ∧ z ∈ A → F ⁡ z − C = G ⁡ z − 0
45 44 breq1d ⊢ φ ∧ z ∈ A → F ⁡ z − C < y ↔ G ⁡ z − 0 < y
46 45 imbi2d ⊢ φ ∧ z ∈ A → z ≠ D ∧ z − D < w → F ⁡ z − C < y ↔ z ≠ D ∧ z − D < w → G ⁡ z − 0 < y
47 46 ralbidva ⊢ φ → ∀ z ∈ A z ≠ D ∧ z − D < w → F ⁡ z − C < y ↔ ∀ z ∈ A z ≠ D ∧ z − D < w → G ⁡ z − 0 < y
48 47 rexbidv ⊢ φ → ∃ w ∈ ℝ + ∀ z ∈ A z ≠ D ∧ z − D < w → F ⁡ z − C < y ↔ ∃ w ∈ ℝ + ∀ z ∈ A z ≠ D ∧ z − D < w → G ⁡ z − 0 < y
49 48 ralbidv ⊢ φ → ∀ y ∈ ℝ + ∃ w ∈ ℝ + ∀ z ∈ A z ≠ D ∧ z − D < w → F ⁡ z − C < y ↔ ∀ y ∈ ℝ + ∃ w ∈ ℝ + ∀ z ∈ A z ≠ D ∧ z − D < w → G ⁡ z − 0 < y
50 8 49 anbi12d ⊢ φ → C ∈ ℂ ∧ ∀ y ∈ ℝ + ∃ w ∈ ℝ + ∀ z ∈ A z ≠ D ∧ z − D < w → F ⁡ z − C < y ↔ 0 ∈ ℂ ∧ ∀ y ∈ ℝ + ∃ w ∈ ℝ + ∀ z ∈ A z ≠ D ∧ z − D < w → G ⁡ z − 0 < y
51 4 1 fmptd ⊢ φ → F : A ⟶ ℂ
52 51 3 5 ellimc3 ⊢ φ → C ∈ F lim ℂ D ↔ C ∈ ℂ ∧ ∀ y ∈ ℝ + ∃ w ∈ ℝ + ∀ z ∈ A z ≠ D ∧ z − D < w → F ⁡ z − C < y
53 11 3 5 ellimc3 ⊢ φ → 0 ∈ G lim ℂ D ↔ 0 ∈ ℂ ∧ ∀ y ∈ ℝ + ∃ w ∈ ℝ + ∀ z ∈ A z ≠ D ∧ z − D < w → G ⁡ z − 0 < y
54 50 52 53 3bitr4d ⊢ φ → C ∈ F lim ℂ D ↔ 0 ∈ G lim ℂ D