Description: The norm of one in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nm1.n | ||
nm1.u | |||
Assertion | nm1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nm1.n | ||
2 | nm1.u | ||
3 | eqid | ||
4 | 1 3 | nrgabv | |
5 | eqid | ||
6 | 2 5 | nzrnz | |
7 | 3 2 5 | abv1z | |
8 | 4 6 7 | syl2an |