Metamath Proof Explorer


Theorem zringinvg

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 AA=invgringA

Proof

Step Hyp Ref Expression
1 zcn AA
2 1 negidd AA+A=0
3 zringgrp ringGrp
4 id AA
5 znegcl AA
6 zringbas =Basering
7 zringplusg +=+ring
8 zring0 0=0ring
9 eqid invgring=invgring
10 6 7 8 9 grpinvid1 ringGrpAAinvgringA=AA+A=0
11 3 4 5 10 mp3an2i AinvgringA=AA+A=0
12 2 11 mpbird AinvgringA=A
13 12 eqcomd AA=invgringA