Theorem zringsub

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

	Ref	Expression
Hypothesis	zringsub.p	|- .- = ( -g ` ZZring )
Assertion	zringsub	|- ( ( X e. ZZ /\ Y e. ZZ ) -> ( X .- Y ) = ( X - Y ) )

Proof

Step	Hyp	Ref	Expression
1		zringsub.p	|- .- = ( -g ` ZZring )
2		zcn	|- ( x e. ZZ -> x e. CC )
3		zaddcl	|- ( ( x e. ZZ /\ y e. ZZ ) -> ( x + y ) e. ZZ )
4		znegcl	|- ( x e. ZZ -> -u x e. ZZ )
5		0z	|- 0 e. ZZ
6	2 3 4 5	cnsubglem	|- ZZ e. ( SubGrp ` CCfld )
7		cnfldsub	|- - = ( -g ` CCfld )
8		df-zring	|- ZZring = ( CCfld |`s ZZ )
9	7 8 1	subgsub	|- ( ( ZZ e. ( SubGrp ` CCfld ) /\ X e. ZZ /\ Y e. ZZ ) -> ( X - Y ) = ( X .- Y ) )
10	6 9	mp3an1	|- ( ( X e. ZZ /\ Y e. ZZ ) -> ( X - Y ) = ( X .- Y ) )
11	10	eqcomd	|- ( ( X e. ZZ /\ Y e. ZZ ) -> ( X .- Y ) = ( X - Y ) )