Metamath Proof Explorer

Theorem nn0oALTV

Description: An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020) (Revised by AV, 21-Jun-2020)

Ref Expression
Assertion nn0oALTV ⊢ N ∈ ℕ 0 ∧ N ∈ Odd → N − 1 2 ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 oddm1div2z ⊢ N ∈ Odd → N − 1 2 ∈ ℤ
2 1 adantl ⊢ N ∈ ℕ 0 ∧ N ∈ Odd → N − 1 2 ∈ ℤ
3 elnn0 ⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0
4 nnm1ge0 ⊢ N ∈ ℕ → 0 ≤ N − 1
5 nnre ⊢ N ∈ ℕ → N ∈ ℝ
6 peano2rem ⊢ N ∈ ℝ → N − 1 ∈ ℝ
7 5 6 syl ⊢ N ∈ ℕ → N − 1 ∈ ℝ
8 2re ⊢ 2 ∈ ℝ
9 8 a1i ⊢ N ∈ ℕ → 2 ∈ ℝ
10 2pos ⊢ 0 < 2
11 10 a1i ⊢ N ∈ ℕ → 0 < 2
12 ge0div ⊢ N − 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 2 → 0 ≤ N − 1 ↔ 0 ≤ N − 1 2
13 7 9 11 12 syl3anc ⊢ N ∈ ℕ → 0 ≤ N − 1 ↔ 0 ≤ N − 1 2
14 4 13 mpbid ⊢ N ∈ ℕ → 0 ≤ N − 1 2
15 14 a1d ⊢ N ∈ ℕ → N ∈ Odd → 0 ≤ N − 1 2
16 eleq1 ⊢ N = 0 → N ∈ Odd ↔ 0 ∈ Odd
17 0noddALTV ⊢ 0 ∉ Odd
18 df-nel ⊢ 0 ∉ Odd ↔ ¬ 0 ∈ Odd
19 pm2.21 ⊢ ¬ 0 ∈ Odd → 0 ∈ Odd → 0 ≤ N − 1 2
20 18 19 sylbi ⊢ 0 ∉ Odd → 0 ∈ Odd → 0 ≤ N − 1 2
21 17 20 ax-mp ⊢ 0 ∈ Odd → 0 ≤ N − 1 2
22 16 21 syl6bi ⊢ N = 0 → N ∈ Odd → 0 ≤ N − 1 2
23 15 22 jaoi ⊢ N ∈ ℕ ∨ N = 0 → N ∈ Odd → 0 ≤ N − 1 2
24 3 23 sylbi ⊢ N ∈ ℕ 0 → N ∈ Odd → 0 ≤ N − 1 2
25 24 imp ⊢ N ∈ ℕ 0 ∧ N ∈ Odd → 0 ≤ N − 1 2
26 elnn0z ⊢ N − 1 2 ∈ ℕ 0 ↔ N − 1 2 ∈ ℤ ∧ 0 ≤ N − 1 2
27 2 25 26 sylanbrc ⊢ N ∈ ℕ 0 ∧ N ∈ Odd → N − 1 2 ∈ ℕ 0