Theorem 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	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 − 𝑣 ) − ( 𝐵 − 𝐶 ) ) ) < 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		negcl	⊢ ( 𝐶 ∈ ℂ → - 𝐶 ∈ ℂ )
2		addcn2	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ - 𝐶 ∈ ℂ ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑤 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑤 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑤 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) )
3	1 2	syl3an3	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑤 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑤 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑤 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) )
4		negcl	⊢ ( 𝑣 ∈ ℂ → - 𝑣 ∈ ℂ )
5		fvoveq1	⊢ ( 𝑤 = - 𝑣 → ( abs ‘ ( 𝑤 − - 𝐶 ) ) = ( abs ‘ ( - 𝑣 − - 𝐶 ) ) )
6	5	breq1d	⊢ ( 𝑤 = - 𝑣 → ( ( abs ‘ ( 𝑤 − - 𝐶 ) ) < 𝑧 ↔ ( abs ‘ ( - 𝑣 − - 𝐶 ) ) < 𝑧 ) )
7	6	anbi2d	⊢ ( 𝑤 = - 𝑣 → ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑤 − - 𝐶 ) ) < 𝑧 ) ↔ ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( - 𝑣 − - 𝐶 ) ) < 𝑧 ) ) )
8		oveq2	⊢ ( 𝑤 = - 𝑣 → ( 𝑢 + 𝑤 ) = ( 𝑢 + - 𝑣 ) )
9	8	fvoveq1d	⊢ ( 𝑤 = - 𝑣 → ( abs ‘ ( ( 𝑢 + 𝑤 ) − ( 𝐵 + - 𝐶 ) ) ) = ( abs ‘ ( ( 𝑢 + - 𝑣 ) − ( 𝐵 + - 𝐶 ) ) ) )
10	9	breq1d	⊢ ( 𝑤 = - 𝑣 → ( ( abs ‘ ( ( 𝑢 + 𝑤 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ↔ ( abs ‘ ( ( 𝑢 + - 𝑣 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) )
11	7 10	imbi12d	⊢ ( 𝑤 = - 𝑣 → ( ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑤 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑤 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) ↔ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( - 𝑣 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + - 𝑣 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) ) )
12	11	rspcv	⊢ ( - 𝑣 ∈ ℂ → ( ∀ 𝑤 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑤 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑤 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) → ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( - 𝑣 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + - 𝑣 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) ) )
13	4 12	syl	⊢ ( 𝑣 ∈ ℂ → ( ∀ 𝑤 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑤 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑤 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) → ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( - 𝑣 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + - 𝑣 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) ) )
14	13	adantl	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( ∀ 𝑤 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑤 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑤 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) → ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( - 𝑣 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + - 𝑣 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) ) )
15		simpr	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → 𝑣 ∈ ℂ )
16		simpll3	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → 𝐶 ∈ ℂ )
17	15 16	neg2subd	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( - 𝑣 − - 𝐶 ) = ( 𝐶 − 𝑣 ) )
18	17	fveq2d	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( abs ‘ ( - 𝑣 − - 𝐶 ) ) = ( abs ‘ ( 𝐶 − 𝑣 ) ) )
19	16 15	abssubd	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( abs ‘ ( 𝐶 − 𝑣 ) ) = ( abs ‘ ( 𝑣 − 𝐶 ) ) )
20	18 19	eqtrd	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( abs ‘ ( - 𝑣 − - 𝐶 ) ) = ( abs ‘ ( 𝑣 − 𝐶 ) ) )
21	20	breq1d	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( ( abs ‘ ( - 𝑣 − - 𝐶 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) )
22	21	anbi2d	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( - 𝑣 − - 𝐶 ) ) < 𝑧 ) ↔ ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) ) )
23		negsub	⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑢 + - 𝑣 ) = ( 𝑢 − 𝑣 ) )
24	23	adantll	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( 𝑢 + - 𝑣 ) = ( 𝑢 − 𝑣 ) )
25		simpll2	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → 𝐵 ∈ ℂ )
26	25 16	negsubd	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( 𝐵 + - 𝐶 ) = ( 𝐵 − 𝐶 ) )
27	24 26	oveq12d	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( ( 𝑢 + - 𝑣 ) − ( 𝐵 + - 𝐶 ) ) = ( ( 𝑢 − 𝑣 ) − ( 𝐵 − 𝐶 ) ) )
28	27	fveq2d	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( abs ‘ ( ( 𝑢 + - 𝑣 ) − ( 𝐵 + - 𝐶 ) ) ) = ( abs ‘ ( ( 𝑢 − 𝑣 ) − ( 𝐵 − 𝐶 ) ) ) )
29	28	breq1d	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( ( abs ‘ ( ( 𝑢 + - 𝑣 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ↔ ( abs ‘ ( ( 𝑢 − 𝑣 ) − ( 𝐵 − 𝐶 ) ) ) < 𝐴 ) )
30	22 29	imbi12d	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( - 𝑣 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + - 𝑣 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) ↔ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 − 𝑣 ) − ( 𝐵 − 𝐶 ) ) ) < 𝐴 ) ) )
31	14 30	sylibd	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) ∧ 𝑣 ∈ ℂ ) → ( ∀ 𝑤 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑤 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑤 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) → ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 − 𝑣 ) − ( 𝐵 − 𝐶 ) ) ) < 𝐴 ) ) )
32	31	ralrimdva	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ ℂ ) → ( ∀ 𝑤 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑤 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑤 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) → ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 − 𝑣 ) − ( 𝐵 − 𝐶 ) ) ) < 𝐴 ) ) )
33	32	ralimdva	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ∀ 𝑢 ∈ ℂ ∀ 𝑤 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑤 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑤 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) → ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 − 𝑣 ) − ( 𝐵 − 𝐶 ) ) ) < 𝐴 ) ) )
34	33	reximdv	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑤 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑤 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑤 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 − 𝑣 ) − ( 𝐵 − 𝐶 ) ) ) < 𝐴 ) ) )
35	34	reximdv	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑤 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑤 − - 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑤 ) − ( 𝐵 + - 𝐶 ) ) ) < 𝐴 ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 − 𝑣 ) − ( 𝐵 − 𝐶 ) ) ) < 𝐴 ) ) )
36	3 35	mpd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 − 𝑣 ) − ( 𝐵 − 𝐶 ) ) ) < 𝐴 ) )