zsubcl

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

		Ref	Expression
	Assertion	zsubcl	$⊢ (M \in ℤ \land N \in ℤ) \to M - N \in ℤ$

Step	Hyp	Ref	Expression
1		zcn	$⊢ M \in ℤ \to M \in ℂ$
2		zcn	$⊢ N \in ℤ \to N \in ℂ$
3		negsub	$⊢ (M \in ℂ \land N \in ℂ) \to M + -N = M - N$
4	1 2 3	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to M + -N = M - N$
5		znegcl	$⊢ N \in ℤ \to - N \in ℤ$
6		zaddcl	$⊢ (M \in ℤ \land - N \in ℤ) \to M + -N \in ℤ$
7	5 6	sylan2	$⊢ (M \in ℤ \land N \in ℤ) \to M + -N \in ℤ$
8	4 7	eqeltrrd	$⊢ (M \in ℤ \land N \in ℤ) \to M - N \in ℤ$

Metamath Proof Explorer