Metamath Proof Explorer

Theorem opoeALTV

Description: The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014) (Revised by AV, 20-Jun-2020)

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

Proof

Step Hyp Ref Expression
1 oddz 
 |-  ( A e. Odd -> A e. ZZ )
2 oddz 
 |-  ( B e. Odd -> B e. ZZ )
3 zaddcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. ZZ )
4 1 2 3 syl2an 
 |-  ( ( A e. Odd /\ B e. Odd ) -> ( A + B ) e. ZZ )
5 eqeq1 
 |-  ( a = A -> ( a = ( ( 2 x. i ) + 1 ) <-> A = ( ( 2 x. i ) + 1 ) ) )
6 5 rexbidv 
 |-  ( a = A -> ( E. i e. ZZ a = ( ( 2 x. i ) + 1 ) <-> E. i e. ZZ A = ( ( 2 x. i ) + 1 ) ) )
7 dfodd6 
 |-  Odd = { a e. ZZ | E. i e. ZZ a = ( ( 2 x. i ) + 1 ) }
8 6 7 elrab2 
 |-  ( A e. Odd <-> ( A e. ZZ /\ E. i e. ZZ A = ( ( 2 x. i ) + 1 ) ) )
9 eqeq1 
 |-  ( b = B -> ( b = ( ( 2 x. j ) + 1 ) <-> B = ( ( 2 x. j ) + 1 ) ) )
10 9 rexbidv 
 |-  ( b = B -> ( E. j e. ZZ b = ( ( 2 x. j ) + 1 ) <-> E. j e. ZZ B = ( ( 2 x. j ) + 1 ) ) )
11 dfodd6 
 |-  Odd = { b e. ZZ | E. j e. ZZ b = ( ( 2 x. j ) + 1 ) }
12 10 11 elrab2 
 |-  ( B e. Odd <-> ( B e. ZZ /\ E. j e. ZZ B = ( ( 2 x. j ) + 1 ) ) )
13 zaddcl 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> ( i + j ) e. ZZ )
14 13 ex 
 |-  ( i e. ZZ -> ( j e. ZZ -> ( i + j ) e. ZZ ) )
15 14 ad3antlr 
 |-  ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) -> ( j e. ZZ -> ( i + j ) e. ZZ ) )
16 15 imp 
 |-  ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) -> ( i + j ) e. ZZ )
17 16 adantr 
 |-  ( ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) /\ B = ( ( 2 x. j ) + 1 ) ) -> ( i + j ) e. ZZ )
18 17 peano2zd 
 |-  ( ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) /\ B = ( ( 2 x. j ) + 1 ) ) -> ( ( i + j ) + 1 ) e. ZZ )
19 oveq2 
 |-  ( n = ( ( i + j ) + 1 ) -> ( 2 x. n ) = ( 2 x. ( ( i + j ) + 1 ) ) )
20 19 eqeq2d 
 |-  ( n = ( ( i + j ) + 1 ) -> ( ( A + B ) = ( 2 x. n ) <-> ( A + B ) = ( 2 x. ( ( i + j ) + 1 ) ) ) )
21 20 adantl 
 |-  ( ( ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) /\ B = ( ( 2 x. j ) + 1 ) ) /\ n = ( ( i + j ) + 1 ) ) -> ( ( A + B ) = ( 2 x. n ) <-> ( A + B ) = ( 2 x. ( ( i + j ) + 1 ) ) ) )
22 oveq12 
 |-  ( ( A = ( ( 2 x. i ) + 1 ) /\ B = ( ( 2 x. j ) + 1 ) ) -> ( A + B ) = ( ( ( 2 x. i ) + 1 ) + ( ( 2 x. j ) + 1 ) ) )
23 22 ex 
 |-  ( A = ( ( 2 x. i ) + 1 ) -> ( B = ( ( 2 x. j ) + 1 ) -> ( A + B ) = ( ( ( 2 x. i ) + 1 ) + ( ( 2 x. j ) + 1 ) ) ) )
24 23 ad3antlr 
 |-  ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) -> ( B = ( ( 2 x. j ) + 1 ) -> ( A + B ) = ( ( ( 2 x. i ) + 1 ) + ( ( 2 x. j ) + 1 ) ) ) )
