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