addlimc

Description: Sum of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	addlimc.f	$⊢ F = (x \in A ⟼ B)$
	addlimc.g	$⊢ G = (x \in A ⟼ C)$
	addlimc.h	$⊢ H = (x \in A ⟼ B + C)$
	addlimc.b	$⊢ (φ \land x \in A) \to B \in ℂ$
	addlimc.c	$⊢ (φ \land x \in A) \to C \in ℂ$
	addlimc.e	$⊢ φ \to E \in (F {lim}_{ℂ} D)$
	addlimc.i	$⊢ φ \to I \in (G {lim}_{ℂ} D)$
Assertion	addlimc	$⊢ φ \to E + I \in (H {lim}_{ℂ} D)$

Proof

Step	Hyp	Ref	Expression
1		addlimc.f	$⊢ F = (x \in A ⟼ B)$
2		addlimc.g	$⊢ G = (x \in A ⟼ C)$
3		addlimc.h	$⊢ H = (x \in A ⟼ B + C)$
4		addlimc.b	$⊢ (φ \land x \in A) \to B \in ℂ$
5		addlimc.c	$⊢ (φ \land x \in A) \to C \in ℂ$
6		addlimc.e	$⊢ φ \to E \in (F {lim}_{ℂ} D)$
7		addlimc.i	$⊢ φ \to I \in (G {lim}_{ℂ} D)$
8		limccl	$⊢ F {lim}_{ℂ} D \subseteq ℂ$
9	8 6	sseldi	$⊢ φ \to E \in ℂ$
10		limccl	$⊢ G {lim}_{ℂ} D \subseteq ℂ$
11	10 7	sseldi	$⊢ φ \to I \in ℂ$
12	9 11	addcld	$⊢ φ \to E + I \in ℂ$
13	4 1	fmptd	$⊢ φ \to F : A ⟶ ℂ$
14	1 4 6	limcmptdm	$⊢ φ \to A \subseteq ℂ$
15		limcrcl	$⊢ E \in (F {lim}_{ℂ} D) \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land D \in ℂ)$
16	6 15	syl	$⊢ φ \to (F : dom F ⟶ ℂ \land dom F \subseteq ℂ \land D \in ℂ)$
17	16	simp3d	$⊢ φ \to D \in ℂ$
18	13 14 17	ellimc3	$⊢ φ \to (E \in (F {lim}_{ℂ} D) \leftrightarrow (E \in ℂ \land \forall z \in ℝ^{+} \exists a \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < z)))$
19	6 18	mpbid	$⊢ φ \to (E \in ℂ \land \forall z \in ℝ^{+} \exists a \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < z))$
20	19	simprd	$⊢ φ \to \forall z \in ℝ^{+} \exists a \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < z)$
21		rphalfcl	$⊢ y \in ℝ^{+} \to \frac{y}{2} \in ℝ^{+}$
22		breq2	$⊢ z = \frac{y}{2} \to (\|F (v) - E\| < z \leftrightarrow \|F (v) - E\| < \frac{y}{2})$
23	22	imbi2d	$⊢ z = \frac{y}{2} \to (((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < z) \leftrightarrow ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}))$
24	23	rexralbidv	$⊢ z = \frac{y}{2} \to (\exists a \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < z) \leftrightarrow \exists a \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}))$
25	24	rspccva	$⊢ (\forall z \in ℝ^{+} \exists a \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < z) \land \frac{y}{2} \in ℝ^{+}) \to \exists a \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2})$
26	20 21 25	syl2an	$⊢ (φ \land y \in ℝ^{+}) \to \exists a \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2})$
27	5 2	fmptd	$⊢ φ \to G : A ⟶ ℂ$
28	27 14 17	ellimc3	$⊢ φ \to (I \in (G {lim}_{ℂ} D) \leftrightarrow (I \in ℂ \land \forall z \in ℝ^{+} \exists b \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < z)))$
29	7 28	mpbid	$⊢ φ \to (I \in ℂ \land \forall z \in ℝ^{+} \exists b \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < z))$
30	29	simprd	$⊢ φ \to \forall z \in ℝ^{+} \exists b \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < z)$
31		breq2	$⊢ z = \frac{y}{2} \to (\|G (v) - I\| < z \leftrightarrow \|G (v) - I\| < \frac{y}{2})$
32	31	imbi2d	$⊢ z = \frac{y}{2} \to (((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < z) \leftrightarrow ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))$
33	32	rexralbidv	$⊢ z = \frac{y}{2} \to (\exists b \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < z) \leftrightarrow \exists b \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))$
34	33	rspccva	$⊢ (\forall z \in ℝ^{+} \exists b \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < z) \land \frac{y}{2} \in ℝ^{+}) \to \exists b \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2})$
35	30 21 34	syl2an	$⊢ (φ \land y \in ℝ^{+}) \to \exists b \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2})$
36		reeanv	$⊢ \exists a \in ℝ^{+} \exists b \in ℝ^{+} (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2})) \leftrightarrow (\exists a \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \exists b \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))$
37	26 35 36	sylanbrc	$⊢ (φ \land y \in ℝ^{+}) \to \exists a \in ℝ^{+} \exists b \in ℝ^{+} (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))$
38		ifcl	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to if (a \leq b, a, b) \in ℝ^{+}$
39	38	3ad2ant2	$⊢ ((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \to if (a \leq b, a, b) \in ℝ^{+}$
40		nfv	$⊢ Ⅎ v (φ \land y \in ℝ^{+})$
41		nfv	$⊢ Ⅎ v (a \in ℝ^{+} \land b \in ℝ^{+})$
42		nfra1	$⊢ Ⅎ v \forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2})$
43		nfra1	$⊢ Ⅎ v \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2})$
44	42 43	nfan	$⊢ Ⅎ v (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))$
45	40 41 44	nf3an	$⊢ Ⅎ v ((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2})))$
46		simp11l	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to φ$
47		simp2	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to v \in A$
48	46 47	jca	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to (φ \land v \in A)$
49		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
50	49	adantl	$⊢ (φ \land y \in ℝ^{+}) \to y \in ℝ$
51	50	3ad2ant1	$⊢ ((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \to y \in ℝ$
52	51	3ad2ant1	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to y \in ℝ$
53		simp13l	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to \forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2})$
54		simp3l	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to v \neq D$
55	14	sselda	$⊢ (φ \land v \in A) \to v \in ℂ$
56	46 47 55	syl2anc	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to v \in ℂ$
57	46 17	syl	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to D \in ℂ$
58	56 57	subcld	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to v - D \in ℂ$
59	58	abscld	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to \|v - D\| \in ℝ$
60	39	rpred	$⊢ ((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \to if (a \leq b, a, b) \in ℝ$
61	60	3ad2ant1	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to if (a \leq b, a, b) \in ℝ$
62		simpl	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to a \in ℝ^{+}$
63	62	rpred	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to a \in ℝ$
64	63	3ad2ant2	$⊢ ((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \to a \in ℝ$
65	64	3ad2ant1	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to a \in ℝ$
66		simp3r	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to \|v - D\| < if (a \leq b, a, b)$
67		simpr	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to b \in ℝ^{+}$
68	67	rpred	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to b \in ℝ$
69		min1	$⊢ (a \in ℝ \land b \in ℝ) \to if (a \leq b, a, b) \leq a$
70	63 68 69	syl2anc	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to if (a \leq b, a, b) \leq a$
71	70	3ad2ant2	$⊢ ((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \to if (a \leq b, a, b) \leq a$
72	71	3ad2ant1	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to if (a \leq b, a, b) \leq a$
73	59 61 65 66 72	ltletrd	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to \|v - D\| < a$
74	54 73	jca	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to (v \neq D \land \|v - D\| < a)$
75		rsp	$⊢ \forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \to (v \in A \to ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}))$
76	53 47 74 75	syl3c	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to \|F (v) - E\| < \frac{y}{2}$
77	48 52 76	jca31	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to (((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2})$
78		simp13r	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2})$
79	68	3ad2ant2	$⊢ ((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \to b \in ℝ$
80	79	3ad2ant1	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to b \in ℝ$
81		min2	$⊢ (a \in ℝ \land b \in ℝ) \to if (a \leq b, a, b) \leq b$
82	63 68 81	syl2anc	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to if (a \leq b, a, b) \leq b$
83	82	3ad2ant2	$⊢ ((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \to if (a \leq b, a, b) \leq b$
84	83	3ad2ant1	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to if (a \leq b, a, b) \leq b$
85	59 61 80 66 84	ltletrd	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to \|v - D\| < b$
86	54 85	jca	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to (v \neq D \land \|v - D\| < b)$
87		rsp	$⊢ \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}) \to (v \in A \to ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))$
88	78 47 86 87	syl3c	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to \|G (v) - I\| < \frac{y}{2}$
89	4 5	addcld	$⊢ (φ \land x \in A) \to B + C \in ℂ$
90	89 3	fmptd	$⊢ φ \to H : A ⟶ ℂ$
91	90	ffvelrnda	$⊢ (φ \land v \in A) \to H (v) \in ℂ$
92	91	ad3antrrr	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to H (v) \in ℂ$
93		simp-4l	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to φ$
94	93 12	syl	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to E + I \in ℂ$
95	92 94	subcld	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to H (v) - (E + I) \in ℂ$
96	95	abscld	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to \|H (v) - (E + I)\| \in ℝ$
97	13	ffvelrnda	$⊢ (φ \land v \in A) \to F (v) \in ℂ$
98	97	ad3antrrr	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to F (v) \in ℂ$
99	93 9	syl	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to E \in ℂ$
100	98 99	subcld	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to F (v) - E \in ℂ$
101	100	abscld	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to \|F (v) - E\| \in ℝ$
102	27	ffvelrnda	$⊢ (φ \land v \in A) \to G (v) \in ℂ$
103	102	ad3antrrr	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to G (v) \in ℂ$
104	93 11	syl	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to I \in ℂ$
105	103 104	subcld	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to G (v) - I \in ℂ$
106	105	abscld	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to \|G (v) - I\| \in ℝ$
107	101 106	readdcld	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to \|F (v) - E\| + \|G (v) - I\| \in ℝ$
108		simpllr	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to y \in ℝ$
109		nfv	$⊢ Ⅎ x (φ \land v \in A)$
110		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B + C)$
111	3 110	nfcxfr	$⊢ \underline{Ⅎ} x H$
112		nfcv	$⊢ \underline{Ⅎ} x v$
113	111 112	nffv	$⊢ \underline{Ⅎ} x H (v)$
114		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
115	1 114	nfcxfr	$⊢ \underline{Ⅎ} x F$
116	115 112	nffv	$⊢ \underline{Ⅎ} x F (v)$
117		nfcv	$⊢ \underline{Ⅎ} x +$
118		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ C)$
119	2 118	nfcxfr	$⊢ \underline{Ⅎ} x G$
120	119 112	nffv	$⊢ \underline{Ⅎ} x G (v)$
121	116 117 120	nfov	$⊢ \underline{Ⅎ} x (F (v) + G (v))$
122	113 121	nfeq	$⊢ Ⅎ x H (v) = F (v) + G (v)$
123	109 122	nfim	$⊢ Ⅎ x ((φ \land v \in A) \to H (v) = F (v) + G (v))$
124		eleq1w	$⊢ x = v \to (x \in A \leftrightarrow v \in A)$
125	124	anbi2d	$⊢ x = v \to ((φ \land x \in A) \leftrightarrow (φ \land v \in A))$
126		fveq2	$⊢ x = v \to H (x) = H (v)$
127		fveq2	$⊢ x = v \to F (x) = F (v)$
128		fveq2	$⊢ x = v \to G (x) = G (v)$
129	127 128	oveq12d	$⊢ x = v \to F (x) + G (x) = F (v) + G (v)$
130	126 129	eqeq12d	$⊢ x = v \to (H (x) = F (x) + G (x) \leftrightarrow H (v) = F (v) + G (v))$
131	125 130	imbi12d	$⊢ x = v \to (((φ \land x \in A) \to H (x) = F (x) + G (x)) \leftrightarrow ((φ \land v \in A) \to H (v) = F (v) + G (v)))$
132		simpr	$⊢ (φ \land x \in A) \to x \in A$
133	3	fvmpt2	$⊢ (x \in A \land B + C \in ℂ) \to H (x) = B + C$
134	132 89 133	syl2anc	$⊢ (φ \land x \in A) \to H (x) = B + C$
135	1	fvmpt2	$⊢ (x \in A \land B \in ℂ) \to F (x) = B$
136	132 4 135	syl2anc	$⊢ (φ \land x \in A) \to F (x) = B$
137	136	eqcomd	$⊢ (φ \land x \in A) \to B = F (x)$
138	2	fvmpt2	$⊢ (x \in A \land C \in ℂ) \to G (x) = C$
139	132 5 138	syl2anc	$⊢ (φ \land x \in A) \to G (x) = C$
140	139	eqcomd	$⊢ (φ \land x \in A) \to C = G (x)$
141	137 140	oveq12d	$⊢ (φ \land x \in A) \to B + C = F (x) + G (x)$
142	134 141	eqtrd	$⊢ (φ \land x \in A) \to H (x) = F (x) + G (x)$
143	123 131 142	chvarfv	$⊢ (φ \land v \in A) \to H (v) = F (v) + G (v)$
144	143	ad3antrrr	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to H (v) = F (v) + G (v)$
145	144	oveq1d	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to H (v) - (E + I) = F (v) + G (v) - (E + I)$
146	98 103 99 104	addsub4d	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to F (v) + G (v) - (E + I) = (F (v) - E) + G (v) - I$
147	145 146	eqtrd	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to H (v) - (E + I) = (F (v) - E) + G (v) - I$
148	147	fveq2d	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to \|H (v) - (E + I)\| = \|(F (v) - E) + G (v) - I\|$
149	100 105	abstrid	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to \|(F (v) - E) + G (v) - I\| \leq \|F (v) - E\| + \|G (v) - I\|$
150	148 149	eqbrtrd	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to \|H (v) - (E + I)\| \leq \|F (v) - E\| + \|G (v) - I\|$
151		simplr	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to \|F (v) - E\| < \frac{y}{2}$
152		simpr	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to \|G (v) - I\| < \frac{y}{2}$
153	101 106 108 151 152	lt2halvesd	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to \|F (v) - E\| + \|G (v) - I\| < y$
154	96 107 108 150 153	lelttrd	$⊢ ((((φ \land v \in A) \land y \in ℝ) \land \|F (v) - E\| < \frac{y}{2}) \land \|G (v) - I\| < \frac{y}{2}) \to \|H (v) - (E + I)\| < y$
155	77 88 154	syl2anc	$⊢ (((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \land v \in A \land (v \neq D \land \|v - D\| < if (a \leq b, a, b))) \to \|H (v) - (E + I)\| < y$
156	155	3exp	$⊢ ((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \to (v \in A \to ((v \neq D \land \|v - D\| < if (a \leq b, a, b)) \to \|H (v) - (E + I)\| < y))$
157	45 156	ralrimi	$⊢ ((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \to \forall v \in A ((v \neq D \land \|v - D\| < if (a \leq b, a, b)) \to \|H (v) - (E + I)\| < y)$
158		brimralrspcev	$⊢ (if (a \leq b, a, b) \in ℝ^{+} \land \forall v \in A ((v \neq D \land \|v - D\| < if (a \leq b, a, b)) \to \|H (v) - (E + I)\| < y)) \to \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|H (v) - (E + I)\| < y)$
159	39 157 158	syl2anc	$⊢ ((φ \land y \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in ℝ^{+}) \land (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2}))) \to \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|H (v) - (E + I)\| < y)$
160	159	3exp	$⊢ (φ \land y \in ℝ^{+}) \to ((a \in ℝ^{+} \land b \in ℝ^{+}) \to ((\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2})) \to \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|H (v) - (E + I)\| < y)))$
161	160	rexlimdvv	$⊢ (φ \land y \in ℝ^{+}) \to (\exists a \in ℝ^{+} \exists b \in ℝ^{+} (\forall v \in A ((v \neq D \land \|v - D\| < a) \to \|F (v) - E\| < \frac{y}{2}) \land \forall v \in A ((v \neq D \land \|v - D\| < b) \to \|G (v) - I\| < \frac{y}{2})) \to \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|H (v) - (E + I)\| < y))$
162	37 161	mpd	$⊢ (φ \land y \in ℝ^{+}) \to \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|H (v) - (E + I)\| < y)$
163	162	ralrimiva	$⊢ φ \to \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|H (v) - (E + I)\| < y)$
164	90 14 17	ellimc3	$⊢ φ \to (E + I \in (H {lim}_{ℂ} D) \leftrightarrow (E + I \in ℂ \land \forall y \in ℝ^{+} \exists w \in ℝ^{+} \forall v \in A ((v \neq D \land \|v - D\| < w) \to \|H (v) - (E + I)\| < y)))$
165	12 163 164	mpbir2and	$⊢ φ \to E + I \in (H {lim}_{ℂ} D)$

Metamath Proof Explorer

Theorem addlimc

Proof