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

Metamath Proof Explorer

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 ) ) )