Theorem zadd2cl

Description: Increasing an integer by 2 results in an integer. (Contributed by Alexander van der Vekens, 16-Sep-2018)

	Ref	Expression
Assertion	zadd2cl	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 2 ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℤ )
2		2z	⊢ 2 ∈ ℤ
3	2	a1i	⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℤ )
4	1 3	zaddcld	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 2 ) ∈ ℤ )