Metamath Proof Explorer

Theorem epee

Description: The sum of two even numbers is even. (Contributed by AV, 21-Jul-2020)

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

Proof

Step Hyp Ref Expression
1 evenp1odd 
 |-  ( A e. Even -> ( A + 1 ) e. Odd )
2 evenm1odd 
 |-  ( B e. Even -> ( B - 1 ) e. Odd )
3 opoeALTV 
 |-  ( ( ( A + 1 ) e. Odd /\ ( B - 1 ) e. Odd ) -> ( ( A + 1 ) + ( B - 1 ) ) e. Even )
4 1 2 3 syl2an 
 |-  ( ( A e. Even /\ B e. Even ) -> ( ( A + 1 ) + ( B - 1 ) ) e. Even )
5 evenz 
 |-  ( A e. Even -> A e. ZZ )
6 5 zcnd 
 |-  ( A e. Even -> A e. CC )
7 6 adantr 
 |-  ( ( A e. Even /\ B e. Even ) -> A e. CC )
8 1cnd 
 |-  ( ( A e. Even /\ B e. Even ) -> 1 e. CC )
9 evenz 
 |-  ( B e. Even -> B e. ZZ )
10 9 zcnd 
 |-  ( B e. Even -> B e. CC )
11 10 adantl 
 |-  ( ( A e. Even /\ B e. Even ) -> B e. CC )
12 ppncan 
 |-  ( ( A e. CC /\ 1 e. CC /\ B e. CC ) -> ( ( A + 1 ) + ( B - 1 ) ) = ( A + B ) )
13 12 eleq1d 
 |-  ( ( A e. CC /\ 1 e. CC /\ B e. CC ) -> ( ( ( A + 1 ) + ( B - 1 ) ) e. Even <-> ( A + B ) e. Even ) )
14 7 8 11 13 syl3anc 
 |-  ( ( A e. Even /\ B e. Even ) -> ( ( ( A + 1 ) + ( B - 1 ) ) e. Even <-> ( A + B ) e. Even ) )
15 4 14 mpbid 
 |-  ( ( A e. Even /\ B e. Even ) -> ( A + B ) e. Even )