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 ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 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 · 𝑚 ) )