Theorem nvcl

Description: The norm of a normed complex vector space is a real number. (Contributed by NM, 24-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvf.1	|- X = ( BaseSet ` U )
	nvf.6	|- N = ( normCV ` U )
Assertion	nvcl	|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		nvf.1	|- X = ( BaseSet ` U )
2		nvf.6	|- N = ( normCV ` U )
3	1 2	nvf	|- ( U e. NrmCVec -> N : X --> RR )
4	3	ffvelrnda	|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. RR )