Metamath Proof Explorer


Theorem nm1

Description: The norm of one in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses nm1.n N = norm R
nm1.u 1 ˙ = 1 R
Assertion nm1 R NrmRing R NzRing N 1 ˙ = 1

Proof

Step Hyp Ref Expression
1 nm1.n N = norm R
2 nm1.u 1 ˙ = 1 R
3 eqid AbsVal R = AbsVal R
4 1 3 nrgabv R NrmRing N AbsVal R
5 eqid 0 R = 0 R
6 2 5 nzrnz R NzRing 1 ˙ 0 R
7 3 2 5 abv1z N AbsVal R 1 ˙ 0 R N 1 ˙ = 1
8 4 6 7 syl2an R NrmRing R NzRing N 1 ˙ = 1