This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opeoALTV

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

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

Proof

Step Hyp Ref Expression
1 oddz 
 |-  ( A e. Odd -> A e. ZZ )
2 evenz 
 |-  ( B e. Even -> 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. Even ) -> ( 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 ) <-> B = ( 2 x. j ) ) )
10 9 rexbidv 
 |-  ( b = B -> ( E. j e. ZZ b = ( 2 x. j ) <-> E. j e. ZZ B = ( 2 x. j ) ) )
11 dfeven4 
 |-  Even = { b e. ZZ | E. j e. ZZ b = ( 2 x. j ) }
12 10 11 elrab2 
 |-  ( B e. Even <-> ( B e. ZZ /\ E. j e. ZZ B = ( 2 x. j ) ) )
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 ) ) -> ( i + j ) e. ZZ )
18 oveq2 
 |-  ( n = ( i + j ) -> ( 2 x. n ) = ( 2 x. ( i + j ) ) )
19 18 oveq1d 
 |-  ( n = ( i + j ) -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. ( i + j ) ) + 1 ) )
20 19 eqeq2d 
 |-  ( n = ( i + j ) -> ( ( A + B ) = ( ( 2 x. n ) + 1 ) <-> ( 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 ) ) /\ n = ( i + j ) ) -> ( ( A + B ) = ( ( 2 x. n ) + 1 ) <-> ( A + B ) = ( ( 2 x. ( i + j ) ) + 1 ) ) )
22 oveq12 
 |-  ( ( A = ( ( 2 x. i ) + 1 ) /\ B = ( 2 x. j ) ) -> ( A + B ) = ( ( ( 2 x. i ) + 1 ) + ( 2 x. j ) ) )
23 22 ex 
 |-  ( A = ( ( 2 x. i ) + 1 ) -> ( B = ( 2 x. j ) -> ( A + B ) = ( ( ( 2 x. i ) + 1 ) + ( 2 x. j ) ) ) )
24 23 ad3antlr 
 |-  ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) -> ( B = ( 2 x. j ) -> ( A + B ) = ( ( ( 2 x. i ) + 1 ) + ( 2 x. j ) ) ) )
25 24 imp 
 |-  ( ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) /\ B = ( 2 x. j ) ) -> ( A + B ) = ( ( ( 2 x. i ) + 1 ) + ( 2 x. j ) ) )
26 2cnd 
 |-  ( ( j e. ZZ /\ i e. ZZ ) -> 2 e. CC )
27 zcn 
 |-  ( i e. ZZ -> i e. CC )
28 27 adantl 
 |-  ( ( j e. ZZ /\ i e. ZZ ) -> i e. CC )
29 26 28 mulcld 
 |-  ( ( j e. ZZ /\ i e. ZZ ) -> ( 2 x. i ) e. CC )
30 29 ancoms 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> ( 2 x. i ) e. CC )
31 1cnd 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> 1 e. CC )
32 2cnd 
 |-  ( i e. ZZ -> 2 e. CC )
33 zcn 
 |-  ( j e. ZZ -> j e. CC )
34 mulcl 
 |-  ( ( 2 e. CC /\ j e. CC ) -> ( 2 x. j ) e. CC )
35 32 33 34 syl2an 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> ( 2 x. j ) e. CC )
36 30 31 35 add32d 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> ( ( ( 2 x. i ) + 1 ) + ( 2 x. j ) ) = ( ( ( 2 x. i ) + ( 2 x. j ) ) + 1 ) )
37 2cnd 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> 2 e. CC )
38 27 adantr 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> i e. CC )
39 33 adantl 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> j e. CC )
40 37 38 39 adddid 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> ( 2 x. ( i + j ) ) = ( ( 2 x. i ) + ( 2 x. j ) ) )
41 40 eqcomd 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> ( ( 2 x. i ) + ( 2 x. j ) ) = ( 2 x. ( i + j ) ) )
42 41 oveq1d 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> ( ( ( 2 x. i ) + ( 2 x. j ) ) + 1 ) = ( ( 2 x. ( i + j ) ) + 1 ) )
43 36 42 eqtrd 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> ( ( ( 2 x. i ) + 1 ) + ( 2 x. j ) ) = ( ( 2 x. ( i + j ) ) + 1 ) )
44 43 ex 
 |-  ( i e. ZZ -> ( j e. ZZ -> ( ( ( 2 x. i ) + 1 ) + ( 2 x. j ) ) = ( ( 2 x. ( i + j ) ) + 1 ) ) )
