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

Metamath Proof Explorer

Theorem addcn

Description: Complex number addition is a continuous function. Part of Proposition 14-4.16 of Gleason p. 243. (Contributed by NM, 30-Jul-2007) (Proof shortened by Mario Carneiro, 5-May-2014)

Ref Expression
Hypothesis addcn.j ⊢ J = TopOpen ⁡ ℂ fld
Assertion addcn ⊢ + ∈ J × t J Cn J

Proof

Step Hyp Ref Expression
1 addcn.j ⊢ J = TopOpen ⁡ ℂ fld
2 ax-addf ⊢ + : ℂ × ℂ ⟶ ℂ
3 addcn2 ⊢ a ∈ ℝ + ∧ b ∈ ℂ ∧ c ∈ ℂ → ∃ y ∈ ℝ + ∃ z ∈ ℝ + ∀ u ∈ ℂ ∀ v ∈ ℂ u − b < y ∧ v − c < z → u + v - b + c < a
4 1 2 3 addcnlem ⊢ + ∈ J × t J Cn J