Metamath Proof Explorer


Theorem emee

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

Ref Expression
Assertion emee ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → ( 𝐴𝐵 ) ∈ Even )

Proof

Step Hyp Ref Expression
1 evenz ( 𝐴 ∈ Even → 𝐴 ∈ ℤ )
2 1 zcnd ( 𝐴 ∈ Even → 𝐴 ∈ ℂ )
3 evenz ( 𝐵 ∈ Even → 𝐵 ∈ ℤ )
4 3 zcnd ( 𝐵 ∈ Even → 𝐵 ∈ ℂ )
5 negsub ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴𝐵 ) )
6 2 4 5 syl2an ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → ( 𝐴 + - 𝐵 ) = ( 𝐴𝐵 ) )
7 enege ( 𝐵 ∈ Even → - 𝐵 ∈ Even )
8 epee ( ( 𝐴 ∈ Even ∧ - 𝐵 ∈ Even ) → ( 𝐴 + - 𝐵 ) ∈ Even )
9 7 8 sylan2 ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → ( 𝐴 + - 𝐵 ) ∈ Even )
10 6 9 eqeltrrd ( ( 𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → ( 𝐴𝐵 ) ∈ Even )