25 24 imp 
 |-  ( ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) /\ B = ( ( 2 x. j ) + 1 ) ) -> ( A + B ) = ( ( ( 2 x. i ) + 1 ) + ( ( 2 x. j ) + 1 ) ) )
26 zcn 
 |-  ( i e. ZZ -> i e. CC )
27 zcn 
 |-  ( j e. ZZ -> j e. CC )
28 2cnd 
 |-  ( j e. CC -> 2 e. CC )
29 28 anim1i 
 |-  ( ( j e. CC /\ i e. CC ) -> ( 2 e. CC /\ i e. CC ) )
30 29 ancoms 
 |-  ( ( i e. CC /\ j e. CC ) -> ( 2 e. CC /\ i e. CC ) )
31 mulcl 
 |-  ( ( 2 e. CC /\ i e. CC ) -> ( 2 x. i ) e. CC )
32 30 31 syl 
 |-  ( ( i e. CC /\ j e. CC ) -> ( 2 x. i ) e. CC )
33 1cnd 
 |-  ( ( i e. CC /\ j e. CC ) -> 1 e. CC )
34 2cnd 
 |-  ( i e. CC -> 2 e. CC )
35 mulcl 
 |-  ( ( 2 e. CC /\ j e. CC ) -> ( 2 x. j ) e. CC )
36 34 35 sylan 
 |-  ( ( i e. CC /\ j e. CC ) -> ( 2 x. j ) e. CC )
37 32 33 36 33 add4d 
 |-  ( ( i e. CC /\ j e. CC ) -> ( ( ( 2 x. i ) + 1 ) + ( ( 2 x. j ) + 1 ) ) = ( ( ( 2 x. i ) + ( 2 x. j ) ) + ( 1 + 1 ) ) )
38 2cnd 
 |-  ( ( i e. CC /\ j e. CC ) -> 2 e. CC )
39 simpl 
 |-  ( ( i e. CC /\ j e. CC ) -> i e. CC )
40 simpr 
 |-  ( ( i e. CC /\ j e. CC ) -> j e. CC )
41 38 39 40 adddid 
 |-  ( ( i e. CC /\ j e. CC ) -> ( 2 x. ( i + j ) ) = ( ( 2 x. i ) + ( 2 x. j ) ) )
42 41 oveq1d 
 |-  ( ( i e. CC /\ j e. CC ) -> ( ( 2 x. ( i + j ) ) + ( 2 x. 1 ) ) = ( ( ( 2 x. i ) + ( 2 x. j ) ) + ( 2 x. 1 ) ) )
43 addcl 
 |-  ( ( i e. CC /\ j e. CC ) -> ( i + j ) e. CC )
44 38 43 33 adddid 
 |-  ( ( i e. CC /\ j e. CC ) -> ( 2 x. ( ( i + j ) + 1 ) ) = ( ( 2 x. ( i + j ) ) + ( 2 x. 1 ) ) )
45 1p1e2 
 |-  ( 1 + 1 ) = 2
46 2t1e2 
 |-  ( 2 x. 1 ) = 2
47 45 46 eqtr4i 
 |-  ( 1 + 1 ) = ( 2 x. 1 )
48 47 a1i 
 |-  ( ( i e. CC /\ j e. CC ) -> ( 1 + 1 ) = ( 2 x. 1 ) )
49 48 oveq2d 
 |-  ( ( i e. CC /\ j e. CC ) -> ( ( ( 2 x. i ) + ( 2 x. j ) ) + ( 1 + 1 ) ) = ( ( ( 2 x. i ) + ( 2 x. j ) ) + ( 2 x. 1 ) ) )
50 42 44 49 3eqtr4rd 
 |-  ( ( i e. CC /\ j e. CC ) -> ( ( ( 2 x. i ) + ( 2 x. j ) ) + ( 1 + 1 ) ) = ( 2 x. ( ( i + j ) + 1 ) ) )
51 37 50 eqtrd 
 |-  ( ( i e. CC /\ j e. CC ) -> ( ( ( 2 x. i ) + 1 ) + ( ( 2 x. j ) + 1 ) ) = ( 2 x. ( ( i + j ) + 1 ) ) )
