Theorem nvcli

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

	Ref	Expression
Hypotheses	nvf.1	|- X = ( BaseSet ` U )
	nvf.6	|- N = ( normCV ` U )
	nvcli.9	|- U e. NrmCVec
	nvcli.7	|- A e. X
Assertion	nvcli	|- ( N ` A ) e. RR

Proof

Step	Hyp	Ref	Expression
1		nvf.1	|- X = ( BaseSet ` U )
2		nvf.6	|- N = ( normCV ` U )
3		nvcli.9	|- U e. NrmCVec
4		nvcli.7	|- A e. X
5	1 2	nvcl	|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. RR )
6	3 4 5	mp2an	|- ( N ` A ) e. RR