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

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

Proof

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