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 ) )