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 = 0 vec ⁡ U
nvgt0.6 ⊢ N = norm CV ⁡ U
Assertion nvgt0 ⊢ U ∈ NrmCVec ∧ A ∈ X → A ≠ Z ↔ 0 < N ⁡ A

Proof

Step Hyp Ref Expression
1 nvgt0.1 ⊢ X = BaseSet ⁡ U
2 nvgt0.5 ⊢ Z = 0 vec ⁡ U
3 nvgt0.6 ⊢ N = norm CV ⁡ U
4 1 2 3 nvz ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A = 0 ↔ A = Z
5 4 necon3bid ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A ≠ 0 ↔ A ≠ Z
6 1 3 nvcl ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A ∈ ℝ
7 1 3 nvge0 ⊢ U ∈ NrmCVec ∧ A ∈ X → 0 ≤ N ⁡ A
8 ne0gt0 ⊢ N ⁡ A ∈ ℝ ∧ 0 ≤ N ⁡ A → N ⁡ A ≠ 0 ↔ 0 < N ⁡ A
9 6 7 8 syl2anc ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A ≠ 0 ↔ 0 < N ⁡ A
10 5 9 bitr3d ⊢ U ∈ NrmCVec ∧ A ∈ X → A ≠ Z ↔ 0 < N ⁡ A