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=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	abscn.4	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
Assertion	abscn	$$⊢\mathrm{abs}\in \left(J\mathrm{Cn}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		abscn.3	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		abscn.4	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
3		cnngp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{NrmGrp}$$
4		cnfldnm	$$⊢\mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$$
5	4 1 2	nmcn	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{NrmGrp}\to \mathrm{abs}\in \left(J\mathrm{Cn}K\right)$$
6	3 5	ax-mp	$$⊢\mathrm{abs}\in \left(J\mathrm{Cn}K\right)$$