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	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
	abscn.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
Assertion	abscn	⊢ abs ∈ ( 𝐽 Cn 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		abscn.3	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		abscn.4	⊢ 𝐾 = ( topGen ‘ ran (,) )
3		cnngp	⊢ ℂfld ∈ NrmGrp
4		cnfldnm	⊢ abs = ( norm ‘ ℂfld )
5	4 1 2	nmcn	⊢ ( ℂfld ∈ NrmGrp → abs ∈ ( 𝐽 Cn 𝐾 ) )
6	3 5	ax-mp	⊢ abs ∈ ( 𝐽 Cn 𝐾 )