Metamath Proof Explorer

Theorem nn0e

Description: An alternate characterization of an even nonnegative integer. (Contributed by AV, 22-Jun-2020)

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

Proof

Step Hyp Ref Expression
1 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
2 nn0re 
 |-  ( N e. NN0 -> N e. RR )
3 2re 
 |-  2 e. RR
4 3 a1i 
 |-  ( N e. NN0 -> 2 e. RR )
5 2pos 
 |-  0 < 2
6 5 a1i 
 |-  ( N e. NN0 -> 0 < 2 )
7 ge0div 
 |-  ( ( N e. RR /\ 2 e. RR /\ 0 < 2 ) -> ( 0 <_ N <-> 0 <_ ( N / 2 ) ) )
8 2 4 6 7 syl3anc 
 |-  ( N e. NN0 -> ( 0 <_ N <-> 0 <_ ( N / 2 ) ) )
9 1 8 mpbid 
 |-  ( N e. NN0 -> 0 <_ ( N / 2 ) )
10 evendiv2z 
 |-  ( N e. Even -> ( N / 2 ) e. ZZ )
11 9 10 anim12ci 
 |-  ( ( N e. NN0 /\ N e. Even ) -> ( ( N / 2 ) e. ZZ /\ 0 <_ ( N / 2 ) ) )
12 elnn0z 
 |-  ( ( N / 2 ) e. NN0 <-> ( ( N / 2 ) e. ZZ /\ 0 <_ ( N / 2 ) ) )
13 11 12 sylibr 
 |-  ( ( N e. NN0 /\ N e. Even ) -> ( N / 2 ) e. NN0 )