Theorem nnpw2even

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

	Ref	Expression
Assertion	nnpw2even	|- ( N e. NN -> ( ( 2 ^ N ) / 2 ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		2cnd	|- ( N e. NN -> 2 e. CC )
2		2ne0	|- 2 =/= 0
3	2	a1i	|- ( N e. NN -> 2 =/= 0 )
4		nnz	|- ( N e. NN -> N e. ZZ )
5	1 3 4	expm1d	|- ( N e. NN -> ( 2 ^ ( N - 1 ) ) = ( ( 2 ^ N ) / 2 ) )
6		2nn	|- 2 e. NN
7	6	a1i	|- ( N e. NN -> 2 e. NN )
8		nnm1nn0	|- ( N e. NN -> ( N - 1 ) e. NN0 )
9	7 8	nnexpcld	|- ( N e. NN -> ( 2 ^ ( N - 1 ) ) e. NN )
10	5 9	eqeltrrd	|- ( N e. NN -> ( ( 2 ^ N ) / 2 ) e. NN )