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 ) ∈ ℕ )