Metamath Proof Explorer

Theorem nnpw2evenALTV

Description: 2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020) (Revised by AV, 20-Jun-2020)

Ref Expression
Assertion nnpw2evenALTV 
|- ( N e. NN -> ( 2 ^ N ) e. Even )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
3 zexpcl 
 |-  ( ( 2 e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) e. ZZ )
4 1 2 3 sylancr 
 |-  ( N e. NN -> ( 2 ^ N ) e. ZZ )
5 iddvdsexp 
 |-  ( ( 2 e. ZZ /\ N e. NN ) -> 2 || ( 2 ^ N ) )
6 1 5 mpan 
 |-  ( N e. NN -> 2 || ( 2 ^ N ) )
7 iseven2 
 |-  ( ( 2 ^ N ) e. Even <-> ( ( 2 ^ N ) e. ZZ /\ 2 || ( 2 ^ N ) ) )
8 4 6 7 sylanbrc 
 |-  ( N e. NN -> ( 2 ^ N ) e. Even )