Theorem evensumeven

Description: If a summand is even, the other summand is even iff the sum is even. (Contributed by AV, 21-Jul-2020)

	Ref	Expression
Assertion	evensumeven	|- ( ( A e. ZZ /\ B e. Even ) -> ( A e. Even <-> ( A + B ) e. Even ) )

Proof

Step	Hyp	Ref	Expression
1		epee	|- ( ( A e. Even /\ B e. Even ) -> ( A + B ) e. Even )
2	1	expcom	|- ( B e. Even -> ( A e. Even -> ( A + B ) e. Even ) )
3	2	adantl	|- ( ( A e. ZZ /\ B e. Even ) -> ( A e. Even -> ( A + B ) e. Even ) )
4		zcn	|- ( A e. ZZ -> A e. CC )
5		evenz	|- ( B e. Even -> B e. ZZ )
6	5	zcnd	|- ( B e. Even -> B e. CC )
7		pncan	|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - B ) = A )
8	4 6 7	syl2an	|- ( ( A e. ZZ /\ B e. Even ) -> ( ( A + B ) - B ) = A )
9	8	adantr	|- ( ( ( A e. ZZ /\ B e. Even ) /\ ( A + B ) e. Even ) -> ( ( A + B ) - B ) = A )
10		simpr	|- ( ( A e. ZZ /\ B e. Even ) -> B e. Even )
11	10	anim1i	|- ( ( ( A e. ZZ /\ B e. Even ) /\ ( A + B ) e. Even ) -> ( B e. Even /\ ( A + B ) e. Even ) )
12	11	ancomd	|- ( ( ( A e. ZZ /\ B e. Even ) /\ ( A + B ) e. Even ) -> ( ( A + B ) e. Even /\ B e. Even ) )
13		emee	|- ( ( ( A + B ) e. Even /\ B e. Even ) -> ( ( A + B ) - B ) e. Even )
14	12 13	syl	|- ( ( ( A e. ZZ /\ B e. Even ) /\ ( A + B ) e. Even ) -> ( ( A + B ) - B ) e. Even )
15	9 14	eqeltrrd	|- ( ( ( A e. ZZ /\ B e. Even ) /\ ( A + B ) e. Even ) -> A e. Even )
16	15	ex	|- ( ( A e. ZZ /\ B e. Even ) -> ( ( A + B ) e. Even -> A e. Even ) )
17	3 16	impbid	|- ( ( A e. ZZ /\ B e. Even ) -> ( A e. Even <-> ( A + B ) e. Even ) )