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 ) |
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 ) |