Description: The additive inverse of an element of the ring of integers. (Contributed by AV, 24-May-2019) (Revised by AV, 10-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | zringinvg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zcn | |
|
2 | 1 | negidd | |
3 | zringgrp | |
|
4 | id | |
|
5 | znegcl | |
|
6 | zringbas | |
|
7 | zringplusg | |
|
8 | zring0 | |
|
9 | eqid | |
|
10 | 6 7 8 9 | grpinvid1 | |
11 | 3 4 5 10 | mp3an2i | |
12 | 2 11 | mpbird | |
13 | 12 | eqcomd | |