Metamath Proof Explorer

Theorem nn0eo

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

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

Proof

Step Hyp Ref Expression
1 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
2 zeo 
 |-  ( N e. ZZ -> ( ( N / 2 ) e. ZZ \/ ( ( N + 1 ) / 2 ) e. ZZ ) )
3 1 2 syl 
 |-  ( N e. NN0 -> ( ( N / 2 ) e. ZZ \/ ( ( N + 1 ) / 2 ) e. ZZ ) )
4 simpr 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. ZZ ) -> ( N / 2 ) e. ZZ )
5 nn0re 
 |-  ( N e. NN0 -> N e. RR )
6 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
7 2re 
 |-  2 e. RR
8 7 a1i 
 |-  ( N e. NN0 -> 2 e. RR )
9 2pos 
 |-  0 < 2
10 9 a1i 
 |-  ( N e. NN0 -> 0 < 2 )
11 divge0 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( N / 2 ) )
12 5 6 8 10 11 syl22anc 
 |-  ( N e. NN0 -> 0 <_ ( N / 2 ) )
13 12 adantr 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. ZZ ) -> 0 <_ ( N / 2 ) )
14 elnn0z 
 |-  ( ( N / 2 ) e. NN0 <-> ( ( N / 2 ) e. ZZ /\ 0 <_ ( N / 2 ) ) )
15 4 13 14 sylanbrc 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. ZZ ) -> ( N / 2 ) e. NN0 )
16 15 ex 
 |-  ( N e. NN0 -> ( ( N / 2 ) e. ZZ -> ( N / 2 ) e. NN0 ) )
17 simpr 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) / 2 ) e. ZZ )
18 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
19 18 nn0red 
 |-  ( N e. NN0 -> ( N + 1 ) e. RR )
20 1red 
 |-  ( N e. NN0 -> 1 e. RR )
21 0le1 
 |-  0 <_ 1
22 21 a1i 
 |-  ( N e. NN0 -> 0 <_ 1 )
23 5 20 6 22 addge0d 
 |-  ( N e. NN0 -> 0 <_ ( N + 1 ) )
24 divge0 
 |-  ( ( ( ( N + 1 ) e. RR /\ 0 <_ ( N + 1 ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( ( N + 1 ) / 2 ) )
25 19 23 8 10 24 syl22anc 
 |-  ( N e. NN0 -> 0 <_ ( ( N + 1 ) / 2 ) )
26 25 adantr 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> 0 <_ ( ( N + 1 ) / 2 ) )
27 elnn0z 
 |-  ( ( ( N + 1 ) / 2 ) e. NN0 <-> ( ( ( N + 1 ) / 2 ) e. ZZ /\ 0 <_ ( ( N + 1 ) / 2 ) ) )
28 17 26 27 sylanbrc 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) / 2 ) e. NN0 )
29 28 ex 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. ZZ -> ( ( N + 1 ) / 2 ) e. NN0 ) )
30 16 29 orim12d 
 |-  ( N e. NN0 -> ( ( ( N / 2 ) e. ZZ \/ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N / 2 ) e. NN0 \/ ( ( N + 1 ) / 2 ) e. NN0 ) ) )
31 3 30 mpd 
 |-  ( N e. NN0 -> ( ( N / 2 ) e. NN0 \/ ( ( N + 1 ) / 2 ) e. NN0 ) )