Description: Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of Gleason p. 243. (Contributed by NM, 30-Jul-2007) (Proof shortened by Mario Carneiro, 5-May-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | addcn.j | |- J = ( TopOpen ` CCfld ) |
|
| Assertion | mulcn | |- x. e. ( ( J tX J ) Cn J ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | addcn.j | |- J = ( TopOpen ` CCfld ) |
|
| 2 | ax-mulf | |- x. : ( CC X. CC ) --> CC |
|
| 3 | mulcn2 | |- ( ( 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 x. v ) - ( b x. c ) ) ) < a ) ) |
|
| 4 | 1 2 3 | addcnlem | |- x. e. ( ( J tX J ) Cn J ) |