Metamath Proof Explorer

Theorem nn0oddm1d2

Description: A positive integer is odd iff its predecessor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion nn0oddm1d2 ⊢ N ∈ ℕ 0 → ¬ 2 ∥ N ↔ N − 1 2 ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 nn0z ⊢ N ∈ ℕ 0 → N ∈ ℤ
2 oddp1d2 ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ N + 1 2 ∈ ℤ
3 1 2 syl ⊢ N ∈ ℕ 0 → ¬ 2 ∥ N ↔ N + 1 2 ∈ ℤ
4 peano2nn0 ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ 0
5 4 nn0red ⊢ N ∈ ℕ 0 → N + 1 ∈ ℝ
6 2rp ⊢ 2 ∈ ℝ +
7 6 a1i ⊢ N ∈ ℕ 0 → 2 ∈ ℝ +
8 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
9 1red ⊢ N ∈ ℕ 0 → 1 ∈ ℝ
10 nn0ge0 ⊢ N ∈ ℕ 0 → 0 ≤ N
11 0le1 ⊢ 0 ≤ 1
12 11 a1i ⊢ N ∈ ℕ 0 → 0 ≤ 1
13 8 9 10 12 addge0d ⊢ N ∈ ℕ 0 → 0 ≤ N + 1
14 5 7 13 divge0d ⊢ N ∈ ℕ 0 → 0 ≤ N + 1 2
15 14 anim1ci ⊢ N ∈ ℕ 0 ∧ N + 1 2 ∈ ℤ → N + 1 2 ∈ ℤ ∧ 0 ≤ N + 1 2
16 elnn0z ⊢ N + 1 2 ∈ ℕ 0 ↔ N + 1 2 ∈ ℤ ∧ 0 ≤ N + 1 2
17 15 16 sylibr ⊢ N ∈ ℕ 0 ∧ N + 1 2 ∈ ℤ → N + 1 2 ∈ ℕ 0
18 17 ex ⊢ N ∈ ℕ 0 → N + 1 2 ∈ ℤ → N + 1 2 ∈ ℕ 0
19 nn0z ⊢ N + 1 2 ∈ ℕ 0 → N + 1 2 ∈ ℤ
20 18 19 impbid1 ⊢ N ∈ ℕ 0 → N + 1 2 ∈ ℤ ↔ N + 1 2 ∈ ℕ 0
21 nn0ob ⊢ N ∈ ℕ 0 → N + 1 2 ∈ ℕ 0 ↔ N − 1 2 ∈ ℕ 0
22 3 20 21 3bitrd ⊢ N ∈ ℕ 0 → ¬ 2 ∥ N ↔ N − 1 2 ∈ ℕ 0