Metamath Proof Explorer

Theorem normne0

Description: A norm is nonzero iff its argument is a nonzero vector. (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion normne0 
|- ( A e. ~H -> ( ( normh ` A ) =/= 0 <-> A =/= 0h ) )

Proof

Step Hyp Ref Expression
1 norm-i 
 |-  ( A e. ~H -> ( ( normh ` A ) = 0 <-> A = 0h ) )
2 1 necon3bid 
 |-  ( A e. ~H -> ( ( normh ` A ) =/= 0 <-> A =/= 0h ) )