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	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ∃ 𝑚 ∈ ℕ0 𝑁 = ( 2 · 𝑚 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 𝑁 / 2 ) ∈ ℕ0 )
2		oveq2	⊢ ( 𝑚 = ( 𝑁 / 2 ) → ( 2 · 𝑚 ) = ( 2 · ( 𝑁 / 2 ) ) )
3	2	adantl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) ∧ 𝑚 = ( 𝑁 / 2 ) ) → ( 2 · 𝑚 ) = ( 2 · ( 𝑁 / 2 ) ) )
4	3	eqeq2d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) ∧ 𝑚 = ( 𝑁 / 2 ) ) → ( 𝑁 = ( 2 · 𝑚 ) ↔ 𝑁 = ( 2 · ( 𝑁 / 2 ) ) ) )
5		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
6		2cnd	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℂ )
7		2ne0	⊢ 2 ≠ 0
8	7	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ≠ 0 )
9		divcan2	⊢ ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 · ( 𝑁 / 2 ) ) = 𝑁 )
10	9	eqcomd	⊢ ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → 𝑁 = ( 2 · ( 𝑁 / 2 ) ) )
11	5 6 8 10	syl3anc	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 = ( 2 · ( 𝑁 / 2 ) ) )
12	11	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → 𝑁 = ( 2 · ( 𝑁 / 2 ) ) )
13	1 4 12	rspcedvd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ∃ 𝑚 ∈ ℕ0 𝑁 = ( 2 · 𝑚 ) )