Metamath Proof Explorer

Theorem nn0o

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

Ref Expression
Assertion nn0o ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 nn0o1gt2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 = 1 ∨ 2 < 𝑁 ) )
2 1m1e0 ⊢ ( 1 − 1 ) = 0
3 2 oveq1i ⊢ ( ( 1 − 1 ) / 2 ) = ( 0 / 2 )
4 2cn ⊢ 2 ∈ ℂ
5 2ne0 ⊢ 2 ≠ 0
6 4 5 div0i ⊢ ( 0 / 2 ) = 0
7 3 6 eqtri ⊢ ( ( 1 − 1 ) / 2 ) = 0
8 0nn0 ⊢ 0 ∈ ℕ0
9 7 8 eqeltri ⊢ ( ( 1 − 1 ) / 2 ) ∈ ℕ0
10 oveq1 ⊢ ( 𝑁 = 1 → ( 𝑁 − 1 ) = ( 1 − 1 ) )
11 10 oveq1d ⊢ ( 𝑁 = 1 → ( ( 𝑁 − 1 ) / 2 ) = ( ( 1 − 1 ) / 2 ) )
12 11 eleq1d ⊢ ( 𝑁 = 1 → ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ↔ ( ( 1 − 1 ) / 2 ) ∈ ℕ0 ) )
13 12 adantr ⊢ ( ( 𝑁 = 1 ∧ ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ) → ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ↔ ( ( 1 − 1 ) / 2 ) ∈ ℕ0 ) )
14 9 13 mpbiri ⊢ ( ( 𝑁 = 1 ∧ ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 )
15 14 ex ⊢ ( 𝑁 = 1 → ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )
16 2z ⊢ 2 ∈ ℤ
17 16 a1i ⊢ ( ( 2 < 𝑁 ∧ ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ) → 2 ∈ ℤ )
18 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
19 18 ad2antrl ⊢ ( ( 2 < 𝑁 ∧ ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ) → 𝑁 ∈ ℤ )
20 2re ⊢ 2 ∈ ℝ
21 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
22 ltle ⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 2 < 𝑁 → 2 ≤ 𝑁 ) )
23 20 21 22 sylancr ⊢ ( 𝑁 ∈ ℕ0 → ( 2 < 𝑁 → 2 ≤ 𝑁 ) )
24 23 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 2 < 𝑁 → 2 ≤ 𝑁 ) )
25 24 impcom ⊢ ( ( 2 < 𝑁 ∧ ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ) → 2 ≤ 𝑁 )
26 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) )
27 17 19 25 26 syl3anbrc ⊢ ( ( 2 < 𝑁 ∧ ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
28 simprr ⊢ ( ( 2 < 𝑁 ∧ ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ) → ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 )
29 27 28 jca ⊢ ( ( 2 < 𝑁 ∧ ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) )
30 nno ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ )
31 nnnn0 ⊢ ( ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 )
32 29 30 31 3syl ⊢ ( ( 2 < 𝑁 ∧ ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 )
33 32 ex ⊢ ( 2 < 𝑁 → ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )
34 15 33 jaoi ⊢ ( ( 𝑁 = 1 ∨ 2 < 𝑁 ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )
35 1 34 mpcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 )