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

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 ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Odd ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 )

Proof

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