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

Proof

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