mullimcf

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

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

Proof

Step	Hyp	Ref	Expression
1		mullimcf.f	$⊢ φ \to F : A ⟶ ℂ$
2		mullimcf.g	$⊢ φ \to G : A ⟶ ℂ$
3		mullimcf.h	$⊢ H = (x \in A ⟼ F (x) G (x))$
4		mullimcf.b	$⊢ φ \to B \in (F {lim}_{ℂ} D)$
5		mullimcf.c	$⊢ φ \to C \in (G {lim}_{ℂ} D)$
6		limccl	$⊢ F {lim}_{ℂ} D \subseteq ℂ$
7	6 4	sseldi	$⊢ φ \to B \in ℂ$
8		limccl	$⊢ G {lim}_{ℂ} D \subseteq ℂ$
9	8 5	sseldi	$⊢ φ \to C \in ℂ$
10	7 9	mulcld	$⊢ φ \to B C \in ℂ$
11		simpr	$⊢ (φ \land w \in ℝ^{+}) \to w \in ℝ^{+}$
12	7	adantr	$⊢ (φ \land w \in ℝ^{+}) \to B \in ℂ$
13	9	adantr	$⊢ (φ \land w \in ℝ^{+}) \to C \in ℂ$
14		mulcn2	$⊢ (w \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \exists a \in ℝ^{+} \exists b \in ℝ^{+} \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)$
15	11 12 13 14	syl3anc	$⊢ (φ \land w \in ℝ^{+}) \to \exists a \in ℝ^{+} \exists b \in ℝ^{+} \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)$
16	1	fdmd	$⊢ φ \to dom F = A$
17		limcrcl	$⊢ B \in (F {lim}_{ℂ} D) \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land D \in ℂ)$
18	4 17	syl	$⊢ φ \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land D \in ℂ)$
19	18	simp2d	$⊢ φ \to dom F \subseteq ℂ$
20	16 19	eqsstrrd	$⊢ φ \to A \subseteq ℂ$
21	18	simp3d	$⊢ φ \to D \in ℂ$
22	1 20 21	ellimc3	$⊢ φ \to (B \in (F {lim}_{ℂ} D) \leftrightarrow (B \in ℂ \land \forall a \in ℝ^{+} \exists e \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - B\| < a)))$
23	4 22	mpbid	$⊢ φ \to (B \in ℂ \land \forall a \in ℝ^{+} \exists e \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - B\| < a))$
24	23	simprd	$⊢ φ \to \forall a \in ℝ^{+} \exists e \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - B\| < a)$
25	24	r19.21bi	$⊢ (φ \land a \in ℝ^{+}) \to \exists e \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - B\| < a)$
26	25	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) - B\| < a)$
27	2 20 21	ellimc3	$⊢ φ \to (C \in (G {lim}_{ℂ} D) \leftrightarrow (C \in ℂ \land \forall b \in ℝ^{+} \exists f \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b)))$
28	5 27	mpbid	$⊢ φ \to (C \in ℂ \land \forall b \in ℝ^{+} \exists f \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))$
29	28	simprd	$⊢ φ \to \forall b \in ℝ^{+} \exists f \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b)$
30	29	r19.21bi	$⊢ (φ \land b \in ℝ^{+}) \to \exists f \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b)$
31	30	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) - C\| < b)$
32		reeanv	$⊢ \exists e \in ℝ^{+} \exists f \in ℝ^{+} (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b)) \leftrightarrow (\exists e \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - B\| < a) \land \exists f \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))$
33	26 31 32	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))$
34		ifcl	$⊢ (e \in ℝ^{+} \land f \in ℝ^{+}) \to if (e \leq f, e, f) \in ℝ^{+}$
35	34	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \to if (e \leq f, e, f) \in ℝ^{+}$
36		nfv	$⊢ Ⅎ z (φ \land (a \in ℝ^{+} \land b \in ℝ^{+}))$
37		nfv	$⊢ Ⅎ z (e \in ℝ^{+} \land f \in ℝ^{+})$
38		nfra1	$⊢ Ⅎ z \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - B\| < a)$
39		nfra1	$⊢ Ⅎ z \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b)$
40	38 39	nfan	$⊢ Ⅎ z (\forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))$
41	36 37 40	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b)))$
42		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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to φ$
43		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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \to a \in ℝ^{+}$
44	43	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to a \in ℝ^{+}$
45	42 44	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to (φ \land a \in ℝ^{+})$
46		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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to (e \in ℝ^{+} \land f \in ℝ^{+})$
47		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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < 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) - B\| < a)$
48	45 46 47	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < 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) - B\| < a))$
49		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) - B\| < 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) - B\| < a)$
50		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) - B\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to z \in A$
51		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) - B\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to z \neq D$
52		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) - B\| < a)) \to φ$
53	52	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) - B\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to φ$
54		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) - B\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to (e \in ℝ^{+} \land f \in ℝ^{+})$
55		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) - B\| < 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)$
56		simp1l	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to φ$
57		simp2	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to z \in A$
58	20	sselda	$⊢ (φ \land z \in A) \to z \in ℂ$
59	56 57 58	syl2anc	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to z \in ℂ$
60	56 21	syl	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to D \in ℂ$
61	59 60	subcld	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to z - D \in ℂ$
62	61	abscld	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to \|z - D\| \in ℝ$
63		rpre	$⊢ e \in ℝ^{+} \to e \in ℝ$
64	63	ad2antrl	$⊢ (φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \to e \in ℝ$
65	64	3ad2ant1	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to e \in ℝ$
66		rpre	$⊢ f \in ℝ^{+} \to f \in ℝ$
67	66	ad2antll	$⊢ (φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \to f \in ℝ$
68	67	3ad2ant1	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to f \in ℝ$
69	65 68	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 ℝ$
70		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)$
71		min1	$⊢ (e \in ℝ \land f \in ℝ) \to if (e \leq f, e, f) \leq e$
72	65 68 71	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$
73	62 69 65 70 72	ltletrd	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to \|z - D\| < e$
74	53 54 50 55 73	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) - B\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|z - D\| < e$
75	51 74	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) - B\| < 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)$
76		rsp	$⊢ \forall z \in A ((z \neq D \land \|z - D\| < e) \to \|F (z) - B\| < a) \to (z \in A \to ((z \neq D \land \|z - D\| < e) \to \|F (z) - B\| < a))$
77	49 50 75 76	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) - B\| < a)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|F (z) - B\| < a$
78	48 77	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|F (z) - B\| < a$
79		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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \to φ$
80	79 43	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \to (φ \land a \in ℝ^{+})$
81		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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \to (e \in ℝ^{+} \land f \in ℝ^{+})$
82		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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \to \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b)$
83	80 81 82	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < 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) - C\| < b))$
84		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) - C\| < 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) - C\| < b)$
85		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) - C\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to z \in A$
86		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) - C\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to z \neq D$
87		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) - C\| < b)) \to φ$
88	87	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) - C\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to φ$
89		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) - C\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to (e \in ℝ^{+} \land f \in ℝ^{+})$
90		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) - C\| < 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)$
91		min2	$⊢ (e \in ℝ \land f \in ℝ) \to if (e \leq f, e, f) \leq f$
92	65 68 91	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$
93	62 69 68 70 92	ltletrd	$⊢ ((φ \land (e \in ℝ^{+} \land f \in ℝ^{+})) \land z \in A \land \|z - D\| < if (e \leq f, e, f)) \to \|z - D\| < f$
94	88 89 85 90 93	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) - C\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|z - D\| < f$
95	86 94	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) - C\| < 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)$
96		rsp	$⊢ \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b) \to (z \in A \to ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))$
97	84 85 95 96	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) - C\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|G (z) - C\| < b$
98	83 97	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to \|G (z) - C\| < b$
99	78 98	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < if (e \leq f, e, f))) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b)$
100	99	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \to (z \in A \to ((z \neq D \land \|z - D\| < if (e \leq f, e, f)) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b)))$
101	41 100	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \to \forall z \in A ((z \neq D \land \|z - D\| < if (e \leq f, e, f)) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))$
102		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) - B\| < a \land \|G (z) - C\| < b))) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))$
103	35 101 102	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b))) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))$
104	103	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))))$
105	104	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) - B\| < a) \land \forall z \in A ((z \neq D \land \|z - D\| < f) \to \|G (z) - C\| < b)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b)))$
106	33 105	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) - B\| < a \land \|G (z) - C\| < b))$
107	106	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) - B\| < a \land \|G (z) - C\| < b))$
108	107	3adant3	$⊢ ((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))$
109		nfv	$⊢ Ⅎ z (((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+})$
110		nfra1	$⊢ Ⅎ z \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))$
111	109 110	nfan	$⊢ Ⅎ z ((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b)))$
112		simp1l	$⊢ ((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \to φ$
113	112	ad2antrr	$⊢ ((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))) \to φ$
114	113	3ad2ant1	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to φ$
115		simp2	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to z \in A$
116		fveq2	$⊢ x = z \to F (x) = F (z)$
117		fveq2	$⊢ x = z \to G (x) = G (z)$
118	116 117	oveq12d	$⊢ x = z \to F (x) G (x) = F (z) G (z)$
119		simpr	$⊢ (φ \land z \in A) \to z \in A$
120	1	ffvelrnda	$⊢ (φ \land z \in A) \to F (z) \in ℂ$
121	2	ffvelrnda	$⊢ (φ \land z \in A) \to G (z) \in ℂ$
122	120 121	mulcld	$⊢ (φ \land z \in A) \to F (z) G (z) \in ℂ$
123	3 118 119 122	fvmptd3	$⊢ (φ \land z \in A) \to H (z) = F (z) G (z)$
124	123	fvoveq1d	$⊢ (φ \land z \in A) \to \|H (z) - B C\| = \|F (z) G (z) - B C\|$
125	114 115 124	syl2anc	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to \|H (z) - B C\| = \|F (z) G (z) - B C\|$
126	120 121	jca	$⊢ (φ \land z \in A) \to (F (z) \in ℂ \land G (z) \in ℂ)$
127	114 115 126	syl2anc	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to (F (z) \in ℂ \land G (z) \in ℂ)$
128		simpll3	$⊢ ((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))) \to \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)$
129	128	3ad2ant1	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)$
130		rsp	$⊢ \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b)) \to (z \in A \to ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b)))$
131	130	3imp	$⊢ (\forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b)) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b)$
132	131	3adant1l	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b)$
133		fvoveq1	$⊢ c = F (z) \to \|c - B\| = \|F (z) - B\|$
134	133	breq1d	$⊢ c = F (z) \to (\|c - B\| < a \leftrightarrow \|F (z) - B\| < a)$
135	134	anbi1d	$⊢ c = F (z) \to ((\|c - B\| < a \land \|d - C\| < b) \leftrightarrow (\|F (z) - B\| < a \land \|d - C\| < b))$
136		oveq1	$⊢ c = F (z) \to c d = F (z) d$
137	136	fvoveq1d	$⊢ c = F (z) \to \|c d - B C\| = \|F (z) d - B C\|$
138	137	breq1d	$⊢ c = F (z) \to (\|c d - B C\| < w \leftrightarrow \|F (z) d - B C\| < w)$
139	135 138	imbi12d	$⊢ c = F (z) \to (((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w) \leftrightarrow ((\|F (z) - B\| < a \land \|d - C\| < b) \to \|F (z) d - B C\| < w))$
140		fvoveq1	$⊢ d = G (z) \to \|d - C\| = \|G (z) - C\|$
141	140	breq1d	$⊢ d = G (z) \to (\|d - C\| < b \leftrightarrow \|G (z) - C\| < b)$
142	141	anbi2d	$⊢ d = G (z) \to ((\|F (z) - B\| < a \land \|d - C\| < b) \leftrightarrow (\|F (z) - B\| < a \land \|G (z) - C\| < b))$
143		oveq2	$⊢ d = G (z) \to F (z) d = F (z) G (z)$
144	143	fvoveq1d	$⊢ d = G (z) \to \|F (z) d - B C\| = \|F (z) G (z) - B C\|$
145	144	breq1d	$⊢ d = G (z) \to (\|F (z) d - B C\| < w \leftrightarrow \|F (z) G (z) - B C\| < w)$
146	142 145	imbi12d	$⊢ d = G (z) \to (((\|F (z) - B\| < a \land \|d - C\| < b) \to \|F (z) d - B C\| < w) \leftrightarrow ((\|F (z) - B\| < a \land \|G (z) - C\| < b) \to \|F (z) G (z) - B C\| < w))$
147	139 146	rspc2v	$⊢ (F (z) \in ℂ \land G (z) \in ℂ) \to (\forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w) \to ((\|F (z) - B\| < a \land \|G (z) - C\| < b) \to \|F (z) G (z) - B C\| < w))$
148	127 129 132 147	syl3c	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to \|F (z) G (z) - B C\| < w$
149	125 148	eqbrtrd	$⊢ (((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))) \land z \in A \land (z \neq D \land \|z - D\| < y)) \to \|H (z) - B C\| < w$
150	149	3exp	$⊢ ((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))) \to (z \in A \to ((z \neq D \land \|z - D\| < y) \to \|H (z) - B C\| < w))$
151	111 150	ralrimi	$⊢ ((((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \land \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b))) \to \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - B C\| < w)$
152	151	ex	$⊢ (((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \land y \in ℝ^{+}) \to (\forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b)) \to \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - B C\| < w))$
153	152	reximdva	$⊢ ((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \to (\exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to (\|F (z) - B\| < a \land \|G (z) - C\| < b)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - B C\| < w))$
154	108 153	mpd	$⊢ ((φ \land w \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - B C\| < w)$
155	154	3exp	$⊢ (φ \land w \in ℝ^{+}) \to ((a \in ℝ^{+} \land b \in ℝ^{+}) \to (\forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - B C\| < w)))$
156	155	rexlimdvv	$⊢ (φ \land w \in ℝ^{+}) \to (\exists a \in ℝ^{+} \exists b \in ℝ^{+} \forall c \in ℂ \forall d \in ℂ ((\|c - B\| < a \land \|d - C\| < b) \to \|c d - B C\| < w) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - B C\| < w))$
157	15 156	mpd	$⊢ (φ \land w \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - B C\| < w)$
158	157	ralrimiva	$⊢ φ \to \forall w \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - B C\| < w)$
159	1	ffvelrnda	$⊢ (φ \land x \in A) \to F (x) \in ℂ$
160	2	ffvelrnda	$⊢ (φ \land x \in A) \to G (x) \in ℂ$
161	159 160	mulcld	$⊢ (φ \land x \in A) \to F (x) G (x) \in ℂ$
162	161 3	fmptd	$⊢ φ \to H : A ⟶ ℂ$
163	162 20 21	ellimc3	$⊢ φ \to (B C \in (H {lim}_{ℂ} D) \leftrightarrow (B C \in ℂ \land \forall w \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in A ((z \neq D \land \|z - D\| < y) \to \|H (z) - B C\| < w)))$
164	10 158 163	mpbir2and	$⊢ φ \to B C \in (H {lim}_{ℂ} D)$

Metamath Proof Explorer

Theorem mullimcf

Proof