Metamath Proof Explorer

Theorem nnoddm1d2

Description: A positive integer is odd iff its successor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021)

Ref Expression
Assertion nnoddm1d2 ⊢ N ∈ ℕ → ¬ 2 ∥ N ↔ N + 1 2 ∈ ℕ

Proof

Step Hyp Ref Expression
1 nnz ⊢ N ∈ ℕ → N ∈ ℤ
2 oddp1d2 ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ N + 1 2 ∈ ℤ
3 1 2 syl ⊢ N ∈ ℕ → ¬ 2 ∥ N ↔ N + 1 2 ∈ ℤ
4 peano2nn ⊢ N ∈ ℕ → N + 1 ∈ ℕ
5 4 nnred ⊢ N ∈ ℕ → N + 1 ∈ ℝ
6 2re ⊢ 2 ∈ ℝ
7 6 a1i ⊢ N ∈ ℕ → 2 ∈ ℝ
8 nnre ⊢ N ∈ ℕ → N ∈ ℝ
9 1red ⊢ N ∈ ℕ → 1 ∈ ℝ
10 nngt0 ⊢ N ∈ ℕ → 0 < N
11 0lt1 ⊢ 0 < 1
12 11 a1i ⊢ N ∈ ℕ → 0 < 1
13 8 9 10 12 addgt0d ⊢ N ∈ ℕ → 0 < N + 1
14 2pos ⊢ 0 < 2
15 14 a1i ⊢ N ∈ ℕ → 0 < 2
16 5 7 13 15 divgt0d ⊢ N ∈ ℕ → 0 < N + 1 2
17 16 anim1ci ⊢ N ∈ ℕ ∧ N + 1 2 ∈ ℤ → N + 1 2 ∈ ℤ ∧ 0 < N + 1 2
18 elnnz ⊢ N + 1 2 ∈ ℕ ↔ N + 1 2 ∈ ℤ ∧ 0 < N + 1 2
19 17 18 sylibr ⊢ N ∈ ℕ ∧ N + 1 2 ∈ ℤ → N + 1 2 ∈ ℕ
20 19 ex ⊢ N ∈ ℕ → N + 1 2 ∈ ℤ → N + 1 2 ∈ ℕ
21 nnz ⊢ N + 1 2 ∈ ℕ → N + 1 2 ∈ ℤ
22 20 21 impbid1 ⊢ N ∈ ℕ → N + 1 2 ∈ ℤ ↔ N + 1 2 ∈ ℕ
23 3 22 bitrd ⊢ N ∈ ℕ → ¬ 2 ∥ N ↔ N + 1 2 ∈ ℕ