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 e. ZZ -> ( N + 2 ) e. ZZ )

Proof

Step Hyp Ref Expression
1 id
 |-  ( N e. ZZ -> N e. ZZ )
2 2z
 |-  2 e. ZZ
3 2 a1i
 |-  ( N e. ZZ -> 2 e. ZZ )
4 1 3 zaddcld
 |-  ( N e. ZZ -> ( N + 2 ) e. ZZ )