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

Metamath Proof Explorer

Theorem nneven

Description: An alternate characterization of an even positive integer. (Contributed by AV, 5-Jun-2023)

Ref Expression
Assertion nneven 
|- ( ( N e. NN /\ N e. Even ) -> ( N / 2 ) e. NN )

Proof

Step Hyp Ref Expression
1 nnre 
 |-  ( N e. NN -> N e. RR )
2 2re 
 |-  2 e. RR
3 2 a1i 
 |-  ( N e. NN -> 2 e. RR )
4 nngt0 
 |-  ( N e. NN -> 0 < N )
5 2pos 
 |-  0 < 2
6 5 a1i 
 |-  ( N e. NN -> 0 < 2 )
7 1 3 4 6 divgt0d 
 |-  ( N e. NN -> 0 < ( N / 2 ) )
8 evendiv2z 
 |-  ( N e. Even -> ( N / 2 ) e. ZZ )
9 7 8 anim12ci 
 |-  ( ( N e. NN /\ N e. Even ) -> ( ( N / 2 ) e. ZZ /\ 0 < ( N / 2 ) ) )
10 elnnz 
 |-  ( ( N / 2 ) e. NN <-> ( ( N / 2 ) e. ZZ /\ 0 < ( N / 2 ) ) )
11 9 10 sylibr 
 |-  ( ( N e. NN /\ N e. Even ) -> ( N / 2 ) e. NN )