This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 · 𝑚 ) )