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 e. Even /\ B e. Odd ) -> ( A + B ) e. Odd )

Proof

Step Hyp Ref Expression
1 evenz
 |-  ( A e. Even -> A e. ZZ )
2 1 zcnd
 |-  ( A e. Even -> A e. CC )
3 oddz
 |-  ( B e. Odd -> B e. ZZ )
4 3 zcnd
 |-  ( B e. Odd -> B e. CC )
5 addcom
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
6 2 4 5 syl2an
 |-  ( ( A e. Even /\ B e. Odd ) -> ( A + B ) = ( B + A ) )
7 opeoALTV
 |-  ( ( B e. Odd /\ A e. Even ) -> ( B + A ) e. Odd )
8 7 ancoms
 |-  ( ( A e. Even /\ B e. Odd ) -> ( B + A ) e. Odd )
9 6 8 eqeltrd
 |-  ( ( A e. Even /\ B e. Odd ) -> ( A + B ) e. Odd )