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 ) |
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 ) |