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 ` CCfld )
Assertion subcn
|- - e. ( ( J tX J ) Cn J )

Proof

Step Hyp Ref Expression
1 addcn.j
 |-  J = ( TopOpen ` CCfld )
2 subf
 |-  - : ( CC X. CC ) --> CC
3 subcn2
 |-  ( ( a e. RR+ /\ b e. CC /\ c e. CC ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - b ) ) < y /\ ( abs ` ( v - c ) ) < z ) -> ( abs ` ( ( u - v ) - ( b - c ) ) ) < a ) )
4 1 2 3 addcnlem
 |-  - e. ( ( J tX J ) Cn J )