Metamath Proof Explorer

Theorem nn0enne

Description: A positive integer is an even nonnegative integer iff it is an even positive integer. (Contributed by AV, 30-May-2020)

Ref Expression
Assertion nn0enne 
|- ( N e. NN -> ( ( N / 2 ) e. NN0 <-> ( N / 2 ) e. NN ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( ( N / 2 ) e. NN0 <-> ( ( N / 2 ) e. NN \/ ( N / 2 ) = 0 ) )
2 nncn 
 |-  ( N e. NN -> N e. CC )
3 2cnd 
 |-  ( N e. NN -> 2 e. CC )
4 2ne0 
 |-  2 =/= 0
5 4 a1i 
 |-  ( N e. NN -> 2 =/= 0 )
6 2 3 5 diveq0ad 
 |-  ( N e. NN -> ( ( N / 2 ) = 0 <-> N = 0 ) )
7 eleq1 
 |-  ( N = 0 -> ( N e. NN <-> 0 e. NN ) )
8 0nnn 
 |-  -. 0 e. NN
9 8 pm2.21i 
 |-  ( 0 e. NN -> ( N / 2 ) e. NN )
10 7 9 syl6bi 
 |-  ( N = 0 -> ( N e. NN -> ( N / 2 ) e. NN ) )
11 10 com12 
 |-  ( N e. NN -> ( N = 0 -> ( N / 2 ) e. NN ) )
12 6 11 sylbid 
 |-  ( N e. NN -> ( ( N / 2 ) = 0 -> ( N / 2 ) e. NN ) )
13 12 com12 
 |-  ( ( N / 2 ) = 0 -> ( N e. NN -> ( N / 2 ) e. NN ) )
14 13 jao1i 
 |-  ( ( ( N / 2 ) e. NN \/ ( N / 2 ) = 0 ) -> ( N e. NN -> ( N / 2 ) e. NN ) )
15 1 14 sylbi 
 |-  ( ( N / 2 ) e. NN0 -> ( N e. NN -> ( N / 2 ) e. NN ) )
16 15 com12 
 |-  ( N e. NN -> ( ( N / 2 ) e. NN0 -> ( N / 2 ) e. NN ) )
17 nnnn0 
 |-  ( ( N / 2 ) e. NN -> ( N / 2 ) e. NN0 )
18 16 17 impbid1 
 |-  ( N e. NN -> ( ( N / 2 ) e. NN0 <-> ( N / 2 ) e. NN ) )