Theorem nn0enne

Description: A positive integer is an even nonnegative integer iff it is an even positive integer. (Contributed by AV, 30-May-2020)

	Ref	Expression
Assertion	nn0enne	|- ( N e. NN -> ( ( N / 2 ) e. NN0 <-> ( N / 2 ) e. NN ) )

Proof

Step	Hyp	Ref	Expression
1		elnn0	|- ( ( N / 2 ) e. NN0 <-> ( ( N / 2 ) e. NN \/ ( N / 2 ) = 0 ) )
2		nncn	|- ( N e. NN -> N e. CC )
3		2cnd	|- ( N e. NN -> 2 e. CC )
4		2ne0	|- 2 =/= 0
5	4	a1i	|- ( N e. NN -> 2 =/= 0 )
6	2 3 5	diveq0ad	|- ( N e. NN -> ( ( N / 2 ) = 0 <-> N = 0 ) )
7		eleq1	|- ( N = 0 -> ( N e. NN <-> 0 e. NN ) )
8		0nnn	|- -. 0 e. NN
9	8	pm2.21i	|- ( 0 e. NN -> ( N / 2 ) e. NN )
10	7 9	biimtrdi	|- ( N = 0 -> ( N e. NN -> ( N / 2 ) e. NN ) )
11	10	com12	|- ( N e. NN -> ( N = 0 -> ( N / 2 ) e. NN ) )
12	6 11	sylbid	|- ( N e. NN -> ( ( N / 2 ) = 0 -> ( N / 2 ) e. NN ) )
13	12	com12	|- ( ( N / 2 ) = 0 -> ( N e. NN -> ( N / 2 ) e. NN ) )
14	13	jao1i	|- ( ( ( N / 2 ) e. NN \/ ( N / 2 ) = 0 ) -> ( N e. NN -> ( N / 2 ) e. NN ) )
15	1 14	sylbi	|- ( ( N / 2 ) e. NN0 -> ( N e. NN -> ( N / 2 ) e. NN ) )
16	15	com12	|- ( N e. NN -> ( ( N / 2 ) e. NN0 -> ( N / 2 ) e. NN ) )
17		nnnn0	|- ( ( N / 2 ) e. NN -> ( N / 2 ) e. NN0 )
18	16 17	impbid1	|- ( N e. NN -> ( ( N / 2 ) e. NN0 <-> ( N / 2 ) e. NN ) )