Theorem nn0onn0ex

Description: For each odd nonnegative integer there is a nonnegative integer which, multiplied by 2 and increased by 1, results in the odd nonnegative integer. (Contributed by AV, 30-May-2020)

	Ref	Expression
Assertion	nn0onn0ex	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \exists m\in {\mathbb{N}}_{0}N=2m+1$$

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		simpr	$$⊢\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$$
3		oveq2	$$⊢m=\frac{N-1}{2}\to 2m=2\left(\frac{N-1}{2}\right)$$
4	3	oveq1d	$$⊢m=\frac{N-1}{2}\to 2m+1=2\left(\frac{N-1}{2}\right)+1$$
5	4	eqeq2d	$$⊢m=\frac{N-1}{2}\to \left(N=2m+1\leftrightarrow N=2\left(\frac{N-1}{2}\right)+1\right)$$
6	5	adantl	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)\wedge m=\frac{N-1}{2}\right)\to \left(N=2m+1\leftrightarrow N=2\left(\frac{N-1}{2}\right)+1\right)$$
7		nn0cn	$$⊢N\in {\mathbb{N}}_0\to N\in ℂ$$
8		peano2cnm	$$⊢N\in ℂ\to N-1\in ℂ$$
9	7 8	syl	$$⊢N\in {\mathbb{N}}_0\to N-1\in ℂ$$
10		2cnd	$$⊢N\in {\mathbb{N}}_0\to 2\in ℂ$$
11		2ne0	$$⊢2\ne 0$$
12	11	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\ne 0$$
13	9 10 12	divcan2d	$$⊢N\in {\mathbb{N}}_0\to 2\left(\frac{N-1}{2}\right)=N-1$$
14	13	oveq1d	$$⊢N\in {\mathbb{N}}_0\to 2\left(\frac{N-1}{2}\right)+1=N-1+1$$
15		npcan1	$$⊢N\in ℂ\to N-1+1=N$$
16	7 15	syl	$$⊢N\in {\mathbb{N}}_0\to N-1+1=N$$
17	14 16	eqtr2d	$$⊢N\in {\mathbb{N}}_0\to N=2\left(\frac{N-1}{2}\right)+1$$
18	17	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)\to N=2\left(\frac{N-1}{2}\right)+1$$
19	2 6 18	rspcedvd	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N-1}{2}\in {\mathbb{N}}_0\right)\to \exists m\in {\mathbb{N}}_{0}N=2m+1$$
20	1 19	syldan	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \exists m\in {\mathbb{N}}_{0}N=2m+1$$