Metamath Proof Explorer

Theorem opoe

Description: The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion opoe 
|- ( ( ( A e. ZZ /\ -. 2 || A ) /\ ( B e. ZZ /\ -. 2 || B ) ) -> 2 || ( A + B ) )

Proof

Step Hyp Ref Expression
1 odd2np1 
 |-  ( A e. ZZ -> ( -. 2 || A <-> E. a e. ZZ ( ( 2 x. a ) + 1 ) = A ) )
2 odd2np1 
 |-  ( B e. ZZ -> ( -. 2 || B <-> E. b e. ZZ ( ( 2 x. b ) + 1 ) = B ) )
3 1 2 bi2anan9 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( -. 2 || A /\ -. 2 || B ) <-> ( E. a e. ZZ ( ( 2 x. a ) + 1 ) = A /\ E. b e. ZZ ( ( 2 x. b ) + 1 ) = B ) ) )
4 reeanv 
 |-  ( E. a e. ZZ E. b e. ZZ ( ( ( 2 x. a ) + 1 ) = A /\ ( ( 2 x. b ) + 1 ) = B ) <-> ( E. a e. ZZ ( ( 2 x. a ) + 1 ) = A /\ E. b e. ZZ ( ( 2 x. b ) + 1 ) = B ) )
5 2z 
 |-  2 e. ZZ
6 zaddcl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a + b ) e. ZZ )
7 6 peano2zd 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( ( a + b ) + 1 ) e. ZZ )
8 dvdsmul1 
 |-  ( ( 2 e. ZZ /\ ( ( a + b ) + 1 ) e. ZZ ) -> 2 || ( 2 x. ( ( a + b ) + 1 ) ) )
9 5 7 8 sylancr 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> 2 || ( 2 x. ( ( a + b ) + 1 ) ) )
10 zcn 
 |-  ( a e. ZZ -> a e. CC )
11 zcn 
 |-  ( b e. ZZ -> b e. CC )
12 addcl 
 |-  ( ( a e. CC /\ b e. CC ) -> ( a + b ) e. CC )
13 2cn 
 |-  2 e. CC
14 ax-1cn 
 |-  1 e. CC
15 adddi 
 |-  ( ( 2 e. CC /\ ( a + b ) e. CC /\ 1 e. CC ) -> ( 2 x. ( ( a + b ) + 1 ) ) = ( ( 2 x. ( a + b ) ) + ( 2 x. 1 ) ) )
16 13 14 15 mp3an13 
 |-  ( ( a + b ) e. CC -> ( 2 x. ( ( a + b ) + 1 ) ) = ( ( 2 x. ( a + b ) ) + ( 2 x. 1 ) ) )
17 12 16 syl 
 |-  ( ( a e. CC /\ b e. CC ) -> ( 2 x. ( ( a + b ) + 1 ) ) = ( ( 2 x. ( a + b ) ) + ( 2 x. 1 ) ) )
18 adddi 
 |-  ( ( 2 e. CC /\ a e. CC /\ b e. CC ) -> ( 2 x. ( a + b ) ) = ( ( 2 x. a ) + ( 2 x. b ) ) )
19 13 18 mp3an1 
 |-  ( ( a e. CC /\ b e. CC ) -> ( 2 x. ( a + b ) ) = ( ( 2 x. a ) + ( 2 x. b ) ) )
20 19 oveq1d 
 |-  ( ( a e. CC /\ b e. CC ) -> ( ( 2 x. ( a + b ) ) + ( 2 x. 1 ) ) = ( ( ( 2 x. a ) + ( 2 x. b ) ) + ( 2 x. 1 ) ) )
21 17 20 eqtrd 
 |-  ( ( a e. CC /\ b e. CC ) -> ( 2 x. ( ( a + b ) + 1 ) ) = ( ( ( 2 x. a ) + ( 2 x. b ) ) + ( 2 x. 1 ) ) )
22 2t1e2 
 |-  ( 2 x. 1 ) = 2
23 df-2 
 |-  2 = ( 1 + 1 )
24 22 23 eqtri 
 |-  ( 2 x. 1 ) = ( 1 + 1 )
25 24 oveq2i 
 |-  ( ( ( 2 x. a ) + ( 2 x. b ) ) + ( 2 x. 1 ) ) = ( ( ( 2 x. a ) + ( 2 x. b ) ) + ( 1 + 1 ) )
