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 syl5bi
 |-  ( ( 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 )