subcn2

Description: Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of Gleason p. 243. (Contributed by Mario Carneiro, 31-Jan-2014)

		Ref	Expression
	Assertion	subcn2	$⊢ (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		negcl	$⊢ C \in ℂ \to - C \in ℂ$
2		addcn2	$⊢ (A \in ℝ^{+} \land B \in ℂ \land - C \in ℂ) \to \exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall w \in ℂ ((\|u - B\| < y \land \|w - (- C)\| < z) \to \|u + w - (B + (- C))\| < A)$
3	1 2	syl3an3	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall w \in ℂ ((\|u - B\| < y \land \|w - (- C)\| < z) \to \|u + w - (B + (- C))\| < A)$
4		negcl	$⊢ v \in ℂ \to - v \in ℂ$
5		fvoveq1	$⊢ w = - v \to \|w - (- C)\| = \|- v - (- C)\|$
6	5	breq1d	$⊢ w = - v \to (\|w - (- C)\| < z \leftrightarrow \|- v - (- C)\| < z)$
7	6	anbi2d	$⊢ w = - v \to ((\|u - B\| < y \land \|w - (- C)\| < z) \leftrightarrow (\|u - B\| < y \land \|- v - (- C)\| < z))$
8		oveq2	$⊢ w = - v \to u + w = u + (- v)$
9	8	fvoveq1d	$⊢ w = - v \to \|u + w - (B + (- C))\| = \|u + (- v) - (B + (- C))\|$
10	9	breq1d	$⊢ w = - v \to (\|u + w - (B + (- C))\| < A \leftrightarrow \|u + (- v) - (B + (- C))\| < A)$
11	7 10	imbi12d	$⊢ w = - v \to (((\|u - B\| < y \land \|w - (- C)\| < z) \to \|u + w - (B + (- C))\| < A) \leftrightarrow ((\|u - B\| < y \land \|- v - (- C)\| < z) \to \|u + (- v) - (B + (- C))\| < A))$
12	11	rspcv	$⊢ - v \in ℂ \to (\forall w \in ℂ ((\|u - B\| < y \land \|w - (- C)\| < z) \to \|u + w - (B + (- C))\| < A) \to ((\|u - B\| < y \land \|- v - (- C)\| < z) \to \|u + (- v) - (B + (- C))\| < A))$
13	4 12	syl	$⊢ v \in ℂ \to (\forall w \in ℂ ((\|u - B\| < y \land \|w - (- C)\| < z) \to \|u + w - (B + (- C))\| < A) \to ((\|u - B\| < y \land \|- v - (- C)\| < z) \to \|u + (- v) - (B + (- C))\| < A))$
14	13	adantl	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to (\forall w \in ℂ ((\|u - B\| < y \land \|w - (- C)\| < z) \to \|u + w - (B + (- C))\| < A) \to ((\|u - B\| < y \land \|- v - (- C)\| < z) \to \|u + (- v) - (B + (- C))\| < A))$
15		simpr	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to v \in ℂ$
16		simpll3	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to C \in ℂ$
17	15 16	neg2subd	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to - v - (- C) = C - v$
18	17	fveq2d	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to \|- v - (- C)\| = \|C - v\|$
19	16 15	abssubd	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to \|C - v\| = \|v - C\|$
20	18 19	eqtrd	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to \|- v - (- C)\| = \|v - C\|$
21	20	breq1d	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to (\|- v - (- C)\| < z \leftrightarrow \|v - C\| < z)$
22	21	anbi2d	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to ((\|u - B\| < y \land \|- v - (- C)\| < z) \leftrightarrow (\|u - B\| < y \land \|v - C\| < z))$
23		negsub	$⊢ (u \in ℂ \land v \in ℂ) \to u + (- v) = u - v$
24	23	adantll	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to u + (- v) = u - v$
25		simpll2	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to B \in ℂ$
26	25 16	negsubd	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to B + (- C) = B - C$
27	24 26	oveq12d	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to u + (- v) - (B + (- C)) = u - v - (B - C)$
28	27	fveq2d	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to \|u + (- v) - (B + (- C))\| = \|u - v - (B - C)\|$
29	28	breq1d	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to (\|u + (- v) - (B + (- C))\| < A \leftrightarrow \|u - v - (B - C)\| < A)$
30	22 29	imbi12d	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to (((\|u - B\| < y \land \|- v - (- C)\| < z) \to \|u + (- v) - (B + (- C))\| < A) \leftrightarrow ((\|u - B\| < y \land \|v - C\| < z) \to \|u - v - (B - C)\| < A))$
31	14 30	sylibd	$⊢ (((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \land v \in ℂ) \to (\forall w \in ℂ ((\|u - B\| < y \land \|w - (- C)\| < z) \to \|u + w - (B + (- C))\| < A) \to ((\|u - B\| < y \land \|v - C\| < z) \to \|u - v - (B - C)\| < A))$
32	31	ralrimdva	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land u \in ℂ) \to (\forall w \in ℂ ((\|u - B\| < y \land \|w - (- C)\| < z) \to \|u + w - (B + (- C))\| < A) \to \forall v \in ℂ ((\|u - B\| < y \land \|v - C\| < z) \to \|u - v - (B - C)\| < A))$
33	32	ralimdva	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to (\forall u \in ℂ \forall w \in ℂ ((\|u - B\| < y \land \|w - (- C)\| < z) \to \|u + w - (B + (- C))\| < A) \to \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < y \land \|v - C\| < z) \to \|u - v - (B - C)\| < A))$
34	33	reximdv	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to (\exists z \in ℝ^{+} \forall u \in ℂ \forall w \in ℂ ((\|u - B\| < y \land \|w - (- C)\| < z) \to \|u + w - (B + (- C))\| < A) \to \exists z \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < y \land \|v - C\| < z) \to \|u - v - (B - C)\| < A))$
35	34	reximdv	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to (\exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall w \in ℂ ((\|u - B\| < y \land \|w - (- C)\| < z) \to \|u + w - (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))$
36	3 35	mpd	$⊢ (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 subcn2

Proof