26 21 25 eqtrdi 
 |-  ( ( a e. CC /\ b e. CC ) -> ( 2 x. ( ( a + b ) + 1 ) ) = ( ( ( 2 x. a ) + ( 2 x. b ) ) + ( 1 + 1 ) ) )
27 mulcl 
 |-  ( ( 2 e. CC /\ a e. CC ) -> ( 2 x. a ) e. CC )
28 13 27 mpan 
 |-  ( a e. CC -> ( 2 x. a ) e. CC )
29 mulcl 
 |-  ( ( 2 e. CC /\ b e. CC ) -> ( 2 x. b ) e. CC )
30 13 29 mpan 
 |-  ( b e. CC -> ( 2 x. b ) e. CC )
31 add4 
 |-  ( ( ( ( 2 x. a ) e. CC /\ ( 2 x. b ) e. CC ) /\ ( 1 e. CC /\ 1 e. CC ) ) -> ( ( ( 2 x. a ) + ( 2 x. b ) ) + ( 1 + 1 ) ) = ( ( ( 2 x. a ) + 1 ) + ( ( 2 x. b ) + 1 ) ) )
32 14 14 31 mpanr12 
 |-  ( ( ( 2 x. a ) e. CC /\ ( 2 x. b ) e. CC ) -> ( ( ( 2 x. a ) + ( 2 x. b ) ) + ( 1 + 1 ) ) = ( ( ( 2 x. a ) + 1 ) + ( ( 2 x. b ) + 1 ) ) )
33 28 30 32 syl2an 
 |-  ( ( a e. CC /\ b e. CC ) -> ( ( ( 2 x. a ) + ( 2 x. b ) ) + ( 1 + 1 ) ) = ( ( ( 2 x. a ) + 1 ) + ( ( 2 x. b ) + 1 ) ) )
34 26 33 eqtrd 
 |-  ( ( a e. CC /\ b e. CC ) -> ( 2 x. ( ( a + b ) + 1 ) ) = ( ( ( 2 x. a ) + 1 ) + ( ( 2 x. b ) + 1 ) ) )
35 10 11 34 syl2an 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( 2 x. ( ( a + b ) + 1 ) ) = ( ( ( 2 x. a ) + 1 ) + ( ( 2 x. b ) + 1 ) ) )
36 9 35 breqtrd 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> 2 || ( ( ( 2 x. a ) + 1 ) + ( ( 2 x. b ) + 1 ) ) )
37 oveq12 
 |-  ( ( ( ( 2 x. a ) + 1 ) = A /\ ( ( 2 x. b ) + 1 ) = B ) -> ( ( ( 2 x. a ) + 1 ) + ( ( 2 x. b ) + 1 ) ) = ( A + B ) )
38 37 breq2d 
 |-  ( ( ( ( 2 x. a ) + 1 ) = A /\ ( ( 2 x. b ) + 1 ) = B ) -> ( 2 || ( ( ( 2 x. a ) + 1 ) + ( ( 2 x. b ) + 1 ) ) <-> 2 || ( A + B ) ) )
39 36 38 syl5ibcom 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( ( ( ( 2 x. a ) + 1 ) = A /\ ( ( 2 x. b ) + 1 ) = B ) -> 2 || ( A + B ) ) )
40 39 rexlimivv 
 |-  ( E. a e. ZZ E. b e. ZZ ( ( ( 2 x. a ) + 1 ) = A /\ ( ( 2 x. b ) + 1 ) = B ) -> 2 || ( A + B ) )
41 4 40 sylbir 
 |-  ( ( E. a e. ZZ ( ( 2 x. a ) + 1 ) = A /\ E. b e. ZZ ( ( 2 x. b ) + 1 ) = B ) -> 2 || ( A + B ) )
42 3 41 syl6bi 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( -. 2 || A /\ -. 2 || B ) -> 2 || ( A + B ) ) )
43 42 imp 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( -. 2 || A /\ -. 2 || B ) ) -> 2 || ( A + B ) )
44 43 an4s 
 |-  ( ( ( A e. ZZ /\ -. 2 || A ) /\ ( B e. ZZ /\ -. 2 || B ) ) -> 2 || ( A + B ) )