addcn2

Description: Complex number addition is a continuous function. Part of Proposition 14-4.16 of Gleason p. 243. (We write out the definition directly because df-cn and df-cncf are not yet available to us. See addcn for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014)

		Ref	Expression
	Assertion	addcn2	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < y \land \|v - C\| < z) \to \|u + v - (B + C)\| < A)$

Proof

Step	Hyp	Ref	Expression
1		rphalfcl	$⊢ A \in ℝ^{+} \to \frac{A}{2} \in ℝ^{+}$
2	1	3ad2ant1	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \frac{A}{2} \in ℝ^{+}$
3		simprl	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to u \in ℂ$
4		simpl2	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to B \in ℂ$
5		simprr	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to v \in ℂ$
6	3 4 5	pnpcan2d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to u + v - (B + v) = u - B$
7	6	fveq2d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|u + v - (B + v)\| = \|u - B\|$
8	7	breq1d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|u + v - (B + v)\| < \frac{A}{2} \leftrightarrow \|u - B\| < \frac{A}{2})$
9		simpl3	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to C \in ℂ$
10	4 5 9	pnpcand	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to B + v - (B + C) = v - C$
11	10	fveq2d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|B + v - (B + C)\| = \|v - C\|$
12	11	breq1d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|B + v - (B + C)\| < \frac{A}{2} \leftrightarrow \|v - C\| < \frac{A}{2})$
13	8 12	anbi12d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|u + v - (B + v)\| < \frac{A}{2} \land \|B + v - (B + C)\| < \frac{A}{2}) \leftrightarrow (\|u - B\| < \frac{A}{2} \land \|v - C\| < \frac{A}{2}))$
14		addcl	$⊢ (u \in ℂ \land v \in ℂ) \to u + v \in ℂ$
15	14	adantl	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to u + v \in ℂ$
16	4 9	addcld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to B + C \in ℂ$
17	4 5	addcld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to B + v \in ℂ$
18		simpl1	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to A \in ℝ^{+}$
19	18	rpred	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to A \in ℝ$
20		abs3lem	$⊢ ((u + v \in ℂ \land B + C \in ℂ) \land (B + v \in ℂ \land A \in ℝ)) \to ((\|u + v - (B + v)\| < \frac{A}{2} \land \|B + v - (B + C)\| < \frac{A}{2}) \to \|u + v - (B + C)\| < A)$
21	15 16 17 19 20	syl22anc	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|u + v - (B + v)\| < \frac{A}{2} \land \|B + v - (B + C)\| < \frac{A}{2}) \to \|u + v - (B + C)\| < A)$
22	13 21	sylbird	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|u - B\| < \frac{A}{2} \land \|v - C\| < \frac{A}{2}) \to \|u + v - (B + C)\| < A)$
23	22	ralrimivva	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < \frac{A}{2} \land \|v - C\| < \frac{A}{2}) \to \|u + v - (B + C)\| < A)$
24		breq2	$⊢ y = \frac{A}{2} \to (\|u - B\| < y \leftrightarrow \|u - B\| < \frac{A}{2})$
25	24	anbi1d	$⊢ y = \frac{A}{2} \to ((\|u - B\| < y \land \|v - C\| < z) \leftrightarrow (\|u - B\| < \frac{A}{2} \land \|v - C\| < z))$
26	25	imbi1d	$⊢ y = \frac{A}{2} \to (((\|u - B\| < y \land \|v - C\| < z) \to \|u + v - (B + C)\| < A) \leftrightarrow ((\|u - B\| < \frac{A}{2} \land \|v - C\| < z) \to \|u + v - (B + C)\| < A))$
27	26	2ralbidv	$⊢ y = \frac{A}{2} \to (\forall u \in ℂ \forall v \in ℂ ((\|u - B\| < y \land \|v - C\| < z) \to \|u + v - (B + C)\| < A) \leftrightarrow \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < \frac{A}{2} \land \|v - C\| < z) \to \|u + v - (B + C)\| < A))$
28		breq2	$⊢ z = \frac{A}{2} \to (\|v - C\| < z \leftrightarrow \|v - C\| < \frac{A}{2})$
29	28	anbi2d	$⊢ z = \frac{A}{2} \to ((\|u - B\| < \frac{A}{2} \land \|v - C\| < z) \leftrightarrow (\|u - B\| < \frac{A}{2} \land \|v - C\| < \frac{A}{2}))$
30	29	imbi1d	$⊢ z = \frac{A}{2} \to (((\|u - B\| < \frac{A}{2} \land \|v - C\| < z) \to \|u + v - (B + C)\| < A) \leftrightarrow ((\|u - B\| < \frac{A}{2} \land \|v - C\| < \frac{A}{2}) \to \|u + v - (B + C)\| < A))$
31	30	2ralbidv	$⊢ z = \frac{A}{2} \to (\forall u \in ℂ \forall v \in ℂ ((\|u - B\| < \frac{A}{2} \land \|v - C\| < z) \to \|u + v - (B + C)\| < A) \leftrightarrow \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < \frac{A}{2} \land \|v - C\| < \frac{A}{2}) \to \|u + v - (B + C)\| < A))$
32	27 31	rspc2ev	$⊢ (\frac{A}{2} \in ℝ^{+} \land \frac{A}{2} \in ℝ^{+} \land \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < \frac{A}{2} \land \|v - C\| < \frac{A}{2}) \to \|u + v - (B + C)\| < A)) \to \exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < y \land \|v - C\| < z) \to \|u + v - (B + C)\| < A)$
33	2 2 23 32	syl3anc	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < y \land \|v - C\| < z) \to \|u + v - (B + C)\| < A)$

Metamath Proof Explorer

Theorem addcn2

Proof