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

Proof

Step	Hyp	Ref	Expression
1		rphalfcl	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 / 2 ) ∈ ℝ+ )
2	1	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 / 2 ) ∈ ℝ+ )
3		simprl	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝑢 ∈ ℂ )
4		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝐵 ∈ ℂ )
5		simprr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝑣 ∈ ℂ )
6	3 4 5	pnpcan2d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝑣 ) ) = ( 𝑢 − 𝐵 ) )
7	6	fveq2d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝑣 ) ) ) = ( abs ‘ ( 𝑢 − 𝐵 ) ) )
8	7	breq1d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝑣 ) ) ) < ( 𝐴 / 2 ) ↔ ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ) )
9		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝐶 ∈ ℂ )
10	4 5 9	pnpcand	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( 𝐵 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) = ( 𝑣 − 𝐶 ) )
11	10	fveq2d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( abs ‘ ( ( 𝐵 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) = ( abs ‘ ( 𝑣 − 𝐶 ) ) )
12	11	breq1d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( abs ‘ ( ( 𝐵 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < ( 𝐴 / 2 ) ↔ ( abs ‘ ( 𝑣 − 𝐶 ) ) < ( 𝐴 / 2 ) ) )
13	8 12	anbi12d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝑣 ) ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( ( 𝐵 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < ( 𝐴 / 2 ) ) ↔ ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < ( 𝐴 / 2 ) ) ) )
14		addcl	⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑢 + 𝑣 ) ∈ ℂ )
15	14	adantl	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( 𝑢 + 𝑣 ) ∈ ℂ )
16	4 9	addcld	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
17	4 5	addcld	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( 𝐵 + 𝑣 ) ∈ ℂ )
18		simpl1	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝐴 ∈ ℝ+ )
19	18	rpred	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → 𝐴 ∈ ℝ )
20		abs3lem	⊢ ( ( ( ( 𝑢 + 𝑣 ) ∈ ℂ ∧ ( 𝐵 + 𝐶 ) ∈ ℂ ) ∧ ( ( 𝐵 + 𝑣 ) ∈ ℂ ∧ 𝐴 ∈ ℝ ) ) → ( ( ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝑣 ) ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( ( 𝐵 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < ( 𝐴 / 2 ) ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) )
21	15 16 17 19 20	syl22anc	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝑣 ) ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( ( 𝐵 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < ( 𝐴 / 2 ) ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) )
22	13 21	sylbird	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) ) → ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < ( 𝐴 / 2 ) ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) )
23	22	ralrimivva	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < ( 𝐴 / 2 ) ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) )
24		breq2	⊢ ( 𝑦 = ( 𝐴 / 2 ) → ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ↔ ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ) )
25	24	anbi1d	⊢ ( 𝑦 = ( 𝐴 / 2 ) → ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) ↔ ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) ) )
26	25	imbi1d	⊢ ( 𝑦 = ( 𝐴 / 2 ) → ( ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) ↔ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) ) )
27	26	2ralbidv	⊢ ( 𝑦 = ( 𝐴 / 2 ) → ( ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) ↔ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) ) )
28		breq2	⊢ ( 𝑧 = ( 𝐴 / 2 ) → ( ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑣 − 𝐶 ) ) < ( 𝐴 / 2 ) ) )
29	28	anbi2d	⊢ ( 𝑧 = ( 𝐴 / 2 ) → ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) ↔ ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < ( 𝐴 / 2 ) ) ) )
30	29	imbi1d	⊢ ( 𝑧 = ( 𝐴 / 2 ) → ( ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) ↔ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < ( 𝐴 / 2 ) ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) ) )
31	30	2ralbidv	⊢ ( 𝑧 = ( 𝐴 / 2 ) → ( ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) ↔ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < ( 𝐴 / 2 ) ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) ) )
32	27 31	rspc2ev	⊢ ( ( ( 𝐴 / 2 ) ∈ ℝ+ ∧ ( 𝐴 / 2 ) ∈ ℝ+ ∧ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < ( 𝐴 / 2 ) ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < ( 𝐴 / 2 ) ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) )
33	2 2 23 32	syl3anc	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) )