Metamath Proof Explorer

Theorem oddnn02np1

Description: A nonnegative integer is odd iff it is one plus twice another nonnegative integer. (Contributed by AV, 19-Jun-2021)

Ref Expression
Assertion oddnn02np1 
|- ( N e. NN0 -> ( -. 2 || N <-> E. n e. NN0 ( ( 2 x. n ) + 1 ) = N ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( ( ( 2 x. n ) + 1 ) e. NN0 <-> N e. NN0 ) )
2 elnn0z 
 |-  ( ( ( 2 x. n ) + 1 ) e. NN0 <-> ( ( ( 2 x. n ) + 1 ) e. ZZ /\ 0 <_ ( ( 2 x. n ) + 1 ) ) )
3 2tnp1ge0ge0 
 |-  ( n e. ZZ -> ( 0 <_ ( ( 2 x. n ) + 1 ) <-> 0 <_ n ) )
4 3 biimpd 
 |-  ( n e. ZZ -> ( 0 <_ ( ( 2 x. n ) + 1 ) -> 0 <_ n ) )
5 4 imdistani 
 |-  ( ( n e. ZZ /\ 0 <_ ( ( 2 x. n ) + 1 ) ) -> ( n e. ZZ /\ 0 <_ n ) )
6 5 expcom 
 |-  ( 0 <_ ( ( 2 x. n ) + 1 ) -> ( n e. ZZ -> ( n e. ZZ /\ 0 <_ n ) ) )
7 elnn0z 
 |-  ( n e. NN0 <-> ( n e. ZZ /\ 0 <_ n ) )
8 6 7 syl6ibr 
 |-  ( 0 <_ ( ( 2 x. n ) + 1 ) -> ( n e. ZZ -> n e. NN0 ) )
9 2 8 simplbiim 
 |-  ( ( ( 2 x. n ) + 1 ) e. NN0 -> ( n e. ZZ -> n e. NN0 ) )
10 1 9 syl6bir 
 |-  ( ( ( 2 x. n ) + 1 ) = N -> ( N e. NN0 -> ( n e. ZZ -> n e. NN0 ) ) )
11 10 com13 
 |-  ( n e. ZZ -> ( N e. NN0 -> ( ( ( 2 x. n ) + 1 ) = N -> n e. NN0 ) ) )
12 11 impcom 
 |-  ( ( N e. NN0 /\ n e. ZZ ) -> ( ( ( 2 x. n ) + 1 ) = N -> n e. NN0 ) )
13 12 pm4.71rd 
 |-  ( ( N e. NN0 /\ n e. ZZ ) -> ( ( ( 2 x. n ) + 1 ) = N <-> ( n e. NN0 /\ ( ( 2 x. n ) + 1 ) = N ) ) )
14 13 bicomd 
 |-  ( ( N e. NN0 /\ n e. ZZ ) -> ( ( n e. NN0 /\ ( ( 2 x. n ) + 1 ) = N ) <-> ( ( 2 x. n ) + 1 ) = N ) )
15 14 rexbidva 
 |-  ( N e. NN0 -> ( E. n e. ZZ ( n e. NN0 /\ ( ( 2 x. n ) + 1 ) = N ) <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
16 nn0ssz 
 |-  NN0 C_ ZZ
17 rexss 
 |-  ( NN0 C_ ZZ -> ( E. n e. NN0 ( ( 2 x. n ) + 1 ) = N <-> E. n e. ZZ ( n e. NN0 /\ ( ( 2 x. n ) + 1 ) = N ) ) )
18 16 17 mp1i 
 |-  ( N e. NN0 -> ( E. n e. NN0 ( ( 2 x. n ) + 1 ) = N <-> E. n e. ZZ ( n e. NN0 /\ ( ( 2 x. n ) + 1 ) = N ) ) )
19 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
20 odd2np1 
 |-  ( N e. ZZ -> ( -. 2 || N <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
21 19 20 syl 
 |-  ( N e. NN0 -> ( -. 2 || N <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
22 15 18 21 3bitr4rd 
 |-  ( N e. NN0 -> ( -. 2 || N <-> E. n e. NN0 ( ( 2 x. n ) + 1 ) = N ) )