This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )