Metamath Proof Explorer


Theorem opeo

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

Ref Expression
Assertion opeo
|- ( ( ( 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 2z
 |-  2 e. ZZ
3 divides
 |-  ( ( 2 e. ZZ /\ B e. ZZ ) -> ( 2 || B <-> E. b e. ZZ ( b x. 2 ) = B ) )
4 2 3 mpan
 |-  ( B e. ZZ -> ( 2 || B <-> E. b e. ZZ ( b x. 2 ) = B ) )
5 1 4 bi2anan9
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( -. 2 || A /\ 2 || B ) <-> ( E. a e. ZZ ( ( 2 x. a ) + 1 ) = A /\ E. b e. ZZ ( b x. 2 ) = B ) ) )
6 reeanv
 |-  ( E. a e. ZZ E. b e. ZZ ( ( ( 2 x. a ) + 1 ) = A /\ ( b x. 2 ) = B ) <-> ( E. a e. ZZ ( ( 2 x. a ) + 1 ) = A /\ E. b e. ZZ ( b x. 2 ) = B ) )
7 zaddcl
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a + b ) e. ZZ )
8 zcn
 |-  ( a e. ZZ -> a e. CC )
9 zcn
 |-  ( b e. ZZ -> b e. CC )
10 2cn
 |-  2 e. CC
11 adddi
 |-  ( ( 2 e. CC /\ a e. CC /\ b e. CC ) -> ( 2 x. ( a + b ) ) = ( ( 2 x. a ) + ( 2 x. b ) ) )
12 10 11 mp3an1
 |-  ( ( a e. CC /\ b e. CC ) -> ( 2 x. ( a + b ) ) = ( ( 2 x. a ) + ( 2 x. b ) ) )
13 12 oveq1d
 |-  ( ( a e. CC /\ b e. CC ) -> ( ( 2 x. ( a + b ) ) + 1 ) = ( ( ( 2 x. a ) + ( 2 x. b ) ) + 1 ) )
14 mulcl
 |-  ( ( 2 e. CC /\ a e. CC ) -> ( 2 x. a ) e. CC )
15 10 14 mpan
 |-  ( a e. CC -> ( 2 x. a ) e. CC )
16 mulcl
 |-  ( ( 2 e. CC /\ b e. CC ) -> ( 2 x. b ) e. CC )
17 10 16 mpan
 |-  ( b e. CC -> ( 2 x. b ) e. CC )
18 ax-1cn
 |-  1 e. CC
19 add32
 |-  ( ( ( 2 x. a ) e. CC /\ ( 2 x. b ) e. CC /\ 1 e. CC ) -> ( ( ( 2 x. a ) + ( 2 x. b ) ) + 1 ) = ( ( ( 2 x. a ) + 1 ) + ( 2 x. b ) ) )
20 18 19 mp3an3
 |-  ( ( ( 2 x. a ) e. CC /\ ( 2 x. b ) e. CC ) -> ( ( ( 2 x. a ) + ( 2 x. b ) ) + 1 ) = ( ( ( 2 x. a ) + 1 ) + ( 2 x. b ) ) )
21 15 17 20 syl2an
 |-  ( ( a e. CC /\ b e. CC ) -> ( ( ( 2 x. a ) + ( 2 x. b ) ) + 1 ) = ( ( ( 2 x. a ) + 1 ) + ( 2 x. b ) ) )
22 mulcom
 |-  ( ( 2 e. CC /\ b e. CC ) -> ( 2 x. b ) = ( b x. 2 ) )
23 10 22 mpan
 |-  ( b e. CC -> ( 2 x. b ) = ( b x. 2 ) )
24 23 adantl
 |-  ( ( a e. CC /\ b e. CC ) -> ( 2 x. b ) = ( b x. 2 ) )
25 24 oveq2d
 |-  ( ( a e. CC /\ b e. CC ) -> ( ( ( 2 x. a ) + 1 ) + ( 2 x. b ) ) = ( ( ( 2 x. a ) + 1 ) + ( b x. 2 ) ) )
26 13 21 25 3eqtrd
 |-  ( ( a e. CC /\ b e. CC ) -> ( ( 2 x. ( a + b ) ) + 1 ) = ( ( ( 2 x. a ) + 1 ) + ( b x. 2 ) ) )
27 8 9 26 syl2an
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( ( 2 x. ( a + b ) ) + 1 ) = ( ( ( 2 x. a ) + 1 ) + ( b x. 2 ) ) )
28 oveq2
 |-  ( c = ( a + b ) -> ( 2 x. c ) = ( 2 x. ( a + b ) ) )
