Theorem nn0oddm1d2

Description: A positive integer is odd iff its predecessor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021) (Proof shortened by AV, 10-Jul-2022)

	Ref	Expression
Assertion	nn0oddm1d2	⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
2		oddp1d2	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
4		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
5	4	nn0red	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℝ )
6		2rp	⊢ 2 ∈ ℝ+
7	6	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ+ )
8		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
9		1red	⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℝ )
10		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
11		0le1	⊢ 0 ≤ 1
12	11	a1i	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 1 )
13	8 9 10 12	addge0d	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ ( 𝑁 + 1 ) )
14	5 7 13	divge0d	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ ( ( 𝑁 + 1 ) / 2 ) )
15	14	anim1ci	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑁 + 1 ) / 2 ) ) )
16		elnn0z	⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ↔ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑁 + 1 ) / 2 ) ) )
17	15 16	sylibr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) → ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 )
18	17	ex	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) )
19		nn0z	⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ )
20	18 19	impbid1	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) )
21		nn0ob	⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )
22	3 20 21	3bitrd	⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ ( ( 𝑁 − 1 ) / 2 ) ∈ ℕ0 ) )