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 ∈ ℤ → N + 2 ∈ ℤ

Proof

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