Theorem evennn02n

Description: A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021) (Proof shortened by AV, 10-Jul-2022)

	Ref	Expression
Assertion	evennn02n	$$⊢N\in {\mathbb{N}}_0\to \left(2\parallel N\leftrightarrow \exists n\in {\mathbb{N}}_{0}2n=N\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢2n=N\to \left(2n\in {\mathbb{N}}_0\leftrightarrow N\in {\mathbb{N}}_0\right)$$
2		simpr	$$⊢\left(2n\in {\mathbb{N}}_0\wedge n\in \mathbb{Z}\right)\to n\in \mathbb{Z}$$
3		2rp	$$⊢2\in {ℝ}^{+}$$
4	3	a1i	$$⊢\left(2n\in {\mathbb{N}}_0\wedge n\in \mathbb{Z}\right)\to 2\in {ℝ}^{+}$$
5		zre	$$⊢n\in \mathbb{Z}\to n\in ℝ$$
6	5	adantl	$$⊢\left(2n\in {\mathbb{N}}_0\wedge n\in \mathbb{Z}\right)\to n\in ℝ$$
7		nn0ge0	$$⊢2n\in {\mathbb{N}}_0\to 0\le 2n$$
8	7	adantr	$$⊢\left(2n\in {\mathbb{N}}_0\wedge n\in \mathbb{Z}\right)\to 0\le 2n$$
9	4 6 8	prodge0rd	$$⊢\left(2n\in {\mathbb{N}}_0\wedge n\in \mathbb{Z}\right)\to 0\le n$$
10		elnn0z	$$⊢n\in {\mathbb{N}}_0\leftrightarrow \left(n\in \mathbb{Z}\wedge 0\le n\right)$$
11	2 9 10	sylanbrc	$$⊢\left(2n\in {\mathbb{N}}_0\wedge n\in \mathbb{Z}\right)\to n\in {\mathbb{N}}_0$$
12	11	ex	$$⊢2n\in {\mathbb{N}}_0\to \left(n\in \mathbb{Z}\to n\in {\mathbb{N}}_0\right)$$
13	1 12	biimtrrdi	$$⊢2n=N\to \left(N\in {\mathbb{N}}_0\to \left(n\in \mathbb{Z}\to n\in {\mathbb{N}}_0\right)\right)$$
14	13	com13	$$⊢n\in \mathbb{Z}\to \left(N\in {\mathbb{N}}_0\to \left(2n=N\to n\in {\mathbb{N}}_0\right)\right)$$
15	14	impcom	$$⊢\left(N\in {\mathbb{N}}_0\wedge n\in \mathbb{Z}\right)\to \left(2n=N\to n\in {\mathbb{N}}_0\right)$$
16	15	pm4.71rd	$$⊢\left(N\in {\mathbb{N}}_0\wedge n\in \mathbb{Z}\right)\to \left(2n=N\leftrightarrow \left(n\in {\mathbb{N}}_0\wedge 2n=N\right)\right)$$
17	16	bicomd	$$⊢\left(N\in {\mathbb{N}}_0\wedge n\in \mathbb{Z}\right)\to \left(\left(n\in {\mathbb{N}}_0\wedge 2n=N\right)\leftrightarrow 2n=N\right)$$
18	17	rexbidva	$$⊢N\in {\mathbb{N}}_0\to \left(\exists n\in \mathbb{Z}\left(n\in {\mathbb{N}}_0\wedge 2n=N\right)\leftrightarrow \exists n\in \mathbb{Z}2n=N\right)$$
19		nn0ssz	$$⊢{\mathbb{N}}_0\subseteq \mathbb{Z}$$
20		rexss	$$⊢{\mathbb{N}}_0\subseteq \mathbb{Z}\to \left(\exists n\in {\mathbb{N}}_{0}2n=N\leftrightarrow \exists n\in \mathbb{Z}\left(n\in {\mathbb{N}}_0\wedge 2n=N\right)\right)$$
21	19 20	mp1i	$$⊢N\in {\mathbb{N}}_0\to \left(\exists n\in {\mathbb{N}}_{0}2n=N\leftrightarrow \exists n\in \mathbb{Z}\left(n\in {\mathbb{N}}_0\wedge 2n=N\right)\right)$$
22		even2n	$$⊢2\parallel N\leftrightarrow \exists n\in \mathbb{Z}2n=N$$
23	22	a1i	$$⊢N\in {\mathbb{N}}_0\to \left(2\parallel N\leftrightarrow \exists n\in \mathbb{Z}2n=N\right)$$
24	18 21 23	3bitr4rd	$$⊢N\in {\mathbb{N}}_0\to \left(2\parallel N\leftrightarrow \exists n\in {\mathbb{N}}_{0}2n=N\right)$$