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

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 ∈ ℋ → norm ℎ ⁡ A ≠ 0 ↔ A ≠ 0 ℎ

Proof

Step Hyp Ref Expression
1 norm-i ⊢ A ∈ ℋ → norm ℎ ⁡ A = 0 ↔ A = 0 ℎ
2 1 necon3bid ⊢ A ∈ ℋ → norm ℎ ⁡ A ≠ 0 ↔ A ≠ 0 ℎ