Theorem nn0ehalf

Description: The half of an even nonnegative integer is a nonnegative integer. (Contributed by AV, 22-Jun-2020) (Revised by AV, 28-Jun-2021) (Proof shortened by AV, 10-Jul-2022)

	Ref	Expression
Assertion	nn0ehalf	|- ( ( N e. NN0 /\ 2 || N ) -> ( N / 2 ) e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		nn0z	|- ( N e. NN0 -> N e. ZZ )
2		evend2	|- ( N e. ZZ -> ( 2 || N <-> ( N / 2 ) e. ZZ ) )
3	1 2	syl	|- ( N e. NN0 -> ( 2 || N <-> ( N / 2 ) e. ZZ ) )
4		nn0re	|- ( N e. NN0 -> N e. RR )
5		2rp	|- 2 e. RR+
6	5	a1i	|- ( N e. NN0 -> 2 e. RR+ )
7		nn0ge0	|- ( N e. NN0 -> 0 <_ N )
8	4 6 7	divge0d	|- ( N e. NN0 -> 0 <_ ( N / 2 ) )
9	8	anim1ci	|- ( ( N e. NN0 /\ ( N / 2 ) e. ZZ ) -> ( ( N / 2 ) e. ZZ /\ 0 <_ ( N / 2 ) ) )
10		elnn0z	|- ( ( N / 2 ) e. NN0 <-> ( ( N / 2 ) e. ZZ /\ 0 <_ ( N / 2 ) ) )
11	9 10	sylibr	|- ( ( N e. NN0 /\ ( N / 2 ) e. ZZ ) -> ( N / 2 ) e. NN0 )
12	11	ex	|- ( N e. NN0 -> ( ( N / 2 ) e. ZZ -> ( N / 2 ) e. NN0 ) )
13	3 12	sylbid	|- ( N e. NN0 -> ( 2 || N -> ( N / 2 ) e. NN0 ) )
14	13	imp	|- ( ( N e. NN0 /\ 2 || N ) -> ( N / 2 ) e. NN0 )