Metamath Proof Explorer

Theorem nnennex

Description: For each even positive integer there is a positive integer which, multiplied by 2, results in the even positive integer. (Contributed by AV, 5-Jun-2023)

		Ref	Expression
	Assertion	nnennex	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ) \to \exists m \in ℕ N = 2 m$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ) \to \frac{N}{2} \in ℕ$
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 ℕ \land \frac{N}{2} \in ℕ) \land m = \frac{N}{2}) \to (N = 2 m \leftrightarrow N = 2 (\frac{N}{2}))$
5		nncn	$⊢ N \in ℕ \to N \in ℂ$
6		2cnd	$⊢ N \in ℕ \to 2 \in ℂ$
7		2ne0	$⊢ 2 \neq 0$
8	7	a1i	$⊢ N \in ℕ \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 ℕ \to N = 2 (\frac{N}{2})$
12	11	adantr	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ) \to N = 2 (\frac{N}{2})$
13	1 4 12	rspcedvd	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ) \to \exists m \in ℕ N = 2 m$