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 𝐽 = ( TopOpen ‘ ℂfld )
Assertion subcn − ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )

Proof

Step Hyp Ref Expression
1 addcn.j 𝐽 = ( TopOpen ‘ ℂfld )
2 subf − : ( ℂ × ℂ ) ⟶ ℂ
3 subcn2 ( ( 𝑎 ∈ ℝ+𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ∃ 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢𝑏 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣𝑐 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢𝑣 ) − ( 𝑏𝑐 ) ) ) < 𝑎 ) )
4 1 2 3 addcnlem − ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )