Theorem nvgt0

Description: A nonzero norm is positive. (Contributed by NM, 20-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvgt0.1	|- X = ( BaseSet ` U )
	nvgt0.5	|- Z = ( 0vec ` U )
	nvgt0.6	|- N = ( normCV ` U )
Assertion	nvgt0	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A =/= Z <-> 0 < ( N ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		nvgt0.1	|- X = ( BaseSet ` U )
2		nvgt0.5	|- Z = ( 0vec ` U )
3		nvgt0.6	|- N = ( normCV ` U )
4	1 2 3	nvz	|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( N ` A ) = 0 <-> A = Z ) )
5	4	necon3bid	|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( N ` A ) =/= 0 <-> A =/= Z ) )
6	1 3	nvcl	|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) e. RR )
7	1 3	nvge0	|- ( ( U e. NrmCVec /\ A e. X ) -> 0 <_ ( N ` A ) )
8		ne0gt0	|- ( ( ( N ` A ) e. RR /\ 0 <_ ( N ` A ) ) -> ( ( N ` A ) =/= 0 <-> 0 < ( N ` A ) ) )
9	6 7 8	syl2anc	|- ( ( U e. NrmCVec /\ A e. X ) -> ( ( N ` A ) =/= 0 <-> 0 < ( N ` A ) ) )
10	5 9	bitr3d	|- ( ( U e. NrmCVec /\ A e. X ) -> ( A =/= Z <-> 0 < ( N ` A ) ) )