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∈ℕ0→¬2∥N↔∃n∈ℕ02⁢n+1=N

Proof

Step Hyp Ref Expression
1 eleq1 ⊢2⁢n+1=N→2⁢n+1∈ℕ0↔N∈ℕ0
2 elnn0z ⊢2⁢n+1∈ℕ0↔2⁢n+1∈ℤ∧0≤2⁢n+1
3 2tnp1ge0ge0 ⊢n∈ℤ→0≤2⁢n+1↔0≤n
4 3 biimpd ⊢n∈ℤ→0≤2⁢n+1→0≤n
5 4 imdistani ⊢n∈ℤ∧0≤2⁢n+1→n∈ℤ∧0≤n
6 5 expcom ⊢0≤2⁢n+1→n∈ℤ→n∈ℤ∧0≤n
7 elnn0z ⊢n∈ℕ0↔n∈ℤ∧0≤n
8 6 7 syl6ibr ⊢0≤2⁢n+1→n∈ℤ→n∈ℕ0
9 2 8 simplbiim ⊢2⁢n+1∈ℕ0→n∈ℤ→n∈ℕ0
10 1 9 syl6bir ⊢2⁢n+1=N→N∈ℕ0→n∈ℤ→n∈ℕ0
11 10 com13 ⊢n∈ℤ→N∈ℕ0→2⁢n+1=N→n∈ℕ0
12 11 impcom ⊢N∈ℕ0∧n∈ℤ→2⁢n+1=N→n∈ℕ0
13 12 pm4.71rd ⊢N∈ℕ0∧n∈ℤ→2⁢n+1=N↔n∈ℕ0∧2⁢n+1=N
14 13 bicomd ⊢N∈ℕ0∧n∈ℤ→n∈ℕ0∧2⁢n+1=N↔2⁢n+1=N
15 14 rexbidva ⊢N∈ℕ0→∃n∈ℤn∈ℕ0∧2⁢n+1=N↔∃n∈ℤ2⁢n+1=N
16 nn0ssz ⊢ℕ0⊆ℤ
17 rexss ⊢ℕ0⊆ℤ→∃n∈ℕ02⁢n+1=N↔∃n∈ℤn∈ℕ0∧2⁢n+1=N
18 16 17 mp1i ⊢N∈ℕ0→∃n∈ℕ02⁢n+1=N↔∃n∈ℤn∈ℕ0∧2⁢n+1=N
19 nn0z ⊢N∈ℕ0→N∈ℤ
20 odd2np1 ⊢N∈ℤ→¬2∥N↔∃n∈ℤ2⁢n+1=N
21 19 20 syl ⊢N∈ℕ0→¬2∥N↔∃n∈ℤ2⁢n+1=N
22 15 18 21 3bitr4rd ⊢N∈ℕ0→¬2∥N↔∃n∈ℕ02⁢n+1=N