This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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