mullimc

Description: Limit of the product of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	mullimc.f	$⊢ F = (x \in A ⟼ B)$
	mullimc.g	$⊢ G = (x \in A ⟼ C)$
	mullimc.h	$⊢ H = (x \in A ⟼ B C)$
	mullimc.b	$⊢ (φ \land x \in A) \to B \in ℂ$
	mullimc.c	$⊢ (φ \land x \in A) \to C \in ℂ$
	mullimc.x	$⊢ φ \to X \in (F {lim}_{ℂ} D)$
	mullimc.y	$⊢ φ \to Y \in (G {lim}_{ℂ} D)$
Assertion	mullimc	$⊢ φ \to X Y \in (H {lim}_{ℂ} D)$

Proof

Step	Hyp	Ref	Expression
1		mullimc.f	$⊢ F = (x \in A ⟼ B)$
2		mullimc.g	$⊢ G = (x \in A ⟼ C)$
3		mullimc.h	$⊢ H = (x \in A ⟼ B C)$
4		mullimc.b	$⊢ (φ \land x \in A) \to B \in ℂ$
5		mullimc.c	$⊢ (φ \land x \in A) \to C \in ℂ$
6		mullimc.x	$⊢ φ \to X \in (F {lim}_{ℂ} D)$
7		mullimc.y	$⊢ φ \to Y \in (G {lim}_{ℂ} D)$
8		limccl	$⊢ F {lim}_{ℂ} D \subseteq ℂ$
9	8 6	sseldi	$⊢ φ \to X \in ℂ$
10		limccl	$⊢ G {lim}_{ℂ} D \subseteq ℂ$
11	10 7	sseldi	$⊢ φ \to Y \in ℂ$
12	9 11	mulcld	$⊢ φ \to X Y \in ℂ$
13		simpr	$⊢ (φ \land w \in ℝ^{+}) \to w \in ℝ^{+}$
14	9	adantr	$⊢ (φ \land w \in ℝ^{+}) \to X \in ℂ$
15	11	adantr	$⊢ (φ \land w \in ℝ^{+}) \to Y \in ℂ$
16		mulcn2	$⊢ (w \in ℝ^{+} \land X \in ℂ \land Y \in ℂ) \to \exists a \in ℝ^{+} \exists b \in ℝ^{+} \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)$
17	13 14 15 16	syl3anc	$⊢ (φ \land w \in ℝ^{+}) \to \exists a \in ℝ^{+} \exists b \in ℝ^{+} \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)$
18	4 1	fmptd	$⊢ φ \to F : A ⟶ ℂ$
19	1 4	dmmptd	$⊢ φ \to dom F = A$
20		limcrcl	$⊢ X \in (F {lim}_{ℂ} D) \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land D \in ℂ)$
21	6 20	syl	$⊢ φ \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land D \in ℂ)$
22	21	simp2d	$⊢ φ \to dom F \subseteq ℂ$
23	19 22	eqsstrrd	$⊢ φ \to A \subseteq ℂ$
24	21	simp3d	$⊢ φ \to D \in ℂ$
25	18 23 24	ellimc3	$⊢ φ \to (X \in (F {lim}_{ℂ} D) \leftrightarrow (X \in ℂ \land \forall a \in ℝ^{+} \exists e \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)))$
26	6 25	mpbid	$⊢ φ \to (X \in ℂ \land \forall a \in ℝ^{+} \exists e \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a))$
27	26	simprd	$⊢ φ \to \forall a \in ℝ^{+} \exists e \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)$
28	27	r19.21bi	$⊢ (φ \land a \in ℝ^{+}) \to \exists e \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)$
29	28	adantrr	$⊢ (φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \to \exists e \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)$
30	5 2	fmptd	$⊢ φ \to G : A ⟶ ℂ$
31	30 23 24	ellimc3	$⊢ φ \to (Y \in (G {lim}_{ℂ} D) \leftrightarrow (Y \in ℂ \land \forall b \in ℝ^{+} \exists f \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)))$
32	7 31	mpbid	$⊢ φ \to (Y \in ℂ \land \forall b \in ℝ^{+} \exists f \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))$
33	32	simprd	$⊢ φ \to \forall b \in ℝ^{+} \exists f \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)$
34	33	r19.21bi	$⊢ (φ \land b \in ℝ^{+}) \to \exists f \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)$
35	34	adantrl	$⊢ (φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \to \exists f \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)$
36		reeanv	$⊢ \exists e \in ℝ^{+} \exists f \in ℝ^{+} (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)) \leftrightarrow (\exists e \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \exists f \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))$
37	29 35 36	sylanbrc	$⊢ (φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \to \exists e \in ℝ^{+} \exists f \in ℝ^{+} (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))$
38		ifcl	$⊢ (e \in ℝ^{+} \land f \in ℝ^{+}) \to if (e \leq f, e, f) \in ℝ^{+}$
39	38	3ad2ant2	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \to if (e \leq f, e, f) \in ℝ^{+}$
40		nfv	$⊢ Ⅎ z (φ \land (a \in ℝ^{+} \land b \in ℝ^{+}))$
41		nfv	$⊢ Ⅎ z (e \in ℝ^{+} \land f \in ℝ^{+})$
42		nfra1	$⊢ Ⅎ z \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)$
43		nfra1	$⊢ Ⅎ z \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)$
44	42 43	nfan	$⊢ Ⅎ z (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))$
45	40 41 44	nf3an	$⊢ Ⅎ z ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)))$
46		simp11l	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to φ$
47		simp1rl	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \to a \in ℝ^{+}$
48	47	3ad2ant1	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to a \in ℝ^{+}$
49	46 48	jca	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to (φ \land a \in ℝ^{+})$
50		simp12	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to (e \in ℝ^{+} \land f \in ℝ^{+})$
51		simp13l	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)$
52	49 50 51	jca31	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to (((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a))$
53		simp1r	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)$
54		simp2	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to z \in A$
55		simp3l	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to z \neq D$
56		simplll	$⊢ (((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)) \to φ$
57	56	3ad2ant1	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to φ$
58		simp1lr	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to (e \in ℝ^{+} \land f \in ℝ^{+})$
59		simp3r	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|z - D\| < if (e \leq f, e, f)$
60		simp1l	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to φ$
61		simp2	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to z \in A$
62	23	sselda	$⊢ (φ \land z \in A) \to z \in ℂ$
63	60 61 62	syl2anc	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to z \in ℂ$
64	60 24	syl	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to D \in ℂ$
65	63 64	subcld	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to z - D \in ℂ$
66	65	abscld	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to \|z - D\| \in ℝ$
67		rpre	$⊢ e \in ℝ^{+} \to e \in ℝ$
68	67	ad2antrl	$⊢ (φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \to e \in ℝ$
69	68	3ad2ant1	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to e \in ℝ$
70		rpre	$⊢ f \in ℝ^{+} \to f \in ℝ$
71	70	ad2antll	$⊢ (φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \to f \in ℝ$
72	71	3ad2ant1	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to f \in ℝ$
73	69 72	ifcld	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to if (e \leq f, e, f) \in ℝ$
74		simp3	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to \|z - D\| < if (e \leq f, e, f)$
75		min1	$⊢ (e \in ℝ \land f \in ℝ) \to if (e \leq f, e, f) \leq e$
76	69 72 75	syl2anc	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to if (e \leq f, e, f) \leq e$
77	66 73 69 74 76	ltletrd	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to \|z - D\| < e$
78	57 58 54 59 77	syl211anc	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|z - D\| < e$
79	55 78	jca	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to (z \neq D \land \|z - D\| < e)$
80		rsp	$⊢ \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \to (z \in A \to ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a))$
81	53 54 79 80	syl3c	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|F (z) - X\| < a$
82	52 81	syld3an1	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|F (z) - X\| < a$
83		simp1l	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \to φ$
84	83 47	jca	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \to (φ \land a \in ℝ^{+})$
85		simp2	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \to (e \in ℝ^{+} \land f \in ℝ^{+})$
86		simp3r	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \to \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)$
87	84 85 86	jca31	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \to (((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))$
88		simp1r	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)$
89		simp2	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to z \in A$
90		simp3l	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to z \neq D$
91		simplll	$⊢ (((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)) \to φ$
92	91	3ad2ant1	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to φ$
93		simp1lr	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to (e \in ℝ^{+} \land f \in ℝ^{+})$
94		simp3r	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|z - D\| < if (e \leq f, e, f)$
95		min2	$⊢ (e \in ℝ \land f \in ℝ) \to if (e \leq f, e, f) \leq f$
96	69 72 95	syl2anc	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to if (e \leq f, e, f) \leq f$
97	66 73 72 74 96	ltletrd	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to \|z - D\| < f$
98	92 93 89 94 97	syl211anc	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|z - D\| < f$
99	90 98	jca	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to (z \neq D \land \|z - D\| < f)$
100		rsp	$⊢ \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b) \to (z \in A \to ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))$
101	88 89 99 100	syl3c	$⊢ ((((φ \land a \in ℝ^{+}) \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|G (z) - Y\| < b$
102	87 101	syl3an1	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|G (z) - Y\| < b$
103	82 102	jca	$⊢ (((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b)$
104	103	3exp	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \to (z \in A \to ((z \neq D \land \|z - D\| < if (e \leq f, e, f)) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b)))$
105	45 104	ralrimi	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \to \forall z \in A ((z \neq D \land \|z - D\| < if (e \leq f, e, f)) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))$
106		brimralrspcev	$⊢ (if (e \leq f, e, f) \in ℝ^{+} \land \forall z \in A ((z \neq D \land \|z - D\| < if (e \leq f, e, f)) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))$
107	39 105 106	syl2anc	$⊢ ((φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \land (e \in ℝ^{+} \land f \in ℝ^{+}) \land (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b))) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))$
108	107	3exp	$⊢ (φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \to ((e \in ℝ^{+} \land f \in ℝ^{+}) \to ((\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))))$
109	108	rexlimdvv	$⊢ (φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \to (\exists e \in ℝ^{+} \exists f \in ℝ^{+} (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - X\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - Y\| < b)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b)))$
110	37 109	mpd	$⊢ (φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))$
111	110	adantlr	$⊢ ((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+})) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))$
112	111	3adant3	$⊢ ((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))$
113		nfv	$⊢ Ⅎ z (((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+})$
114		nfra1	$⊢ Ⅎ z \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))$
115	113 114	nfan	$⊢ Ⅎ z ((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b)))$
116		simp1l	$⊢ ((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \to φ$
117	116	ad2antrr	$⊢ ((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))) \to φ$
118	117	3ad2ant1	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to φ$
119		simp2	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to z \in A$
120		nfv	$⊢ Ⅎ x (φ \land z \in A)$
121		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B C)$
122	3 121	nfcxfr	$⊢ \underline{Ⅎ} x H$
123		nfcv	$⊢ \underline{Ⅎ} x z$
124	122 123	nffv	$⊢ \underline{Ⅎ} x H (z)$
125		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
126	1 125	nfcxfr	$⊢ \underline{Ⅎ} x F$
127	126 123	nffv	$⊢ \underline{Ⅎ} x F (z)$
128		nfcv	$⊢ \underline{Ⅎ} x \times$
129		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ C)$
130	2 129	nfcxfr	$⊢ \underline{Ⅎ} x G$
131	130 123	nffv	$⊢ \underline{Ⅎ} x G (z)$
132	127 128 131	nfov	$⊢ \underline{Ⅎ} x F (z) G (z)$
133	124 132	nfeq	$⊢ Ⅎ x H (z) = F (z) G (z)$
134	120 133	nfim	$⊢ Ⅎ x ((φ \land z \in A) \to H (z) = F (z) G (z))$
135		eleq1w	$⊢ x = z \to (x \in A \leftrightarrow z \in A)$
136	135	anbi2d	$⊢ x = z \to ((φ \land x \in A) \leftrightarrow (φ \land z \in A))$
137		fveq2	$⊢ x = z \to H (x) = H (z)$
138		fveq2	$⊢ x = z \to F (x) = F (z)$
139		fveq2	$⊢ x = z \to G (x) = G (z)$
140	138 139	oveq12d	$⊢ x = z \to F (x) G (x) = F (z) G (z)$
141	137 140	eqeq12d	$⊢ x = z \to (H (x) = F (x) G (x) \leftrightarrow H (z) = F (z) G (z))$
142	136 141	imbi12d	$⊢ x = z \to (((φ \land x \in A) \to H (x) = F (x) G (x)) \leftrightarrow ((φ \land z \in A) \to H (z) = F (z) G (z)))$
143		simpr	$⊢ (φ \land x \in A) \to x \in A$
144	4 5	mulcld	$⊢ (φ \land x \in A) \to B C \in ℂ$
145	3	fvmpt2	$⊢ (x \in A \land B C \in ℂ) \to H (x) = B C$
146	143 144 145	syl2anc	$⊢ (φ \land x \in A) \to H (x) = B C$
147	1	fvmpt2	$⊢ (x \in A \land B \in ℂ) \to F (x) = B$
148	143 4 147	syl2anc	$⊢ (φ \land x \in A) \to F (x) = B$
149	148	eqcomd	$⊢ (φ \land x \in A) \to B = F (x)$
150	2	fvmpt2	$⊢ (x \in A \land C \in ℂ) \to G (x) = C$
151	143 5 150	syl2anc	$⊢ (φ \land x \in A) \to G (x) = C$
152	151	eqcomd	$⊢ (φ \land x \in A) \to C = G (x)$
153	149 152	oveq12d	$⊢ (φ \land x \in A) \to B C = F (x) G (x)$
154	146 153	eqtrd	$⊢ (φ \land x \in A) \to H (x) = F (x) G (x)$
155	134 142 154	chvarfv	$⊢ (φ \land z \in A) \to H (z) = F (z) G (z)$
156	155	fvoveq1d	$⊢ (φ \land z \in A) \to \|H (z) - X Y\| = \|F (z) G (z) - X Y\|$
157	118 119 156	syl2anc	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to \|H (z) - X Y\| = \|F (z) G (z) - X Y\|$
158	18	ffvelrnda	$⊢ (φ \land z \in A) \to F (z) \in ℂ$
159	30	ffvelrnda	$⊢ (φ \land z \in A) \to G (z) \in ℂ$
160	158 159	jca	$⊢ (φ \land z \in A) \to (F (z) \in ℂ \land G (z) \in ℂ)$
161	118 119 160	syl2anc	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to (F (z) \in ℂ \land G (z) \in ℂ)$
162		simpll3	$⊢ ((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))) \to \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)$
163	162	3ad2ant1	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)$
164		rsp	$⊢ \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b)) \to (z \in A \to ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b)))$
165	164	3imp	$⊢ (\forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b)$
166	165	3adant1l	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b)$
167		fvoveq1	$⊢ c = F (z) \to \|c - X\| = \|F (z) - X\|$
168	167	breq1d	$⊢ c = F (z) \to (\|c - X\| < a \leftrightarrow \|F (z) - X\| < a)$
169	168	anbi1d	$⊢ c = F (z) \to ((\|c - X\| < a \land \|d - Y\| < b) \leftrightarrow (\|F (z) - X\| < a \land \|d - Y\| < b))$
170		oveq1	$⊢ c = F (z) \to c d = F (z) d$
171	170	fvoveq1d	$⊢ c = F (z) \to \|c d - X Y\| = \|F (z) d - X Y\|$
172	171	breq1d	$⊢ c = F (z) \to (\|c d - X Y\| < w \leftrightarrow \|F (z) d - X Y\| < w)$
173	169 172	imbi12d	$⊢ c = F (z) \to (((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w) \leftrightarrow ((\|F (z) - X\| < a \land \|d - Y\| < b) \to \|F (z) d - X Y\| < w))$
174		fvoveq1	$⊢ d = G (z) \to \|d - Y\| = \|G (z) - Y\|$
175	174	breq1d	$⊢ d = G (z) \to (\|d - Y\| < b \leftrightarrow \|G (z) - Y\| < b)$
176	175	anbi2d	$⊢ d = G (z) \to ((\|F (z) - X\| < a \land \|d - Y\| < b) \leftrightarrow (\|F (z) - X\| < a \land \|G (z) - Y\| < b))$
177		oveq2	$⊢ d = G (z) \to F (z) d = F (z) G (z)$
178	177	fvoveq1d	$⊢ d = G (z) \to \|F (z) d - X Y\| = \|F (z) G (z) - X Y\|$
179	178	breq1d	$⊢ d = G (z) \to (\|F (z) d - X Y\| < w \leftrightarrow \|F (z) G (z) - X Y\| < w)$
180	176 179	imbi12d	$⊢ d = G (z) \to (((\|F (z) - X\| < a \land \|d - Y\| < b) \to \|F (z) d - X Y\| < w) \leftrightarrow ((\|F (z) - X\| < a \land \|G (z) - Y\| < b) \to \|F (z) G (z) - X Y\| < w))$
181	173 180	rspc2v	$⊢ (F (z) \in ℂ \land G (z) \in ℂ) \to (\forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w) \to ((\|F (z) - X\| < a \land \|G (z) - Y\| < b) \to \|F (z) G (z) - X Y\| < w))$
182	161 163 166 181	syl3c	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to \|F (z) G (z) - X Y\| < w$
183	157 182	eqbrtrd	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to \|H (z) - X Y\| < w$
184	183	3exp	$⊢ ((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))) \to (z \in A \to ((z \neq D \land \|z - D\| < y) \to \|H (z) - X Y\| < w))$
185	115 184	ralrimi	$⊢ ((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b))) \to \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - X Y\| < w)$
186	185	ex	$⊢ (((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \land y \in ℝ^{+}) \to (\forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b)) \to \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - X Y\| < w))$
187	186	reximdva	$⊢ ((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \to (\exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - X\| < a \land \|G (z) - Y\| < b)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - X Y\| < w))$
188	112 187	mpd	$⊢ ((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - X Y\| < w)$
189	188	3exp	$⊢ (φ \land w \in ℝ^{+}) \to ((a \in ℝ^{+} \land b \in ℝ^{+}) \to (\forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - X Y\| < w)))$
190	189	rexlimdvv	$⊢ (φ \land w \in ℝ^{+}) \to (\exists a \in ℝ^{+} \exists b \in ℝ^{+} \forall c \in ℂ \forall d \in ℂ ((\|c - X\| < a \land \|d - Y\| < b) \to \|c d - X Y\| < w) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - X Y\| < w))$
191	17 190	mpd	$⊢ (φ \land w \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - X Y\| < w)$
192	191	ralrimiva	$⊢ φ \to \forall w \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - X Y\| < w)$
193	144 3	fmptd	$⊢ φ \to H : A ⟶ ℂ$
194	193 23 24	ellimc3	$⊢ φ \to (X Y \in (H {lim}_{ℂ} D) \leftrightarrow (X Y \in ℂ \land \forall w \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - X Y\| < w)))$
195	12 192 194	mpbir2and	$⊢ φ \to X Y \in (H {lim}_{ℂ} D)$

Metamath Proof Explorer

Theorem mullimc

Proof