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

Proof

Step Hyp Ref Expression
1 nn0e ( ( 𝑁 ∈ ℕ0𝑁 ∈ Even ) → ( 𝑁 / 2 ) ∈ ℕ0 )
2 oveq2 ( 𝑚 = ( 𝑁 / 2 ) → ( 2 · 𝑚 ) = ( 2 · ( 𝑁 / 2 ) ) )
3 2 eqeq2d ( 𝑚 = ( 𝑁 / 2 ) → ( 𝑁 = ( 2 · 𝑚 ) ↔ 𝑁 = ( 2 · ( 𝑁 / 2 ) ) ) )
4 3 adantl ( ( ( 𝑁 ∈ ℕ0𝑁 ∈ Even ) ∧ 𝑚 = ( 𝑁 / 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𝑁 ∈ Even ) → 𝑁 = ( 2 · ( 𝑁 / 2 ) ) )
13 1 4 12 rspcedvd ( ( 𝑁 ∈ ℕ0𝑁 ∈ Even ) → ∃ 𝑚 ∈ ℕ0 𝑁 = ( 2 · 𝑚 ) )