Metamath Proof Explorer


Theorem epoo

Description: The sum of an even and an odd is odd. (Contributed by AV, 24-Jul-2020)

Ref Expression
Assertion epoo A Even B Odd A + B Odd

Proof

Step Hyp Ref Expression
1 evenz A Even A
2 1 zcnd A Even A
3 oddz B Odd B
4 3 zcnd B Odd B
5 addcom A B A + B = B + A
6 2 4 5 syl2an A Even B Odd A + B = B + A
7 opeoALTV B Odd A Even B + A Odd
8 7 ancoms A Even B Odd B + A Odd
9 6 8 eqeltrd A Even B Odd A + B Odd