This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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