ellimcabssub0

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

	Ref	Expression
Hypotheses	ellimcabssub0.f	$⊢ F = (x \in A ⟼ B)$
	ellimcabssub0.g	$⊢ G = (x \in A ⟼ B - C)$
	ellimcabssub0.a	$⊢ φ \to A \subseteq ℂ$
	ellimcabssub0.b	$⊢ (φ \land x \in A) \to B \in ℂ$
	ellimcabssub0.p	$⊢ φ \to D \in ℂ$
	ellimcabssub0.c	$⊢ φ \to C \in ℂ$
Assertion	ellimcabssub0	$⊢ φ \to (C \in (F {lim}_{ℂ} D) \leftrightarrow 0 \in (G {lim}_{ℂ} D))$

Proof

Step	Hyp	Ref	Expression
1		ellimcabssub0.f	$⊢ F = (x \in A ⟼ B)$
2		ellimcabssub0.g	$⊢ G = (x \in A ⟼ B - C)$
3		ellimcabssub0.a	$⊢ φ \to A \subseteq ℂ$
4		ellimcabssub0.b	$⊢ (φ \land x \in A) \to B \in ℂ$
5		ellimcabssub0.p	$⊢ φ \to D \in ℂ$
6		ellimcabssub0.c	$⊢ φ \to C \in ℂ$
7		0cnd	$⊢ φ \to 0 \in ℂ$
8	6 7	2thd	$⊢ φ \to (C \in ℂ \leftrightarrow 0 \in ℂ)$
9	6	adantr	$⊢ (φ \land x \in A) \to C \in ℂ$
10	4 9	subcld	$⊢ (φ \land x \in A) \to B - C \in ℂ$
11	10 2	fmptd	$⊢ φ \to G : A ⟶ ℂ$
12	11	ffvelcdmda	$⊢ (φ \land z \in A) \to G (z) \in ℂ$
13	12	subid1d	$⊢ (φ \land z \in A) \to G (z) - 0 = G (z)$
14		simpr	$⊢ (φ \land z \in A) \to z \in A$
15		csbov1g	$⊢ z \in V \to ⦋ z / x ⦌ (B - C) = ⦋ z / x ⦌ B - C$
16	15	elv	$⊢ ⦋ z / x ⦌ (B - C) = ⦋ z / x ⦌ B - C$
17		sban	$⊢ [z/ x] (φ \land x \in A) \leftrightarrow ([z/ x] φ \land [z/ x] x \in A)$
18		nfv	$⊢ Ⅎ x φ$
19	18	sbf	$⊢ [z/ x] φ \leftrightarrow φ$
20		clelsb1	$⊢ [z/ x] x \in A \leftrightarrow z \in A$
21	19 20	anbi12i	$⊢ ([z/ x] φ \land [z/ x] x \in A) \leftrightarrow (φ \land z \in A)$
22	17 21	bitri	$⊢ [z/ x] (φ \land x \in A) \leftrightarrow (φ \land z \in A)$
23	4	nfth	$⊢ Ⅎ x ((φ \land x \in A) \to B \in ℂ)$
24	23	sbf	$⊢ [z/ x] ((φ \land x \in A) \to B \in ℂ) \leftrightarrow ((φ \land x \in A) \to B \in ℂ)$
25		sbim	$⊢ [z/ x] ((φ \land x \in A) \to B \in ℂ) \leftrightarrow ([z/ x] (φ \land x \in A) \to [z/ x] B \in ℂ)$
26	24 25	sylbb1	$⊢ ((φ \land x \in A) \to B \in ℂ) \to ([z/ x] (φ \land x \in A) \to [z/ x] B \in ℂ)$
27	22 26	biimtrrid	$⊢ ((φ \land x \in A) \to B \in ℂ) \to ((φ \land z \in A) \to [z/ x] B \in ℂ)$
28	4 27	ax-mp	$⊢ (φ \land z \in A) \to [z/ x] B \in ℂ$
29		sbsbc	$⊢ [z/ x] B \in ℂ \leftrightarrow \underset{˙}{[} z / x \underset{˙}{]} B \in ℂ$
30		sbcel1g	$⊢ z \in V \to (\underset{˙}{[} z / x \underset{˙}{]} B \in ℂ \leftrightarrow ⦋ z / x ⦌ B \in ℂ)$
31	30	elv	$⊢ \underset{˙}{[} z / x \underset{˙}{]} B \in ℂ \leftrightarrow ⦋ z / x ⦌ B \in ℂ$
32	29 31	bitri	$⊢ [z/ x] B \in ℂ \leftrightarrow ⦋ z / x ⦌ B \in ℂ$
33	28 32	sylib	$⊢ (φ \land z \in A) \to ⦋ z / x ⦌ B \in ℂ$
34	6	adantr	$⊢ (φ \land z \in A) \to C \in ℂ$
35	33 34	subcld	$⊢ (φ \land z \in A) \to ⦋ z / x ⦌ B - C \in ℂ$
36	16 35	eqeltrid	$⊢ (φ \land z \in A) \to ⦋ z / x ⦌ (B - C) \in ℂ$
37	2	fvmpts	$⊢ (z \in A \land ⦋ z / x ⦌ (B - C) \in ℂ) \to G (z) = ⦋ z / x ⦌ (B - C)$
38	14 36 37	syl2anc	$⊢ (φ \land z \in A) \to G (z) = ⦋ z / x ⦌ (B - C)$
39	1	fvmpts	$⊢ (z \in A \land ⦋ z / x ⦌ B \in ℂ) \to F (z) = ⦋ z / x ⦌ B$
40	14 33 39	syl2anc	$⊢ (φ \land z \in A) \to F (z) = ⦋ z / x ⦌ B$
41	40	oveq1d	$⊢ (φ \land z \in A) \to F (z) - C = ⦋ z / x ⦌ B - C$
42	16 41	eqtr4id	$⊢ (φ \land z \in A) \to ⦋ z / x ⦌ (B - C) = F (z) - C$
43	13 38 42	3eqtrrd	$⊢ (φ \land z \in A) \to F (z) - C = G (z) - 0$
44	43	fveq2d	$⊢ (φ \land z \in A) \to \|F (z) - C\| = \|G (z) - 0\|$
45	44	breq1d	$⊢ (φ \land z \in A) \to (\|F (z) - C\| < y \leftrightarrow \|G (z) - 0\| < y)$
46	45	imbi2d	$⊢ (φ \land z \in A) \to (((z \neq D \land \|z - D\| < w) \to \|F (z) - C\| < y) \leftrightarrow ((z \neq D \land \|z - D\| < w) \to \|G (z) - 0\| < y))$
47	46	ralbidva	$⊢ φ \to (\forall z \in A ((z \neq D \land \|z - D\| < w) \to \|F (z) - C\| < y) \leftrightarrow \forall z \in A ((z \neq D \land \|z - D\| < w) \to \|G (z) - 0\| < y))$
48	47	rexbidv	$⊢ φ \to (\exists w \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < w) \to \|F (z) - C\| < y) \leftrightarrow \exists w \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < w) \to \|G (z) - 0\| < y))$
49	48	ralbidv	$⊢ φ \to (\forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < w) \to \|F (z) - C\| < y) \leftrightarrow \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < w) \to \|G (z) - 0\| < y))$
50	8 49	anbi12d	$⊢ φ \to ((C \in ℂ \land \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < w) \to \|F (z) - C\| < y)) \leftrightarrow (0 \in ℂ \land \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < w) \to \|G (z) - 0\| < y)))$
51	4 1	fmptd	$⊢ φ \to F : A ⟶ ℂ$
52	51 3 5	ellimc3	$⊢ φ \to (C \in (F {lim}_{ℂ} D) \leftrightarrow (C \in ℂ \land \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < w) \to \|F (z) - C\| < y)))$
53	11 3 5	ellimc3	$⊢ φ \to (0 \in (G {lim}_{ℂ} D) \leftrightarrow (0 \in ℂ \land \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < w) \to \|G (z) - 0\| < y)))$
54	50 52 53	3bitr4d	$⊢ φ \to (C \in (F {lim}_{ℂ} D) \leftrightarrow 0 \in (G {lim}_{ℂ} D))$

Metamath Proof Explorer

Theorem ellimcabssub0

Proof