zringsub

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

		Ref	Expression
	Hypothesis	zringsub.p	$⊢ \underset{˙}{-} = -_{ℤ_{ring}}$
	Assertion	zringsub	$⊢ (X \in ℤ \land Y \in ℤ) \to X \underset{˙}{-} Y = X - Y$

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

Metamath Proof Explorer