Metamath Proof Explorer


Theorem abscn

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 )

Proof

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 )