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 )