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∈ℤ→N∈Odd↔∃n∈ℤ2⁢n+1=N

Proof

Step Hyp Ref Expression
1 ibar ⊢N∈ℤ→∃n∈ℤN=2⁢n+1↔N∈ℤ∧∃n∈ℤN=2⁢n+1
2 eqcom ⊢2⁢n+1=N↔N=2⁢n+1
3 2 a1i ⊢N∈ℤ→2⁢n+1=N↔N=2⁢n+1
4 3 rexbidv ⊢N∈ℤ→∃n∈ℤ2⁢n+1=N↔∃n∈ℤN=2⁢n+1
5 eqeq1 ⊢z=N→z=2⁢n+1↔N=2⁢n+1
6 5 rexbidv ⊢z=N→∃n∈ℤz=2⁢n+1↔∃n∈ℤN=2⁢n+1
7 dfodd6 ⊢Odd=z∈ℤ|∃n∈ℤz=2⁢n+1
8 6 7 elrab2 ⊢N∈Odd↔N∈ℤ∧∃n∈ℤN=2⁢n+1
9 8 a1i ⊢N∈ℤ→N∈Odd↔N∈ℤ∧∃n∈ℤN=2⁢n+1
10 1 4 9 3bitr4rd ⊢N∈ℤ→N∈Odd↔∃n∈ℤ2⁢n+1=N