Metamath Proof Explorer

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	$⊢ N \in ℤ \to N + 2 \in ℤ$

Step	Hyp	Ref	Expression
1		id	$⊢ N \in ℤ \to N \in ℤ$
2		2z	$⊢ 2 \in ℤ$
3	2	a1i	$⊢ N \in ℤ \to 2 \in ℤ$
4	1 3	zaddcld	$⊢ N \in ℤ \to N + 2 \in ℤ$