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 )