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 ( 𝑁 ∈ ℤ → ( 𝑁 + 2 ) ∈ ℤ )

Proof

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