29 28 oveq1d
 |-  ( c = ( a + b ) -> ( ( 2 x. c ) + 1 ) = ( ( 2 x. ( a + b ) ) + 1 ) )
30 29 eqeq1d
 |-  ( c = ( a + b ) -> ( ( ( 2 x. c ) + 1 ) = ( ( ( 2 x. a ) + 1 ) + ( b x. 2 ) ) <-> ( ( 2 x. ( a + b ) ) + 1 ) = ( ( ( 2 x. a ) + 1 ) + ( b x. 2 ) ) ) )
31 30 rspcev
 |-  ( ( ( a + b ) e. ZZ /\ ( ( 2 x. ( a + b ) ) + 1 ) = ( ( ( 2 x. a ) + 1 ) + ( b x. 2 ) ) ) -> E. c e. ZZ ( ( 2 x. c ) + 1 ) = ( ( ( 2 x. a ) + 1 ) + ( b x. 2 ) ) )
32 7 27 31 syl2anc
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> E. c e. ZZ ( ( 2 x. c ) + 1 ) = ( ( ( 2 x. a ) + 1 ) + ( b x. 2 ) ) )
33 oveq12
 |-  ( ( ( ( 2 x. a ) + 1 ) = A /\ ( b x. 2 ) = B ) -> ( ( ( 2 x. a ) + 1 ) + ( b x. 2 ) ) = ( A + B ) )
34 33 eqeq2d
 |-  ( ( ( ( 2 x. a ) + 1 ) = A /\ ( b x. 2 ) = B ) -> ( ( ( 2 x. c ) + 1 ) = ( ( ( 2 x. a ) + 1 ) + ( b x. 2 ) ) <-> ( ( 2 x. c ) + 1 ) = ( A + B ) ) )
35 34 rexbidv
 |-  ( ( ( ( 2 x. a ) + 1 ) = A /\ ( b x. 2 ) = B ) -> ( E. c e. ZZ ( ( 2 x. c ) + 1 ) = ( ( ( 2 x. a ) + 1 ) + ( b x. 2 ) ) <-> E. c e. ZZ ( ( 2 x. c ) + 1 ) = ( A + B ) ) )
36 32 35 syl5ibcom
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( ( ( ( 2 x. a ) + 1 ) = A /\ ( b x. 2 ) = B ) -> E. c e. ZZ ( ( 2 x. c ) + 1 ) = ( A + B ) ) )
37 36 rexlimivv
 |-  ( E. a e. ZZ E. b e. ZZ ( ( ( 2 x. a ) + 1 ) = A /\ ( b x. 2 ) = B ) -> E. c e. ZZ ( ( 2 x. c ) + 1 ) = ( A + B ) )
38 6 37 sylbir
 |-  ( ( E. a e. ZZ ( ( 2 x. a ) + 1 ) = A /\ E. b e. ZZ ( b x. 2 ) = B ) -> E. c e. ZZ ( ( 2 x. c ) + 1 ) = ( A + B ) )
39 5 38 syl6bi
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( -. 2 || A /\ 2 || B ) -> E. c e. ZZ ( ( 2 x. c ) + 1 ) = ( A + B ) ) )
40 39 imp
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( -. 2 || A /\ 2 || B ) ) -> E. c e. ZZ ( ( 2 x. c ) + 1 ) = ( A + B ) )
41 40 an4s
 |-  ( ( ( A e. ZZ /\ -. 2 || A ) /\ ( B e. ZZ /\ 2 || B ) ) -> E. c e. ZZ ( ( 2 x. c ) + 1 ) = ( A + B ) )
42 zaddcl
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. ZZ )
43 42 ad2ant2r
 |-  ( ( ( A e. ZZ /\ -. 2 || A ) /\ ( B e. ZZ /\ 2 || B ) ) -> ( A + B ) e. ZZ )
44 odd2np1
 |-  ( ( A + B ) e. ZZ -> ( -. 2 || ( A + B ) <-> E. c e. ZZ ( ( 2 x. c ) + 1 ) = ( A + B ) ) )
45 43 44 syl
 |-  ( ( ( A e. ZZ /\ -. 2 || A ) /\ ( B e. ZZ /\ 2 || B ) ) -> ( -. 2 || ( A + B ) <-> E. c e. ZZ ( ( 2 x. c ) + 1 ) = ( A + B ) ) )
46 41 45 mpbird
 |-  ( ( ( A e. ZZ /\ -. 2 || A ) /\ ( B e. ZZ /\ 2 || B ) ) -> -. 2 || ( A + B ) )