Theorem zsubcl

Description: Closure of subtraction of integers. (Contributed by NM, 11-May-2004)

	Ref	Expression
Assertion	zsubcl	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M - N ) e. ZZ )

Proof

Step	Hyp	Ref	Expression
1		zcn	|- ( M e. ZZ -> M e. CC )
2		zcn	|- ( N e. ZZ -> N e. CC )
3		negsub	|- ( ( M e. CC /\ N e. CC ) -> ( M + -u N ) = ( M - N ) )
4	1 2 3	syl2an	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M + -u N ) = ( M - N ) )
5		znegcl	|- ( N e. ZZ -> -u N e. ZZ )
6		zaddcl	|- ( ( M e. ZZ /\ -u N e. ZZ ) -> ( M + -u N ) e. ZZ )
7	5 6	sylan2	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M + -u N ) e. ZZ )
8	4 7	eqeltrrd	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M - N ) e. ZZ )