Metamath Proof Explorer

Theorem odd2np1ALTV

Description: An integer is odd iff it is one plus twice another integer. (Contributed by Scott Fenton, 3-Apr-2014) (Revised by AV, 19-Jun-2020)

Ref Expression
Assertion odd2np1ALTV 
|- ( N e. ZZ -> ( N e. Odd <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )

Proof

Step Hyp Ref Expression
1 ibar 
 |-  ( N e. ZZ -> ( E. n e. ZZ N = ( ( 2 x. n ) + 1 ) <-> ( N e. ZZ /\ E. n e. ZZ N = ( ( 2 x. n ) + 1 ) ) ) )
2 eqcom 
 |-  ( ( ( 2 x. n ) + 1 ) = N <-> N = ( ( 2 x. n ) + 1 ) )
3 2 a1i 
 |-  ( N e. ZZ -> ( ( ( 2 x. n ) + 1 ) = N <-> N = ( ( 2 x. n ) + 1 ) ) )
4 3 rexbidv 
 |-  ( N e. ZZ -> ( E. n e. ZZ ( ( 2 x. n ) + 1 ) = N <-> E. n e. ZZ N = ( ( 2 x. n ) + 1 ) ) )
5 eqeq1 
 |-  ( z = N -> ( z = ( ( 2 x. n ) + 1 ) <-> N = ( ( 2 x. n ) + 1 ) ) )
6 5 rexbidv 
 |-  ( z = N -> ( E. n e. ZZ z = ( ( 2 x. n ) + 1 ) <-> E. n e. ZZ N = ( ( 2 x. n ) + 1 ) ) )
7 dfodd6 
 |-  Odd = { z e. ZZ | E. n e. ZZ z = ( ( 2 x. n ) + 1 ) }
8 6 7 elrab2 
 |-  ( N e. Odd <-> ( N e. ZZ /\ E. n e. ZZ N = ( ( 2 x. n ) + 1 ) ) )
9 8 a1i 
 |-  ( N e. ZZ -> ( N e. Odd <-> ( N e. ZZ /\ E. n e. ZZ N = ( ( 2 x. n ) + 1 ) ) ) )
10 1 4 9 3bitr4rd 
 |-  ( N e. ZZ -> ( N e. Odd <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )