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	$$⊢A\in \mathbb{Z}\to -A={inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		zcn	$$⊢A\in \mathbb{Z}\to A\in ℂ$$
2	1	negidd	$$⊢A\in \mathbb{Z}\to A+\left(-A\right)=0$$
3		zringgrp	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Grp}$$
4		id	$$⊢A\in \mathbb{Z}\to A\in \mathbb{Z}$$
5		znegcl	$$⊢A\in \mathbb{Z}\to -A\in \mathbb{Z}$$
6		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
7		zringplusg	$$⊢+={+}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
8		zring0	$$⊢0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$
9		eqid	$$⊢{inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)={inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
10	6 7 8 9	grpinvid1	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Grp}\wedge A\in \mathbb{Z}\wedge -A\in \mathbb{Z}\right)\to \left({inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(A\right)=-A\leftrightarrow A+\left(-A\right)=0\right)$$
11	3 4 5 10	mp3an2i	$$⊢A\in \mathbb{Z}\to \left({inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(A\right)=-A\leftrightarrow A+\left(-A\right)=0\right)$$
12	2 11	mpbird	$$⊢A\in \mathbb{Z}\to {inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(A\right)=-A$$
13	12	eqcomd	$$⊢A\in \mathbb{Z}\to -A={inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(A\right)$$