45 44 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 ) ) = ( ( 2 x. ( i + j ) ) + 1 ) ) )
46 45 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 ) ) = ( ( 2 x. ( i + j ) ) + 1 ) )
47 46 adantr 
 |-  ( ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) /\ B = ( 2 x. j ) ) -> ( ( ( 2 x. i ) + 1 ) + ( 2 x. j ) ) = ( ( 2 x. ( i + j ) ) + 1 ) )
48 25 47 eqtrd 
 |-  ( ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) /\ B = ( 2 x. j ) ) -> ( A + B ) = ( ( 2 x. ( i + j ) ) + 1 ) )
49 17 21 48 rspcedvd 
 |-  ( ( ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) /\ j e. ZZ ) /\ B = ( 2 x. j ) ) -> E. n e. ZZ ( A + B ) = ( ( 2 x. n ) + 1 ) )
50 49 rexlimdva2 
 |-  ( ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) /\ B e. ZZ ) -> ( E. j e. ZZ B = ( 2 x. j ) -> E. n e. ZZ ( A + B ) = ( ( 2 x. n ) + 1 ) ) )
51 50 expimpd 
 |-  ( ( ( A e. ZZ /\ i e. ZZ ) /\ A = ( ( 2 x. i ) + 1 ) ) -> ( ( B e. ZZ /\ E. j e. ZZ B = ( 2 x. j ) ) -> E. n e. ZZ ( A + B ) = ( ( 2 x. n ) + 1 ) ) )
52 51 r19.29an 
 |-  ( ( A e. ZZ /\ E. i e. ZZ A = ( ( 2 x. i ) + 1 ) ) -> ( ( B e. ZZ /\ E. j e. ZZ B = ( 2 x. j ) ) -> E. n e. ZZ ( A + B ) = ( ( 2 x. n ) + 1 ) ) )
53 12 52 biimtrid 
 |-  ( ( A e. ZZ /\ E. i e. ZZ A = ( ( 2 x. i ) + 1 ) ) -> ( B e. Even -> E. n e. ZZ ( A + B ) = ( ( 2 x. n ) + 1 ) ) )
54 8 53 sylbi 
 |-  ( A e. Odd -> ( B e. Even -> E. n e. ZZ ( A + B ) = ( ( 2 x. n ) + 1 ) ) )
55 54 imp 
 |-  ( ( A e. Odd /\ B e. Even ) -> E. n e. ZZ ( A + B ) = ( ( 2 x. n ) + 1 ) )
56 eqeq1 
 |-  ( z = ( A + B ) -> ( z = ( ( 2 x. n ) + 1 ) <-> ( A + B ) = ( ( 2 x. n ) + 1 ) ) )
57 56 rexbidv 
 |-  ( z = ( A + B ) -> ( E. n e. ZZ z = ( ( 2 x. n ) + 1 ) <-> E. n e. ZZ ( A + B ) = ( ( 2 x. n ) + 1 ) ) )
58 dfodd6 
 |-  Odd = { z e. ZZ | E. n e. ZZ z = ( ( 2 x. n ) + 1 ) }
59 57 58 elrab2 
 |-  ( ( A + B ) e. Odd <-> ( ( A + B ) e. ZZ /\ E. n e. ZZ ( A + B ) = ( ( 2 x. n ) + 1 ) ) )
60 4 55 59 sylanbrc 
 |-  ( ( A e. Odd /\ B e. Even ) -> ( A + B ) e. Odd )