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

Step	Hyp	Ref	Expression
1		nnz	$⊢ N \in ℕ \to N \in ℤ$
2		oddp1d2	$⊢ N \in ℤ \to (\neg 2 ∥ N \leftrightarrow \frac{N + 1}{2} \in ℤ)$
3	1 2	syl	$⊢ N \in ℕ \to (\neg 2 ∥ N \leftrightarrow \frac{N + 1}{2} \in ℤ)$
4		peano2nn	$⊢ N \in ℕ \to N + 1 \in ℕ$
5	4	nnred	$⊢ N \in ℕ \to N + 1 \in ℝ$
6		2re	$⊢ 2 \in ℝ$
7	6	a1i	$⊢ N \in ℕ \to 2 \in ℝ$
8		nnre	$⊢ N \in ℕ \to N \in ℝ$
9		1red	$⊢ N \in ℕ \to 1 \in ℝ$
10		nngt0	$⊢ N \in ℕ \to 0 < N$
11		0lt1	$⊢ 0 < 1$
12	11	a1i	$⊢ N \in ℕ \to 0 < 1$
13	8 9 10 12	addgt0d	$⊢ N \in ℕ \to 0 < N + 1$
14		2pos	$⊢ 0 < 2$
15	14	a1i	$⊢ N \in ℕ \to 0 < 2$
16	5 7 13 15	divgt0d	$⊢ N \in ℕ \to 0 < \frac{N + 1}{2}$
17	16	anim1ci	$⊢ (N \in ℕ \land \frac{N + 1}{2} \in ℤ) \to (\frac{N + 1}{2} \in ℤ \land 0 < \frac{N + 1}{2})$
18		elnnz	$⊢ \frac{N + 1}{2} \in ℕ \leftrightarrow (\frac{N + 1}{2} \in ℤ \land 0 < \frac{N + 1}{2})$
19	17 18	sylibr	$⊢ (N \in ℕ \land \frac{N + 1}{2} \in ℤ) \to \frac{N + 1}{2} \in ℕ$
20	19	ex	$⊢ N \in ℕ \to (\frac{N + 1}{2} \in ℤ \to \frac{N + 1}{2} \in ℕ)$
21		nnz	$⊢ \frac{N + 1}{2} \in ℕ \to \frac{N + 1}{2} \in ℤ$
22	20 21	impbid1	$⊢ N \in ℕ \to (\frac{N + 1}{2} \in ℤ \leftrightarrow \frac{N + 1}{2} \in ℕ)$
23	3 22	bitrd	$⊢ N \in ℕ \to (\neg 2 ∥ N \leftrightarrow \frac{N + 1}{2} \in ℕ)$

Metamath Proof Explorer