Metamath Proof Explorer


Theorem emee

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

Ref Expression
Assertion emee AEvenBEvenABEven

Proof

Step Hyp Ref Expression
1 evenz AEvenA
2 1 zcnd AEvenA
3 evenz BEvenB
4 3 zcnd BEvenB
5 negsub ABA+B=AB
6 2 4 5 syl2an AEvenBEvenA+B=AB
7 enege BEvenBEven
8 epee AEvenBEvenA+BEven
9 7 8 sylan2 AEvenBEvenA+BEven
10 6 9 eqeltrrd AEvenBEvenABEven