Theorem nn0enn0ex

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

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

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N}{2}\in {\mathbb{N}}_0\right)\to \frac{N}{2}\in {\mathbb{N}}_0$$
2		oveq2	$$⊢m=\frac{N}{2}\to 2m=2\left(\frac{N}{2}\right)$$
3	2	adantl	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge \frac{N}{2}\in {\mathbb{N}}_0\right)\wedge m=\frac{N}{2}\right)\to 2m=2\left(\frac{N}{2}\right)$$
4	3	eqeq2d	$$⊢\left(\left(N\in {\mathbb{N}}_0\wedge \frac{N}{2}\in {\mathbb{N}}_0\right)\wedge m=\frac{N}{2}\right)\to \left(N=2m\leftrightarrow N=2\left(\frac{N}{2}\right)\right)$$
5		nn0cn	$$⊢N\in {\mathbb{N}}_0\to N\in ℂ$$
6		2cnd	$$⊢N\in {\mathbb{N}}_0\to 2\in ℂ$$
7		2ne0	$$⊢2\ne 0$$
8	7	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\ne 0$$
9		divcan2	$$⊢\left(N\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to 2\left(\frac{N}{2}\right)=N$$
10	9	eqcomd	$$⊢\left(N\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to N=2\left(\frac{N}{2}\right)$$
11	5 6 8 10	syl3anc	$$⊢N\in {\mathbb{N}}_0\to N=2\left(\frac{N}{2}\right)$$
12	11	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N}{2}\in {\mathbb{N}}_0\right)\to N=2\left(\frac{N}{2}\right)$$
13	1 4 12	rspcedvd	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N}{2}\in {\mathbb{N}}_0\right)\to \exists m\in {\mathbb{N}}_{0}N=2m$$