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 AnormA0A0

Proof

Step Hyp Ref Expression
1 norm-i AnormA=0A=0
2 1 necon3bid AnormA0A0