Theorem nmcl

Description: The norm of a normed group is closed in the reals. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	nmf.x	|- X = ( Base ` G )
	nmf.n	|- N = ( norm ` G )
Assertion	nmcl	|- ( ( G e. NrmGrp /\ A e. X ) -> ( N ` A ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		nmf.x	|- X = ( Base ` G )
2		nmf.n	|- N = ( norm ` G )
3	1 2	nmf	|- ( G e. NrmGrp -> N : X --> RR )
4	3	ffvelcdmda	|- ( ( G e. NrmGrp /\ A e. X ) -> ( N ` A ) e. RR )