Theorem nneom

Description: A positive integer is even or odd. (Contributed by AV, 30-May-2020)

	Ref	Expression
Assertion	nneom	|- ( N e. NN -> ( ( N / 2 ) e. NN \/ ( ( N - 1 ) / 2 ) e. NN0 ) )

Proof

Step	Hyp	Ref	Expression
1		nneop	|- ( N e. NN -> ( ( N / 2 ) e. NN \/ ( ( N + 1 ) / 2 ) e. NN ) )
2		nnnn0	|- ( N e. NN -> N e. NN0 )
3		nnnn0	|- ( ( ( N + 1 ) / 2 ) e. NN -> ( ( N + 1 ) / 2 ) e. NN0 )
4		nn0o	|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN0 )
5	2 3 4	syl2an	|- ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. NN ) -> ( ( N - 1 ) / 2 ) e. NN0 )
6	5	ex	|- ( N e. NN -> ( ( ( N + 1 ) / 2 ) e. NN -> ( ( N - 1 ) / 2 ) e. NN0 ) )
7	6	orim2d	|- ( N e. NN -> ( ( ( N / 2 ) e. NN \/ ( ( N + 1 ) / 2 ) e. NN ) -> ( ( N / 2 ) e. NN \/ ( ( N - 1 ) / 2 ) e. NN0 ) ) )
8	1 7	mpd	|- ( N e. NN -> ( ( N / 2 ) e. NN \/ ( ( N - 1 ) / 2 ) e. NN0 ) )