ellimc3

Description: Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016)

	Ref	Expression
Hypotheses	ellimc3.f	$⊢ φ \to F : A ⟶ ℂ$
	ellimc3.a	$⊢ φ \to A \subseteq ℂ$
	ellimc3.b	$⊢ φ \to B \in ℂ$
Assertion	ellimc3	$⊢ φ \to (C \in (F {lim}_{ℂ} B) \leftrightarrow (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - C\| < x)))$

Proof

Step	Hyp	Ref	Expression
1		ellimc3.f	$⊢ φ \to F : A ⟶ ℂ$
2		ellimc3.a	$⊢ φ \to A \subseteq ℂ$
3		ellimc3.b	$⊢ φ \to B \in ℂ$
4		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
5	1 2 3 4	ellimc2	$⊢ φ \to (C \in (F {lim}_{ℂ} B) \leftrightarrow (C \in ℂ \land \forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u))))$
6		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
7		simplr	$⊢ ((φ \land C \in ℂ) \land x \in ℝ^{+}) \to C \in ℂ$
8		simpr	$⊢ ((φ \land C \in ℂ) \land x \in ℝ^{+}) \to x \in ℝ^{+}$
9		blcntr	$⊢ (abs \circ - \in ∞Met (ℂ) \land C \in ℂ \land x \in ℝ^{+}) \to C \in (C ball (abs \circ -) x)$
10	6 7 8 9	mp3an2i	$⊢ ((φ \land C \in ℂ) \land x \in ℝ^{+}) \to C \in (C ball (abs \circ -) x)$
11		rpxr	$⊢ x \in ℝ^{+} \to x \in ℝ^{*}$
12	11	adantl	$⊢ ((φ \land C \in ℂ) \land x \in ℝ^{+}) \to x \in ℝ^{*}$
13	4	cnfldtopn	$⊢ TopOpen (ℂ_{fld}) = MetOpen (abs \circ -)$
14	13	blopn	$⊢ (abs \circ - \in ∞Met (ℂ) \land C \in ℂ \land x \in ℝ^{*}) \to C ball (abs \circ -) x \in TopOpen (ℂ_{fld})$
15	6 7 12 14	mp3an2i	$⊢ ((φ \land C \in ℂ) \land x \in ℝ^{+}) \to C ball (abs \circ -) x \in TopOpen (ℂ_{fld})$
16		eleq2	$⊢ u = C ball (abs \circ -) x \to (C \in u \leftrightarrow C \in (C ball (abs \circ -) x))$
17		sseq2	$⊢ u = C ball (abs \circ -) x \to (F [v \cap (A ∖ \{B\})] \subseteq u \leftrightarrow F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)$
18	17	anbi2d	$⊢ u = C ball (abs \circ -) x \to ((B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u) \leftrightarrow (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x))$
19	18	rexbidv	$⊢ u = C ball (abs \circ -) x \to (\exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u) \leftrightarrow \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x))$
20	16 19	imbi12d	$⊢ u = C ball (abs \circ -) x \to ((C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)) \leftrightarrow (C \in (C ball (abs \circ -) x) \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)))$
21	20	rspcv	$⊢ C ball (abs \circ -) x \in TopOpen (ℂ_{fld}) \to (\forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)) \to (C \in (C ball (abs \circ -) x) \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)))$
22	15 21	syl	$⊢ ((φ \land C \in ℂ) \land x \in ℝ^{+}) \to (\forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)) \to (C \in (C ball (abs \circ -) x) \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)))$
23	10 22	mpid	$⊢ ((φ \land C \in ℂ) \land x \in ℝ^{+}) \to (\forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)) \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x))$
24	13	mopni2	$⊢ (abs \circ - \in ∞Met (ℂ) \land v \in TopOpen (ℂ_{fld}) \land B \in v) \to \exists y \in ℝ^{+} B ball (abs \circ -) y \subseteq v$
25	6 24	mp3an1	$⊢ (v \in TopOpen (ℂ_{fld}) \land B \in v) \to \exists y \in ℝ^{+} B ball (abs \circ -) y \subseteq v$
26		ssrin	$⊢ B ball (abs \circ -) y \subseteq v \to (B ball (abs \circ -) y) \cap (A ∖ \{B\}) \subseteq v \cap (A ∖ \{B\})$
27		imass2	$⊢ (B ball (abs \circ -) y) \cap (A ∖ \{B\}) \subseteq v \cap (A ∖ \{B\}) \to F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq F [v \cap (A ∖ \{B\})]$
28		sstr2	$⊢ F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq F [v \cap (A ∖ \{B\})] \to (F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)$
29	26 27 28	3syl	$⊢ B ball (abs \circ -) y \subseteq v \to (F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)$
30	29	com12	$⊢ F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to (B ball (abs \circ -) y \subseteq v \to F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)$
31	30	reximdv	$⊢ F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to (\exists y \in ℝ^{+} B ball (abs \circ -) y \subseteq v \to \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)$
32	25 31	syl5com	$⊢ (v \in TopOpen (ℂ_{fld}) \land B \in v) \to (F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)$
33	32	impr	$⊢ (v \in TopOpen (ℂ_{fld}) \land (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)) \to \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x$
34	33	rexlimiva	$⊢ \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x) \to \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x$
35	23 34	syl6	$⊢ ((φ \land C \in ℂ) \land x \in ℝ^{+}) \to (\forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)) \to \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)$
36	35	ralrimdva	$⊢ (φ \land C \in ℂ) \to (\forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)) \to \forall x \in ℝ^{+} \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)$
37	13	mopni2	$⊢ (abs \circ - \in ∞Met (ℂ) \land u \in TopOpen (ℂ_{fld}) \land C \in u) \to \exists x \in ℝ^{+} C ball (abs \circ -) x \subseteq u$
38	6 37	mp3an1	$⊢ (u \in TopOpen (ℂ_{fld}) \land C \in u) \to \exists x \in ℝ^{+} C ball (abs \circ -) x \subseteq u$
39		r19.29r	$⊢ (\exists x \in ℝ^{+} C ball (abs \circ -) x \subseteq u \land \forall x \in ℝ^{+} \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x) \to \exists x \in ℝ^{+} (C ball (abs \circ -) x \subseteq u \land \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)$
40	3	ad3antrrr	$⊢ (((φ \land C \in ℂ) \land x \in ℝ^{+}) \land y \in ℝ^{+}) \to B \in ℂ$
41		simpr	$⊢ (((φ \land C \in ℂ) \land x \in ℝ^{+}) \land y \in ℝ^{+}) \to y \in ℝ^{+}$
42	41	rpxrd	$⊢ (((φ \land C \in ℂ) \land x \in ℝ^{+}) \land y \in ℝ^{+}) \to y \in ℝ^{*}$
43	13	blopn	$⊢ (abs \circ - \in ∞Met (ℂ) \land B \in ℂ \land y \in ℝ^{*}) \to B ball (abs \circ -) y \in TopOpen (ℂ_{fld})$
44	6 40 42 43	mp3an2i	$⊢ (((φ \land C \in ℂ) \land x \in ℝ^{+}) \land y \in ℝ^{+}) \to B ball (abs \circ -) y \in TopOpen (ℂ_{fld})$
45		blcntr	$⊢ (abs \circ - \in ∞Met (ℂ) \land B \in ℂ \land y \in ℝ^{+}) \to B \in (B ball (abs \circ -) y)$
46	6 40 41 45	mp3an2i	$⊢ (((φ \land C \in ℂ) \land x \in ℝ^{+}) \land y \in ℝ^{+}) \to B \in (B ball (abs \circ -) y)$
47		eleq2	$⊢ v = B ball (abs \circ -) y \to (B \in v \leftrightarrow B \in (B ball (abs \circ -) y))$
48		ineq1	$⊢ v = B ball (abs \circ -) y \to v \cap (A ∖ \{B\}) = (B ball (abs \circ -) y) \cap (A ∖ \{B\})$
49	48	imaeq2d	$⊢ v = B ball (abs \circ -) y \to F [v \cap (A ∖ \{B\})] = F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})]$
50	49	sseq1d	$⊢ v = B ball (abs \circ -) y \to (F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \leftrightarrow F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)$
51	47 50	anbi12d	$⊢ v = B ball (abs \circ -) y \to ((B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x) \leftrightarrow (B \in (B ball (abs \circ -) y) \land F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x))$
52	51	rspcev	$⊢ (B ball (abs \circ -) y \in TopOpen (ℂ_{fld}) \land (B \in (B ball (abs \circ -) y) \land F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)) \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)$
53	52	expr	$⊢ (B ball (abs \circ -) y \in TopOpen (ℂ_{fld}) \land B \in (B ball (abs \circ -) y)) \to (F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x))$
54	44 46 53	syl2anc	$⊢ (((φ \land C \in ℂ) \land x \in ℝ^{+}) \land y \in ℝ^{+}) \to (F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x))$
55	54	rexlimdva	$⊢ ((φ \land C \in ℂ) \land x \in ℝ^{+}) \to (\exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x))$
56		sstr2	$⊢ F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to (C ball (abs \circ -) x \subseteq u \to F [v \cap (A ∖ \{B\})] \subseteq u)$
57	56	com12	$⊢ C ball (abs \circ -) x \subseteq u \to (F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to F [v \cap (A ∖ \{B\})] \subseteq u)$
58	57	anim2d	$⊢ C ball (abs \circ -) x \subseteq u \to ((B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x) \to (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u))$
59	58	reximdv	$⊢ C ball (abs \circ -) x \subseteq u \to (\exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x) \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u))$
60	55 59	syl9	$⊢ ((φ \land C \in ℂ) \land x \in ℝ^{+}) \to (C ball (abs \circ -) x \subseteq u \to (\exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)))$
61	60	impd	$⊢ ((φ \land C \in ℂ) \land x \in ℝ^{+}) \to ((C ball (abs \circ -) x \subseteq u \land \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x) \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u))$
62	61	rexlimdva	$⊢ (φ \land C \in ℂ) \to (\exists x \in ℝ^{+} (C ball (abs \circ -) x \subseteq u \land \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x) \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u))$
63	39 62	syl5	$⊢ (φ \land C \in ℂ) \to ((\exists x \in ℝ^{+} C ball (abs \circ -) x \subseteq u \land \forall x \in ℝ^{+} \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x) \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u))$
64	63	expd	$⊢ (φ \land C \in ℂ) \to (\exists x \in ℝ^{+} C ball (abs \circ -) x \subseteq u \to (\forall x \in ℝ^{+} \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)))$
65	38 64	syl5	$⊢ (φ \land C \in ℂ) \to ((u \in TopOpen (ℂ_{fld}) \land C \in u) \to (\forall x \in ℝ^{+} \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)))$
66	65	expdimp	$⊢ ((φ \land C \in ℂ) \land u \in TopOpen (ℂ_{fld})) \to (C \in u \to (\forall x \in ℝ^{+} \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)))$
67	66	com23	$⊢ ((φ \land C \in ℂ) \land u \in TopOpen (ℂ_{fld})) \to (\forall x \in ℝ^{+} \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)))$
68	67	ralrimdva	$⊢ (φ \land C \in ℂ) \to (\forall x \in ℝ^{+} \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \to \forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)))$
69	36 68	impbid	$⊢ (φ \land C \in ℂ) \to (\forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)) \leftrightarrow \forall x \in ℝ^{+} \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x)$
70	1	ad2antrr	$⊢ ((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to F : A ⟶ ℂ$
71	70	ffund	$⊢ ((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to Fun F$
72		inss2	$⊢ (B ball (abs \circ -) y) \cap (A ∖ \{B\}) \subseteq A ∖ \{B\}$
73		difss	$⊢ A ∖ \{B\} \subseteq A$
74	70	fdmd	$⊢ ((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to dom F = A$
75	73 74	sseqtrrid	$⊢ ((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to A ∖ \{B\} \subseteq dom F$
76	72 75	sstrid	$⊢ ((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to (B ball (abs \circ -) y) \cap (A ∖ \{B\}) \subseteq dom F$
77		funimass4	$⊢ (Fun F \land (B ball (abs \circ -) y) \cap (A ∖ \{B\}) \subseteq dom F) \to (F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \leftrightarrow \forall z \in ((B ball (abs \circ -) y) \cap (A ∖ \{B\})) F (z) \in (C ball (abs \circ -) x))$
78	71 76 77	syl2anc	$⊢ ((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to (F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \leftrightarrow \forall z \in ((B ball (abs \circ -) y) \cap (A ∖ \{B\})) F (z) \in (C ball (abs \circ -) x))$
79	6	a1i	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to abs \circ - \in ∞Met (ℂ)$
80		simplrr	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to y \in ℝ^{+}$
81	80	rpxrd	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to y \in ℝ^{*}$
82	3	ad3antrrr	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to B \in ℂ$
83	73 2	sstrid	$⊢ φ \to A ∖ \{B\} \subseteq ℂ$
84	83	ad2antrr	$⊢ ((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to A ∖ \{B\} \subseteq ℂ$
85	84	sselda	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to z \in ℂ$
86		elbl3	$⊢ ((abs \circ - \in ∞Met (ℂ) \land y \in ℝ^{*}) \land (B \in ℂ \land z \in ℂ)) \to (z \in (B ball (abs \circ -) y) \leftrightarrow z (abs \circ -) B < y)$
87	79 81 82 85 86	syl22anc	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to (z \in (B ball (abs \circ -) y) \leftrightarrow z (abs \circ -) B < y)$
88		eqid	$⊢ abs \circ - = abs \circ -$
89	88	cnmetdval	$⊢ (z \in ℂ \land B \in ℂ) \to z (abs \circ -) B = \|z - B\|$
90	85 82 89	syl2anc	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to z (abs \circ -) B = \|z - B\|$
91	90	breq1d	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to (z (abs \circ -) B < y \leftrightarrow \|z - B\| < y)$
92	87 91	bitrd	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to (z \in (B ball (abs \circ -) y) \leftrightarrow \|z - B\| < y)$
93		simplrl	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to x \in ℝ^{+}$
94	93	rpxrd	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to x \in ℝ^{*}$
95		simpllr	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to C \in ℂ$
96		eldifi	$⊢ z \in (A ∖ \{B\}) \to z \in A$
97		ffvelcdm	$⊢ (F : A ⟶ ℂ \land z \in A) \to F (z) \in ℂ$
98	70 96 97	syl2an	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to F (z) \in ℂ$
99		elbl3	$⊢ ((abs \circ - \in ∞Met (ℂ) \land x \in ℝ^{*}) \land (C \in ℂ \land F (z) \in ℂ)) \to (F (z) \in (C ball (abs \circ -) x) \leftrightarrow F (z) (abs \circ -) C < x)$
100	79 94 95 98 99	syl22anc	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to (F (z) \in (C ball (abs \circ -) x) \leftrightarrow F (z) (abs \circ -) C < x)$
101	88	cnmetdval	$⊢ (F (z) \in ℂ \land C \in ℂ) \to F (z) (abs \circ -) C = \|F (z) - C\|$
102	98 95 101	syl2anc	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to F (z) (abs \circ -) C = \|F (z) - C\|$
103	102	breq1d	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to (F (z) (abs \circ -) C < x \leftrightarrow \|F (z) - C\| < x)$
104	100 103	bitrd	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to (F (z) \in (C ball (abs \circ -) x) \leftrightarrow \|F (z) - C\| < x)$
105	92 104	imbi12d	$⊢ (((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \land z \in (A ∖ \{B\})) \to ((z \in (B ball (abs \circ -) y) \to F (z) \in (C ball (abs \circ -) x)) \leftrightarrow (\|z - B\| < y \to \|F (z) - C\| < x))$
106	105	ralbidva	$⊢ ((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to (\forall z \in (A ∖ \{B\}) (z \in (B ball (abs \circ -) y) \to F (z) \in (C ball (abs \circ -) x)) \leftrightarrow \forall z \in (A ∖ \{B\}) (\|z - B\| < y \to \|F (z) - C\| < x))$
107		elin	$⊢ z \in ((B ball (abs \circ -) y) \cap (A ∖ \{B\})) \leftrightarrow (z \in (B ball (abs \circ -) y) \land z \in (A ∖ \{B\}))$
108	107	biancomi	$⊢ z \in ((B ball (abs \circ -) y) \cap (A ∖ \{B\})) \leftrightarrow (z \in (A ∖ \{B\}) \land z \in (B ball (abs \circ -) y))$
109	108	imbi1i	$⊢ (z \in ((B ball (abs \circ -) y) \cap (A ∖ \{B\})) \to F (z) \in (C ball (abs \circ -) x)) \leftrightarrow ((z \in (A ∖ \{B\}) \land z \in (B ball (abs \circ -) y)) \to F (z) \in (C ball (abs \circ -) x))$
110		impexp	$⊢ ((z \in (A ∖ \{B\}) \land z \in (B ball (abs \circ -) y)) \to F (z) \in (C ball (abs \circ -) x)) \leftrightarrow (z \in (A ∖ \{B\}) \to (z \in (B ball (abs \circ -) y) \to F (z) \in (C ball (abs \circ -) x)))$
111	109 110	bitr2i	$⊢ (z \in (A ∖ \{B\}) \to (z \in (B ball (abs \circ -) y) \to F (z) \in (C ball (abs \circ -) x))) \leftrightarrow (z \in ((B ball (abs \circ -) y) \cap (A ∖ \{B\})) \to F (z) \in (C ball (abs \circ -) x))$
112	111	ralbii2	$⊢ \forall z \in (A ∖ \{B\}) (z \in (B ball (abs \circ -) y) \to F (z) \in (C ball (abs \circ -) x)) \leftrightarrow \forall z \in ((B ball (abs \circ -) y) \cap (A ∖ \{B\})) F (z) \in (C ball (abs \circ -) x)$
113		impexp	$⊢ ((z \in A \land z \neq B) \to (\|z - B\| < y \to \|F (z) - C\| < x)) \leftrightarrow (z \in A \to (z \neq B \to (\|z - B\| < y \to \|F (z) - C\| < x)))$
114		eldifsn	$⊢ z \in (A ∖ \{B\}) \leftrightarrow (z \in A \land z \neq B)$
115	114	imbi1i	$⊢ (z \in (A ∖ \{B\}) \to (\|z - B\| < y \to \|F (z) - C\| < x)) \leftrightarrow ((z \in A \land z \neq B) \to (\|z - B\| < y \to \|F (z) - C\| < x))$
116		impexp	$⊢ ((z \neq B \land \|z - B\| < y) \to \|F (z) - C\| < x) \leftrightarrow (z \neq B \to (\|z - B\| < y \to \|F (z) - C\| < x))$
117	116	imbi2i	$⊢ (z \in A \to ((z \neq B \land \|z - B\| < y) \to \|F (z) - C\| < x)) \leftrightarrow (z \in A \to (z \neq B \to (\|z - B\| < y \to \|F (z) - C\| < x)))$
118	113 115 117	3bitr4i	$⊢ (z \in (A ∖ \{B\}) \to (\|z - B\| < y \to \|F (z) - C\| < x)) \leftrightarrow (z \in A \to ((z \neq B \land \|z - B\| < y) \to \|F (z) - C\| < x))$
119	118	ralbii2	$⊢ \forall z \in (A ∖ \{B\}) (\|z - B\| < y \to \|F (z) - C\| < x) \leftrightarrow \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - C\| < x)$
120	106 112 119	3bitr3g	$⊢ ((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to (\forall z \in ((B ball (abs \circ -) y) \cap (A ∖ \{B\})) F (z) \in (C ball (abs \circ -) x) \leftrightarrow \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - C\| < x))$
121	78 120	bitrd	$⊢ ((φ \land C \in ℂ) \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to (F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \leftrightarrow \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - C\| < x))$
122	121	anassrs	$⊢ (((φ \land C \in ℂ) \land x \in ℝ^{+}) \land y \in ℝ^{+}) \to (F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \leftrightarrow \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - C\| < x))$
123	122	rexbidva	$⊢ ((φ \land C \in ℂ) \land x \in ℝ^{+}) \to (\exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \leftrightarrow \exists y \in ℝ^{+} \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - C\| < x))$
124	123	ralbidva	$⊢ (φ \land C \in ℂ) \to (\forall x \in ℝ^{+} \exists y \in ℝ^{+} F [(B ball (abs \circ -) y) \cap (A ∖ \{B\})] \subseteq C ball (abs \circ -) x \leftrightarrow \forall x \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - C\| < x))$
125	69 124	bitrd	$⊢ (φ \land C \in ℂ) \to (\forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u)) \leftrightarrow \forall x \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - C\| < x))$
126	125	pm5.32da	$⊢ φ \to ((C \in ℂ \land \forall u \in TopOpen (ℂ_{fld}) (C \in u \to \exists v \in TopOpen (ℂ_{fld}) (B \in v \land F [v \cap (A ∖ \{B\})] \subseteq u))) \leftrightarrow (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - C\| < x)))$
127	5 126	bitrd	$⊢ φ \to (C \in (F {lim}_{ℂ} B) \leftrightarrow (C \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in A ((z \neq B \land \|z - B\| < y) \to \|F (z) - C\| < x)))$

Metamath Proof Explorer

Theorem ellimc3

Proof