Theorem nnoddm1d2

Description: A positive integer is odd iff its successor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021)

	Ref	Expression
Assertion	nnoddm1d2	⊢ ( 𝑁 ∈ ℕ → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
2		oddp1d2	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℕ → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
4		peano2nn	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
5	4	nnred	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℝ )
6		2re	⊢ 2 ∈ ℝ
7	6	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ )
8		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
9		1red	⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
10		nngt0	⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
11		0lt1	⊢ 0 < 1
12	11	a1i	⊢ ( 𝑁 ∈ ℕ → 0 < 1 )
13	8 9 10 12	addgt0d	⊢ ( 𝑁 ∈ ℕ → 0 < ( 𝑁 + 1 ) )
14		2pos	⊢ 0 < 2
15	14	a1i	⊢ ( 𝑁 ∈ ℕ → 0 < 2 )
16	5 7 13 15	divgt0d	⊢ ( 𝑁 ∈ ℕ → 0 < ( ( 𝑁 + 1 ) / 2 ) )
17	16	anim1ci	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ 0 < ( ( 𝑁 + 1 ) / 2 ) ) )
18		elnnz	⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ↔ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ 0 < ( ( 𝑁 + 1 ) / 2 ) ) )
19	17 18	sylibr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ )
20	19	ex	⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
21		nnz	⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ )
22	20 21	impbid1	⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
23	3 22	bitrd	⊢ ( 𝑁 ∈ ℕ → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )