Metamath Proof Explorer

Theorem nn0oALTV

Description: An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020) (Revised by AV, 21-Jun-2020)

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

Proof

Step Hyp Ref Expression
1 oddm1div2z 
 |-  ( N e. Odd -> ( ( N - 1 ) / 2 ) e. ZZ )
2 1 adantl 
 |-  ( ( N e. NN0 /\ N e. Odd ) -> ( ( N - 1 ) / 2 ) e. ZZ )
3 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
4 nnm1ge0 
 |-  ( N e. NN -> 0 <_ ( N - 1 ) )
5 nnre 
 |-  ( N e. NN -> N e. RR )
6 peano2rem 
 |-  ( N e. RR -> ( N - 1 ) e. RR )
7 5 6 syl 
 |-  ( N e. NN -> ( N - 1 ) e. RR )
8 2re 
 |-  2 e. RR
9 8 a1i 
 |-  ( N e. NN -> 2 e. RR )
10 2pos 
 |-  0 < 2
11 10 a1i 
 |-  ( N e. NN -> 0 < 2 )
12 ge0div 
 |-  ( ( ( N - 1 ) e. RR /\ 2 e. RR /\ 0 < 2 ) -> ( 0 <_ ( N - 1 ) <-> 0 <_ ( ( N - 1 ) / 2 ) ) )
13 7 9 11 12 syl3anc 
 |-  ( N e. NN -> ( 0 <_ ( N - 1 ) <-> 0 <_ ( ( N - 1 ) / 2 ) ) )
14 4 13 mpbid 
 |-  ( N e. NN -> 0 <_ ( ( N - 1 ) / 2 ) )
15 14 a1d 
 |-  ( N e. NN -> ( N e. Odd -> 0 <_ ( ( N - 1 ) / 2 ) ) )
16 eleq1 
 |-  ( N = 0 -> ( N e. Odd <-> 0 e. Odd ) )
17 0noddALTV 
 |-  0 e/ Odd
18 df-nel 
 |-  ( 0 e/ Odd <-> -. 0 e. Odd )
19 pm2.21 
 |-  ( -. 0 e. Odd -> ( 0 e. Odd -> 0 <_ ( ( N - 1 ) / 2 ) ) )
20 18 19 sylbi 
 |-  ( 0 e/ Odd -> ( 0 e. Odd -> 0 <_ ( ( N - 1 ) / 2 ) ) )
21 17 20 ax-mp 
 |-  ( 0 e. Odd -> 0 <_ ( ( N - 1 ) / 2 ) )
22 16 21 biimtrdi 
 |-  ( N = 0 -> ( N e. Odd -> 0 <_ ( ( N - 1 ) / 2 ) ) )
23 15 22 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( N e. Odd -> 0 <_ ( ( N - 1 ) / 2 ) ) )
24 3 23 sylbi 
 |-  ( N e. NN0 -> ( N e. Odd -> 0 <_ ( ( N - 1 ) / 2 ) ) )
25 24 imp 
 |-  ( ( N e. NN0 /\ N e. Odd ) -> 0 <_ ( ( N - 1 ) / 2 ) )
26 elnn0z 
 |-  ( ( ( N - 1 ) / 2 ) e. NN0 <-> ( ( ( N - 1 ) / 2 ) e. ZZ /\ 0 <_ ( ( N - 1 ) / 2 ) ) )
27 2 25 26 sylanbrc 
 |-  ( ( N e. NN0 /\ N e. Odd ) -> ( ( N - 1 ) / 2 ) e. NN0 )