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 ⊢ N ∈ ℕ ∧ N 2 ∈ ℕ → ∃ m ∈ ℕ N = 2 ⁢ m

Proof

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