Description: The absolute value function on complex numbers is continuous. (Contributed by NM, 22-Aug-2007) (Proof shortened by Mario Carneiro, 10-Jan-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | abscn.3 | |- J = ( TopOpen ` CCfld ) |
|
| abscn.4 | |- K = ( topGen ` ran (,) ) |
||
| Assertion | abscn | |- abs e. ( J Cn K ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abscn.3 | |- J = ( TopOpen ` CCfld ) |
|
| 2 | abscn.4 | |- K = ( topGen ` ran (,) ) |
|
| 3 | cnngp | |- CCfld e. NrmGrp |
|
| 4 | cnfldnm | |- abs = ( norm ` CCfld ) |
|
| 5 | 4 1 2 | nmcn | |- ( CCfld e. NrmGrp -> abs e. ( J Cn K ) ) |
| 6 | 3 5 | ax-mp | |- abs e. ( J Cn K ) |