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