Metamath Proof Explorer

Theorem nn0enn0exALTV

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) (Revised by AV, 22-Jun-2020)

		Ref	Expression
	Assertion	nn0enn0exALTV	$⊢ (N \in ℕ_{0} \land N \in Even) \to \exists m \in ℕ_{0} N = 2 m$

Proof

Step	Hyp	Ref	Expression
1		nn0e	$⊢ (N \in ℕ_{0} \land N \in Even) \to \frac{N}{2} \in ℕ_{0}$
2		oveq2	$⊢ m = \frac{N}{2} \to 2 m = 2 (\frac{N}{2})$
3	2	eqeq2d	$⊢ m = \frac{N}{2} \to (N = 2 m \leftrightarrow N = 2 (\frac{N}{2}))$
4	3	adantl	$⊢ ((N \in ℕ_{0} \land N \in Even) \land m = \frac{N}{2}) \to (N = 2 m \leftrightarrow N = 2 (\frac{N}{2}))$
5		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
6		2cnd	$⊢ N \in ℕ_{0} \to 2 \in ℂ$
7		2ne0	$⊢ 2 \neq 0$
8	7	a1i	$⊢ N \in ℕ_{0} \to 2 \neq 0$
9		divcan2	$⊢ (N \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to 2 (\frac{N}{2}) = N$
10	9	eqcomd	$⊢ (N \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to N = 2 (\frac{N}{2})$
11	5 6 8 10	syl3anc	$⊢ N \in ℕ_{0} \to N = 2 (\frac{N}{2})$
12	11	adantr	$⊢ (N \in ℕ_{0} \land N \in Even) \to N = 2 (\frac{N}{2})$
13	1 4 12	rspcedvd	$⊢ (N \in ℕ_{0} \land N \in Even) \to \exists m \in ℕ_{0} N = 2 m$