Metamath Proof Explorer

Theorem epee

Description: The sum of two even numbers is even. (Contributed by AV, 21-Jul-2020)

Ref Expression
Assertion epee ⊢ A ∈ Even ∧ B ∈ Even → A + B ∈ Even

Proof

Step Hyp Ref Expression
1 evenp1odd ⊢ A ∈ Even → A + 1 ∈ Odd
2 evenm1odd ⊢ B ∈ Even → B − 1 ∈ Odd
3 opoeALTV ⊢ A + 1 ∈ Odd ∧ B − 1 ∈ Odd → A + 1 + B − 1 ∈ Even
4 1 2 3 syl2an ⊢ A ∈ Even ∧ B ∈ Even → A + 1 + B − 1 ∈ Even
5 evenz ⊢ A ∈ Even → A ∈ ℤ
6 5 zcnd ⊢ A ∈ Even → A ∈ ℂ
7 6 adantr ⊢ A ∈ Even ∧ B ∈ Even → A ∈ ℂ
8 1cnd ⊢ A ∈ Even ∧ B ∈ Even → 1 ∈ ℂ
9 evenz ⊢ B ∈ Even → B ∈ ℤ
10 9 zcnd ⊢ B ∈ Even → B ∈ ℂ
11 10 adantl ⊢ A ∈ Even ∧ B ∈ Even → B ∈ ℂ
12 ppncan ⊢ A ∈ ℂ ∧ 1 ∈ ℂ ∧ B ∈ ℂ → A + 1 + B − 1 = A + B
13 12 eleq1d ⊢ A ∈ ℂ ∧ 1 ∈ ℂ ∧ B ∈ ℂ → A + 1 + B − 1 ∈ Even ↔ A + B ∈ Even
14 7 8 11 13 syl3anc ⊢ A ∈ Even ∧ B ∈ Even → A + 1 + B − 1 ∈ Even ↔ A + B ∈ Even
15 4 14 mpbid ⊢ A ∈ Even ∧ B ∈ Even → A + B ∈ Even