Metamath Proof Explorer

Theorem nnoddm1d2

Description: A positive integer is odd iff its successor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021)

Ref Expression
Assertion nnoddm1d2 
|- ( N e. NN -> ( -. 2 || N <-> ( ( N + 1 ) / 2 ) e. NN ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( N e. NN -> N e. ZZ )
2 oddp1d2 
 |-  ( N e. ZZ -> ( -. 2 || N <-> ( ( N + 1 ) / 2 ) e. ZZ ) )
3 1 2 syl 
 |-  ( N e. NN -> ( -. 2 || N <-> ( ( N + 1 ) / 2 ) e. ZZ ) )
4 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
5 4 nnred 
 |-  ( N e. NN -> ( N + 1 ) e. RR )
6 2re 
 |-  2 e. RR
7 6 a1i 
 |-  ( N e. NN -> 2 e. RR )
8 nnre 
 |-  ( N e. NN -> N e. RR )
9 1red 
 |-  ( N e. NN -> 1 e. RR )
10 nngt0 
 |-  ( N e. NN -> 0 < N )
11 0lt1 
 |-  0 < 1
12 11 a1i 
 |-  ( N e. NN -> 0 < 1 )
13 8 9 10 12 addgt0d 
 |-  ( N e. NN -> 0 < ( N + 1 ) )
14 2pos 
 |-  0 < 2
15 14 a1i 
 |-  ( N e. NN -> 0 < 2 )
16 5 7 13 15 divgt0d 
 |-  ( N e. NN -> 0 < ( ( N + 1 ) / 2 ) )
17 16 anim1ci 
 |-  ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( N + 1 ) / 2 ) e. ZZ /\ 0 < ( ( N + 1 ) / 2 ) ) )
18 elnnz 
 |-  ( ( ( N + 1 ) / 2 ) e. NN <-> ( ( ( N + 1 ) / 2 ) e. ZZ /\ 0 < ( ( N + 1 ) / 2 ) ) )
19 17 18 sylibr 
 |-  ( ( N e. NN /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) / 2 ) e. NN )
20 19 ex 
 |-  ( N e. NN -> ( ( ( N + 1 ) / 2 ) e. ZZ -> ( ( N + 1 ) / 2 ) e. NN ) )
21 nnz 
 |-  ( ( ( N + 1 ) / 2 ) e. NN -> ( ( N + 1 ) / 2 ) e. ZZ )
22 20 21 impbid1 
 |-  ( N e. NN -> ( ( ( N + 1 ) / 2 ) e. ZZ <-> ( ( N + 1 ) / 2 ) e. NN ) )
23 3 22 bitrd 
 |-  ( N e. NN -> ( -. 2 || N <-> ( ( N + 1 ) / 2 ) e. NN ) )