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 ∈ ℕ 0 2 ⁢ 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 ∈ ℕ 0 2 ⁢ n + 1 = N ↔ ∃ n ∈ ℤ n ∈ ℕ 0 ∧ 2 ⁢ n + 1 = N
18 16 17 mp1i ⊢ N ∈ ℕ 0 → ∃ n ∈ ℕ 0 2 ⁢ 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 ∈ ℕ 0 2 ⁢ n + 1 = N