Theorem zringsub

Description: The subtraction of elements in the ring of integers. (Contributed by AV, 24-Mar-2025)

	Ref	Expression
Hypothesis	zringsub.p	$$⊢\underset{\dot{}}{-}={-}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
Assertion	zringsub	$$⊢\left(X\in \mathbb{Z}\wedge Y\in \mathbb{Z}\right)\to X\underset{\dot{}}{-}Y=X-Y$$

Proof

Step	Hyp	Ref	Expression
1		zringsub.p	$$⊢\underset{\dot{}}{-}={-}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
2		zcn	$$⊢x\in \mathbb{Z}\to x\in ℂ$$
3		zaddcl	$$⊢\left(x\in \mathbb{Z}\wedge y\in \mathbb{Z}\right)\to x+y\in \mathbb{Z}$$
4		znegcl	$$⊢x\in \mathbb{Z}\to -x\in \mathbb{Z}$$
5		0z	$$⊢0\in \mathbb{Z}$$
6	2 3 4 5	cnsubglem	$$⊢\mathbb{Z}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
7		cnfldsub	$$⊢-={-}_{{ℂ}_{\mathrm{fld}}}$$
8		df-zring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
9	7 8 1	subgsub	$$⊢\left(\mathbb{Z}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge X\in \mathbb{Z}\wedge Y\in \mathbb{Z}\right)\to X-Y=X\underset{\dot{}}{-}Y$$
10	6 9	mp3an1	$$⊢\left(X\in \mathbb{Z}\wedge Y\in \mathbb{Z}\right)\to X-Y=X\underset{\dot{}}{-}Y$$
11	10	eqcomd	$$⊢\left(X\in \mathbb{Z}\wedge Y\in \mathbb{Z}\right)\to X\underset{\dot{}}{-}Y=X-Y$$