Metamath Proof Explorer

Theorem omeo

Description: The difference 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 omeo 
|- ( ( ( 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 zsubcl 
 |-  ( ( 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 subdi 
 |-  ( ( 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 addsub 
 |-  ( ( ( 2 x. a ) e. CC /\ 1 e. CC /\ ( 2 x. b ) e. CC ) -> ( ( ( 2 x. a ) + 1 ) - ( 2 x. b ) ) = ( ( ( 2 x. a ) - ( 2 x. b ) ) + 1 ) )
20 18 19 mp3an2 
 |-  ( ( ( 2 x. a ) e. CC /\ ( 2 x. b ) e. CC ) -> ( ( ( 2 x. a ) + 1 ) - ( 2 x. b ) ) = ( ( ( 2 x. a ) - ( 2 x. b ) ) + 1 ) )
21 15 17 20 syl2an 
 |-  ( ( a e. CC /\ b e. CC ) -> ( ( ( 2 x. a ) + 1 ) - ( 2 x. b ) ) = ( ( ( 2 x. a ) - ( 2 x. b ) ) + 1 ) )
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 oveq2d 
 |-  ( b e. CC -> ( ( ( 2 x. a ) + 1 ) - ( 2 x. b ) ) = ( ( ( 2 x. a ) + 1 ) - ( b x. 2 ) ) )
25 24 adantl 
 |-  ( ( a e. CC /\ b e. CC ) -> ( ( ( 2 x. a ) + 1 ) - ( 2 x. b ) ) = ( ( ( 2 x. a ) + 1 ) - ( b x. 2 ) ) )
26 13 21 25 3eqtr2d 
 |-  ( ( 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 zsubcl 
 |-  ( ( 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 ) )