Metamath Proof Explorer

Theorem zsubcl

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

Ref Expression
Assertion zsubcl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M − N ∈ ℤ

Proof

Step Hyp Ref Expression
1 zcn ⊢ M ∈ ℤ → M ∈ ℂ
2 zcn ⊢ N ∈ ℤ → N ∈ ℂ
3 negsub ⊢ M ∈ ℂ ∧ N ∈ ℂ → M + -N = M − N
4 1 2 3 syl2an ⊢ M ∈ ℤ ∧ N ∈ ℤ → M + -N = M − N
5 znegcl ⊢ N ∈ ℤ → − N ∈ ℤ
6 zaddcl ⊢ M ∈ ℤ ∧ − N ∈ ℤ → M + -N ∈ ℤ
7 5 6 sylan2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M + -N ∈ ℤ
8 4 7 eqeltrrd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M − N ∈ ℤ