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

Metamath Proof Explorer

Theorem nn0oddm1d2

Description: A positive integer is odd iff its predecessor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion nn0oddm1d2 
|- ( N e. NN0 -> ( -. 2 || N <-> ( ( N - 1 ) / 2 ) e. NN0 ) )

Proof

Step Hyp Ref Expression
1 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
2 oddp1d2 
 |-  ( N e. ZZ -> ( -. 2 || N <-> ( ( N + 1 ) / 2 ) e. ZZ ) )
3 1 2 syl 
 |-  ( N e. NN0 -> ( -. 2 || N <-> ( ( N + 1 ) / 2 ) e. ZZ ) )
4 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
5 4 nn0red 
 |-  ( N e. NN0 -> ( N + 1 ) e. RR )
6 2rp 
 |-  2 e. RR+
7 6 a1i 
 |-  ( N e. NN0 -> 2 e. RR+ )
8 nn0re 
 |-  ( N e. NN0 -> N e. RR )
9 1red 
 |-  ( N e. NN0 -> 1 e. RR )
10 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
11 0le1 
 |-  0 <_ 1
12 11 a1i 
 |-  ( N e. NN0 -> 0 <_ 1 )
13 8 9 10 12 addge0d 
 |-  ( N e. NN0 -> 0 <_ ( N + 1 ) )
14 5 7 13 divge0d 
 |-  ( N e. NN0 -> 0 <_ ( ( N + 1 ) / 2 ) )
15 14 anim1ci 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( ( N + 1 ) / 2 ) e. ZZ /\ 0 <_ ( ( N + 1 ) / 2 ) ) )
16 elnn0z 
 |-  ( ( ( N + 1 ) / 2 ) e. NN0 <-> ( ( ( N + 1 ) / 2 ) e. ZZ /\ 0 <_ ( ( N + 1 ) / 2 ) ) )
17 15 16 sylibr 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( ( N + 1 ) / 2 ) e. NN0 )
18 17 ex 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. ZZ -> ( ( N + 1 ) / 2 ) e. NN0 ) )
19 nn0z 
 |-  ( ( ( N + 1 ) / 2 ) e. NN0 -> ( ( N + 1 ) / 2 ) e. ZZ )
20 18 19 impbid1 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. ZZ <-> ( ( N + 1 ) / 2 ) e. NN0 ) )
21 nn0ob 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. NN0 <-> ( ( N - 1 ) / 2 ) e. NN0 ) )
22 3 20 21 3bitrd 
 |-  ( N e. NN0 -> ( -. 2 || N <-> ( ( N - 1 ) / 2 ) e. NN0 ) )