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 )