This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ ( ( 𝑢 + 𝑣 ) − ( 𝐵 + 𝐶 ) ) ) < 𝐴 ) )