Metamath Proof Explorer

Theorem emee

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

Ref Expression
Assertion emee ⊢ A ∈ Even ∧ B ∈ Even → A − B ∈ Even

Proof

Step Hyp Ref Expression
1 evenz ⊢ A ∈ Even → A ∈ ℤ
2 1 zcnd ⊢ A ∈ Even → A ∈ ℂ
3 evenz ⊢ B ∈ Even → B ∈ ℤ
4 3 zcnd ⊢ B ∈ Even → B ∈ ℂ
5 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
6 2 4 5 syl2an ⊢ A ∈ Even ∧ B ∈ Even → A + − B = A − B
7 enege ⊢ B ∈ Even → − B ∈ Even
8 epee ⊢ A ∈ Even ∧ − B ∈ Even → A + − B ∈ Even
9 7 8 sylan2 ⊢ A ∈ Even ∧ B ∈ Even → A + − B ∈ Even
10 6 9 eqeltrrd ⊢ A ∈ Even ∧ B ∈ Even → A − B ∈ Even