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	$⊢ N \in ℕ_{0} \to (\neg 2 ∥ N \leftrightarrow \frac{N - 1}{2} \in ℕ_{0})$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
2		oddp1d2	$⊢ N \in ℤ \to (\neg 2 ∥ N \leftrightarrow \frac{N + 1}{2} \in ℤ)$
3	1 2	syl	$⊢ N \in ℕ_{0} \to (\neg 2 ∥ N \leftrightarrow \frac{N + 1}{2} \in ℤ)$
4		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
5	4	nn0red	$⊢ N \in ℕ_{0} \to N + 1 \in ℝ$
6		2rp	$⊢ 2 \in ℝ^{+}$
7	6	a1i	$⊢ N \in ℕ_{0} \to 2 \in ℝ^{+}$
8		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
9		1red	$⊢ N \in ℕ_{0} \to 1 \in ℝ$
10		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
11		0le1	$⊢ 0 \leq 1$
12	11	a1i	$⊢ N \in ℕ_{0} \to 0 \leq 1$
13	8 9 10 12	addge0d	$⊢ N \in ℕ_{0} \to 0 \leq N + 1$
14	5 7 13	divge0d	$⊢ N \in ℕ_{0} \to 0 \leq \frac{N + 1}{2}$
15	14	anim1ci	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℤ) \to (\frac{N + 1}{2} \in ℤ \land 0 \leq \frac{N + 1}{2})$
16		elnn0z	$⊢ \frac{N + 1}{2} \in ℕ_{0} \leftrightarrow (\frac{N + 1}{2} \in ℤ \land 0 \leq \frac{N + 1}{2})$
17	15 16	sylibr	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℤ) \to \frac{N + 1}{2} \in ℕ_{0}$
18	17	ex	$⊢ N \in ℕ_{0} \to (\frac{N + 1}{2} \in ℤ \to \frac{N + 1}{2} \in ℕ_{0})$
19		nn0z	$⊢ \frac{N + 1}{2} \in ℕ_{0} \to \frac{N + 1}{2} \in ℤ$
20	18 19	impbid1	$⊢ N \in ℕ_{0} \to (\frac{N + 1}{2} \in ℤ \leftrightarrow \frac{N + 1}{2} \in ℕ_{0})$
21		nn0ob	$⊢ N \in ℕ_{0} \to (\frac{N + 1}{2} \in ℕ_{0} \leftrightarrow \frac{N - 1}{2} \in ℕ_{0})$
22	3 20 21	3bitrd	$⊢ N \in ℕ_{0} \to (\neg 2 ∥ N \leftrightarrow \frac{N - 1}{2} \in ℕ_{0})$

Metamath Proof Explorer

Theorem nn0oddm1d2

Proof