Theorem nn0ob

Description: Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020)

	Ref	Expression
Assertion	nn0ob	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\leftrightarrow \frac{N-1}{2}\in {\mathbb{N}}_0\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0o	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\in {\mathbb{N}}_0$$
2		nn0cn	$$⊢N\in {\mathbb{N}}_0\to N\in ℂ$$
3		xp1d2m1eqxm1d2	$$⊢N\in ℂ\to \left(\frac{N+1}{2}\right)-1=\frac{N-1}{2}$$
4	3	eqcomd	$$⊢N\in ℂ\to \frac{N-1}{2}=\left(\frac{N+1}{2}\right)-1$$
5	2 4	syl	$$⊢N\in {\mathbb{N}}_0\to \frac{N-1}{2}=\left(\frac{N+1}{2}\right)-1$$
6		peano2cnm	$$⊢N\in ℂ\to N-1\in ℂ$$
7	2 6	syl	$$⊢N\in {\mathbb{N}}_0\to N-1\in ℂ$$
8	7	halfcld	$$⊢N\in {\mathbb{N}}_0\to \frac{N-1}{2}\in ℂ$$
9		1cnd	$$⊢N\in {\mathbb{N}}_0\to 1\in ℂ$$
10		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
11	10	nn0cnd	$$⊢N\in {\mathbb{N}}_0\to N+1\in ℂ$$
12	11	halfcld	$$⊢N\in {\mathbb{N}}_0\to \frac{N+1}{2}\in ℂ$$
13	8 9 12	addlsub	$$⊢N\in {\mathbb{N}}_0\to \left(\left(\frac{N-1}{2}\right)+1=\frac{N+1}{2}\leftrightarrow \frac{N-1}{2}=\left(\frac{N+1}{2}\right)-1\right)$$
14	5 13	mpbird	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{N-1}{2}\right)+1=\frac{N+1}{2}$$
15	14	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)\to \left(\frac{N-1}{2}\right)+1=\frac{N+1}{2}$$
16		peano2nn0	$$⊢\frac{N-1}{2}\in {\mathbb{N}}_0\to \left(\frac{N-1}{2}\right)+1\in {\mathbb{N}}_0$$
17	16	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)\to \left(\frac{N-1}{2}\right)+1\in {\mathbb{N}}_0$$
18	15 17	eqeltrrd	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)\to \frac{N+1}{2}\in {\mathbb{N}}_0$$
19	1 18	impbida	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\leftrightarrow \frac{N-1}{2}\in {\mathbb{N}}_0\right)$$