52 26 27 51 syl2an 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> ( ( ( 2 x. i ) + 1 ) + ( ( 2 x. j ) + 1 ) ) = ( 2 x. ( ( i + j ) + 1 ) ) )
53 52 ex 
 |-  ( i e. ZZ -> ( j e. ZZ -> ( ( ( 2 x. i ) + 1 ) + ( ( 2 x. j ) + 1 ) ) = ( 2 x. ( ( i + j ) + 1 ) ) ) )
54 53 ad3antlr 
 |-  ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) -> ( j e. ZZ -> ( ( ( 2 x. i ) + 1 ) + ( ( 2 x. j ) + 1 ) ) = ( 2 x. ( ( i + j ) + 1 ) ) ) )
55 54 imp 
 |-  ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) -> ( ( ( 2 x. i ) + 1 ) + ( ( 2 x. j ) + 1 ) ) = ( 2 x. ( ( i + j ) + 1 ) ) )
56 55 adantr 
 |-  ( ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) /\ B = ( ( 2 x. j ) + 1 ) ) -> ( ( ( 2 x. i ) + 1 ) + ( ( 2 x. j ) + 1 ) ) = ( 2 x. ( ( i + j ) + 1 ) ) )
57 25 56 eqtrd 
 |-  ( ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) /\ B = ( ( 2 x. j ) + 1 ) ) -> ( A + B ) = ( 2 x. ( ( i + j ) + 1 ) ) )
58 18 21 57 rspcedvd 
 |-  ( ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) /\ B = ( ( 2 x. j ) + 1 ) ) -> E. n e. ZZ ( A + B ) = ( 2 x. n ) )
59 58 rexlimdva2 
 |-  ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) -> ( E. j e. ZZ B = ( ( 2 x. j ) + 1 ) -> E. n e. ZZ ( A + B ) = ( 2 x. n ) ) )
60 59 expimpd 
 |-  ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) -> ( ( B e. ZZ /\ E. j e. ZZ B = ( ( 2 x. j ) + 1 ) ) -> E. n e. ZZ ( A + B ) = ( 2 x. n ) ) )
61 60 rexlimdva2 
 |-  ( A e. ZZ -> ( E. i e. ZZ A = ( ( 2 x. i ) + 1 ) -> ( ( B e. ZZ /\ E. j e. ZZ B = ( ( 2 x. j ) + 1 ) ) -> E. n e. ZZ ( A + B ) = ( 2 x. n ) ) ) )
62 61 imp 
 |-  ( ( A e. ZZ /\ E. i e. ZZ A = ( ( 2 x. i ) + 1 ) ) -> ( ( B e. ZZ /\ E. j e. ZZ B = ( ( 2 x. j ) + 1 ) ) -> E. n e. ZZ ( A + B ) = ( 2 x. n ) ) )
63 12 62 biimtrid 
 |-  ( ( A e. ZZ /\ E. i e. ZZ A = ( ( 2 x. i ) + 1 ) ) -> ( B e. Odd -> E. n e. ZZ ( A + B ) = ( 2 x. n ) ) )
64 8 63 sylbi 
 |-  ( A e. Odd -> ( B e. Odd -> E. n e. ZZ ( A + B ) = ( 2 x. n ) ) )
65 64 imp 
 |-  ( ( A e. Odd /\ B e. Odd ) -> E. n e. ZZ ( A + B ) = ( 2 x. n ) )
66 eqeq1 
 |-  ( z = ( A + B ) -> ( z = ( 2 x. n ) <-> ( A + B ) = ( 2 x. n ) ) )
67 66 rexbidv 
 |-  ( z = ( A + B ) -> ( E. n e. ZZ z = ( 2 x. n ) <-> E. n e. ZZ ( A + B ) = ( 2 x. n ) ) )
68 dfeven4 
 |-  Even = { z e. ZZ | E. n e. ZZ z = ( 2 x. n ) }
69 67 68 elrab2 
 |-  ( ( A + B ) e. Even <-> ( ( A + B ) e. ZZ /\ E. n e. ZZ ( A + B ) = ( 2 x. n ) ) )
70 4 65 69 sylanbrc 
 |-  ( ( A e. Odd /\ B e. Odd ) -> ( A + B ) e. Even )