Metamath Proof Explorer

Theorem nnoALTV

Description: An alternate characterization of an odd number greater than 1. (Contributed by AV, 2-Jun-2020) (Revised by AV, 21-Jun-2020)

Ref Expression
Assertion nnoALTV ⊢ N ∈ ℤ ≥ 2 ∧ N ∈ Odd → N − 1 2 ∈ ℕ

Proof

Step Hyp Ref Expression
1 oddm1div2z ⊢ N ∈ Odd → N − 1 2 ∈ ℤ
2 1 adantl ⊢ N ∈ ℤ ≥ 2 ∧ N ∈ Odd → N − 1 2 ∈ ℤ
3 eluz2b1 ⊢ N ∈ ℤ ≥ 2 ↔ N ∈ ℤ ∧ 1 < N
4 1red ⊢ N ∈ ℤ → 1 ∈ ℝ
5 zre ⊢ N ∈ ℤ → N ∈ ℝ
6 4 5 posdifd ⊢ N ∈ ℤ → 1 < N ↔ 0 < N − 1
7 6 biimpa ⊢ N ∈ ℤ ∧ 1 < N → 0 < N − 1
8 peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ
9 8 zred ⊢ N ∈ ℤ → N − 1 ∈ ℝ
10 2re ⊢ 2 ∈ ℝ
11 10 a1i ⊢ N ∈ ℤ → 2 ∈ ℝ
12 2pos ⊢ 0 < 2
13 12 a1i ⊢ N ∈ ℤ → 0 < 2
14 9 11 13 3jca ⊢ N ∈ ℤ → N − 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 2
15 14 adantr ⊢ N ∈ ℤ ∧ 1 < N → N − 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 2
16 gt0div ⊢ N − 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 2 → 0 < N − 1 ↔ 0 < N − 1 2
17 15 16 syl ⊢ N ∈ ℤ ∧ 1 < N → 0 < N − 1 ↔ 0 < N − 1 2
18 7 17 mpbid ⊢ N ∈ ℤ ∧ 1 < N → 0 < N − 1 2
19 3 18 sylbi ⊢ N ∈ ℤ ≥ 2 → 0 < N − 1 2
20 19 adantr ⊢ N ∈ ℤ ≥ 2 ∧ N ∈ Odd → 0 < N − 1 2
21 elnnz ⊢ N − 1 2 ∈ ℕ ↔ N − 1 2 ∈ ℤ ∧ 0 < N − 1 2
22 2 20 21 sylanbrc ⊢ N ∈ ℤ ≥ 2 ∧ N ∈ Odd → N − 1 2 ∈ ℕ