This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ0 ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )

Proof

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