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