Metamath Proof Explorer


Theorem nmgt0

Description: The norm of a nonzero element is a positive real. (Contributed by NM, 20-Nov-2007) (Revised by AV, 8-Oct-2021)

Ref Expression
Hypotheses nmgt0.x X = Base G
nmgt0.n N = norm G
nmgt0.z 0 ˙ = 0 G
Assertion nmgt0 G NrmGrp A X A 0 ˙ 0 < N A

Proof

Step Hyp Ref Expression
1 nmgt0.x X = Base G
2 nmgt0.n N = norm G
3 nmgt0.z 0 ˙ = 0 G
4 1 2 3 nmeq0 G NrmGrp A X N A = 0 A = 0 ˙
5 4 necon3bid G NrmGrp A X N A 0 A 0 ˙
6 1 2 nmcl G NrmGrp A X N A
7 1 2 nmge0 G NrmGrp A X 0 N A
8 ne0gt0 N A 0 N A N A 0 0 < N A
9 6 7 8 syl2anc G NrmGrp A X N A 0 0 < N A
10 5 9 bitr3d G NrmGrp A X A 0 ˙ 0 < N A