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

Metamath Proof Explorer

Theorem subcn

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

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

Proof

Step Hyp Ref Expression
1 addcn.j ⊢ J = TopOpen ⁡ ℂ fld
2 subf ⊢ − : ℂ × ℂ ⟶ ℂ
3 subcn2 ⊢ 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