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 ( ( ๐ด โˆˆ Odd โˆง ๐ต โˆˆ Even ) โ†’ ( ๐ด + ๐ต ) โˆˆ Odd )

Proof

Step Hyp Ref Expression
1 oddz โŠข ( ๐ด โˆˆ Odd โ†’ ๐ด โˆˆ โ„ค )
2 evenz โŠข ( ๐ต โˆˆ Even โ†’ ๐ต โˆˆ โ„ค )
3 zaddcl โŠข ( ( ๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค ) โ†’ ( ๐ด + ๐ต ) โˆˆ โ„ค )
4 1 2 3 syl2an โŠข ( ( ๐ด โˆˆ Odd โˆง ๐ต โˆˆ Even ) โ†’ ( ๐ด + ๐ต ) โˆˆ โ„ค )
5 eqeq1 โŠข ( ๐‘Ž = ๐ด โ†’ ( ๐‘Ž = ( ( 2 ยท ๐‘– ) + 1 ) โ†” ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) )
6 5 rexbidv โŠข ( ๐‘Ž = ๐ด โ†’ ( โˆƒ ๐‘– โˆˆ โ„ค ๐‘Ž = ( ( 2 ยท ๐‘– ) + 1 ) โ†” โˆƒ ๐‘– โˆˆ โ„ค ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) )
7 dfodd6 โŠข Odd = { ๐‘Ž โˆˆ โ„ค โˆฃ โˆƒ ๐‘– โˆˆ โ„ค ๐‘Ž = ( ( 2 ยท ๐‘– ) + 1 ) }
8 6 7 elrab2 โŠข ( ๐ด โˆˆ Odd โ†” ( ๐ด โˆˆ โ„ค โˆง โˆƒ ๐‘– โˆˆ โ„ค ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) )
9 eqeq1 โŠข ( ๐‘ = ๐ต โ†’ ( ๐‘ = ( 2 ยท ๐‘— ) โ†” ๐ต = ( 2 ยท ๐‘— ) ) )
10 9 rexbidv โŠข ( ๐‘ = ๐ต โ†’ ( โˆƒ ๐‘— โˆˆ โ„ค ๐‘ = ( 2 ยท ๐‘— ) โ†” โˆƒ ๐‘— โˆˆ โ„ค ๐ต = ( 2 ยท ๐‘— ) ) )
11 dfeven4 โŠข Even = { ๐‘ โˆˆ โ„ค โˆฃ โˆƒ ๐‘— โˆˆ โ„ค ๐‘ = ( 2 ยท ๐‘— ) }
12 10 11 elrab2 โŠข ( ๐ต โˆˆ Even โ†” ( ๐ต โˆˆ โ„ค โˆง โˆƒ ๐‘— โˆˆ โ„ค ๐ต = ( 2 ยท ๐‘— ) ) )
13 zaddcl โŠข ( ( ๐‘– โˆˆ โ„ค โˆง ๐‘— โˆˆ โ„ค ) โ†’ ( ๐‘– + ๐‘— ) โˆˆ โ„ค )
14 13 ex โŠข ( ๐‘– โˆˆ โ„ค โ†’ ( ๐‘— โˆˆ โ„ค โ†’ ( ๐‘– + ๐‘— ) โˆˆ โ„ค ) )
15 14 ad3antlr โŠข ( ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โˆง ๐ต โˆˆ โ„ค ) โ†’ ( ๐‘— โˆˆ โ„ค โ†’ ( ๐‘– + ๐‘— ) โˆˆ โ„ค ) )
16 15 imp โŠข ( ( ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โˆง ๐ต โˆˆ โ„ค ) โˆง ๐‘— โˆˆ โ„ค ) โ†’ ( ๐‘– + ๐‘— ) โˆˆ โ„ค )
17 16 adantr โŠข ( ( ( ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โˆง ๐ต โˆˆ โ„ค ) โˆง ๐‘— โˆˆ โ„ค ) โˆง ๐ต = ( 2 ยท ๐‘— ) ) โ†’ ( ๐‘– + ๐‘— ) โˆˆ โ„ค )
18 oveq2 โŠข ( ๐‘› = ( ๐‘– + ๐‘— ) โ†’ ( 2 ยท ๐‘› ) = ( 2 ยท ( ๐‘– + ๐‘— ) ) )
19 18 oveq1d โŠข ( ๐‘› = ( ๐‘– + ๐‘— ) โ†’ ( ( 2 ยท ๐‘› ) + 1 ) = ( ( 2 ยท ( ๐‘– + ๐‘— ) ) + 1 ) )
20 19 eqeq2d โŠข ( ๐‘› = ( ๐‘– + ๐‘— ) โ†’ ( ( ๐ด + ๐ต ) = ( ( 2 ยท ๐‘› ) + 1 ) โ†” ( ๐ด + ๐ต ) = ( ( 2 ยท ( ๐‘– + ๐‘— ) ) + 1 ) ) )
21 20 adantl โŠข ( ( ( ( ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โˆง ๐ต โˆˆ โ„ค ) โˆง ๐‘— โˆˆ โ„ค ) โˆง ๐ต = ( 2 ยท ๐‘— ) ) โˆง ๐‘› = ( ๐‘– + ๐‘— ) ) โ†’ ( ( ๐ด + ๐ต ) = ( ( 2 ยท ๐‘› ) + 1 ) โ†” ( ๐ด + ๐ต ) = ( ( 2 ยท ( ๐‘– + ๐‘— ) ) + 1 ) ) )
22 oveq12 โŠข ( ( ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) โˆง ๐ต = ( 2 ยท ๐‘— ) ) โ†’ ( ๐ด + ๐ต ) = ( ( ( 2 ยท ๐‘– ) + 1 ) + ( 2 ยท ๐‘— ) ) )
23 22 ex โŠข ( ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) โ†’ ( ๐ต = ( 2 ยท ๐‘— ) โ†’ ( ๐ด + ๐ต ) = ( ( ( 2 ยท ๐‘– ) + 1 ) + ( 2 ยท ๐‘— ) ) ) )
24 23 ad3antlr โŠข ( ( ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โˆง ๐ต โˆˆ โ„ค ) โˆง ๐‘— โˆˆ โ„ค ) โ†’ ( ๐ต = ( 2 ยท ๐‘— ) โ†’ ( ๐ด + ๐ต ) = ( ( ( 2 ยท ๐‘– ) + 1 ) + ( 2 ยท ๐‘— ) ) ) )
25 24 imp โŠข ( ( ( ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โˆง ๐ต โˆˆ โ„ค ) โˆง ๐‘— โˆˆ โ„ค ) โˆง ๐ต = ( 2 ยท ๐‘— ) ) โ†’ ( ๐ด + ๐ต ) = ( ( ( 2 ยท ๐‘– ) + 1 ) + ( 2 ยท ๐‘— ) ) )
26 2cnd โŠข ( ( ๐‘— โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โ†’ 2 โˆˆ โ„‚ )
27 zcn โŠข ( ๐‘– โˆˆ โ„ค โ†’ ๐‘– โˆˆ โ„‚ )
28 27 adantl โŠข ( ( ๐‘— โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โ†’ ๐‘– โˆˆ โ„‚ )
29 26 28 mulcld โŠข ( ( ๐‘— โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โ†’ ( 2 ยท ๐‘– ) โˆˆ โ„‚ )
30 29 ancoms โŠข ( ( ๐‘– โˆˆ โ„ค โˆง ๐‘— โˆˆ โ„ค ) โ†’ ( 2 ยท ๐‘– ) โˆˆ โ„‚ )
31 1cnd โŠข ( ( ๐‘– โˆˆ โ„ค โˆง ๐‘— โˆˆ โ„ค ) โ†’ 1 โˆˆ โ„‚ )
32 2cnd โŠข ( ๐‘– โˆˆ โ„ค โ†’ 2 โˆˆ โ„‚ )
33 zcn โŠข ( ๐‘— โˆˆ โ„ค โ†’ ๐‘— โˆˆ โ„‚ )
34 mulcl โŠข ( ( 2 โˆˆ โ„‚ โˆง ๐‘— โˆˆ โ„‚ ) โ†’ ( 2 ยท ๐‘— ) โˆˆ โ„‚ )
35 32 33 34 syl2an โŠข ( ( ๐‘– โˆˆ โ„ค โˆง ๐‘— โˆˆ โ„ค ) โ†’ ( 2 ยท ๐‘— ) โˆˆ โ„‚ )
36 30 31 35 add32d โŠข ( ( ๐‘– โˆˆ โ„ค โˆง ๐‘— โˆˆ โ„ค ) โ†’ ( ( ( 2 ยท ๐‘– ) + 1 ) + ( 2 ยท ๐‘— ) ) = ( ( ( 2 ยท ๐‘– ) + ( 2 ยท ๐‘— ) ) + 1 ) )
37 2cnd โŠข ( ( ๐‘– โˆˆ โ„ค โˆง ๐‘— โˆˆ โ„ค ) โ†’ 2 โˆˆ โ„‚ )
38 27 adantr โŠข ( ( ๐‘– โˆˆ โ„ค โˆง ๐‘— โˆˆ โ„ค ) โ†’ ๐‘– โˆˆ โ„‚ )
39 33 adantl โŠข ( ( ๐‘– โˆˆ โ„ค โˆง ๐‘— โˆˆ โ„ค ) โ†’ ๐‘— โˆˆ โ„‚ )
40 37 38 39 adddid โŠข ( ( ๐‘– โˆˆ โ„ค โˆง ๐‘— โˆˆ โ„ค ) โ†’ ( 2 ยท ( ๐‘– + ๐‘— ) ) = ( ( 2 ยท ๐‘– ) + ( 2 ยท ๐‘— ) ) )
41 40 eqcomd โŠข ( ( ๐‘– โˆˆ โ„ค โˆง ๐‘— โˆˆ โ„ค ) โ†’ ( ( 2 ยท ๐‘– ) + ( 2 ยท ๐‘— ) ) = ( 2 ยท ( ๐‘– + ๐‘— ) ) )
42 41 oveq1d โŠข ( ( ๐‘– โˆˆ โ„ค โˆง ๐‘— โˆˆ โ„ค ) โ†’ ( ( ( 2 ยท ๐‘– ) + ( 2 ยท ๐‘— ) ) + 1 ) = ( ( 2 ยท ( ๐‘– + ๐‘— ) ) + 1 ) )
43 36 42 eqtrd โŠข ( ( ๐‘– โˆˆ โ„ค โˆง ๐‘— โˆˆ โ„ค ) โ†’ ( ( ( 2 ยท ๐‘– ) + 1 ) + ( 2 ยท ๐‘— ) ) = ( ( 2 ยท ( ๐‘– + ๐‘— ) ) + 1 ) )
44 43 ex โŠข ( ๐‘– โˆˆ โ„ค โ†’ ( ๐‘— โˆˆ โ„ค โ†’ ( ( ( 2 ยท ๐‘– ) + 1 ) + ( 2 ยท ๐‘— ) ) = ( ( 2 ยท ( ๐‘– + ๐‘— ) ) + 1 ) ) )
45 44 ad3antlr โŠข ( ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โˆง ๐ต โˆˆ โ„ค ) โ†’ ( ๐‘— โˆˆ โ„ค โ†’ ( ( ( 2 ยท ๐‘– ) + 1 ) + ( 2 ยท ๐‘— ) ) = ( ( 2 ยท ( ๐‘– + ๐‘— ) ) + 1 ) ) )
46 45 imp โŠข ( ( ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โˆง ๐ต โˆˆ โ„ค ) โˆง ๐‘— โˆˆ โ„ค ) โ†’ ( ( ( 2 ยท ๐‘– ) + 1 ) + ( 2 ยท ๐‘— ) ) = ( ( 2 ยท ( ๐‘– + ๐‘— ) ) + 1 ) )
47 46 adantr โŠข ( ( ( ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โˆง ๐ต โˆˆ โ„ค ) โˆง ๐‘— โˆˆ โ„ค ) โˆง ๐ต = ( 2 ยท ๐‘— ) ) โ†’ ( ( ( 2 ยท ๐‘– ) + 1 ) + ( 2 ยท ๐‘— ) ) = ( ( 2 ยท ( ๐‘– + ๐‘— ) ) + 1 ) )
48 25 47 eqtrd โŠข ( ( ( ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โˆง ๐ต โˆˆ โ„ค ) โˆง ๐‘— โˆˆ โ„ค ) โˆง ๐ต = ( 2 ยท ๐‘— ) ) โ†’ ( ๐ด + ๐ต ) = ( ( 2 ยท ( ๐‘– + ๐‘— ) ) + 1 ) )
49 17 21 48 rspcedvd โŠข ( ( ( ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โˆง ๐ต โˆˆ โ„ค ) โˆง ๐‘— โˆˆ โ„ค ) โˆง ๐ต = ( 2 ยท ๐‘— ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„ค ( ๐ด + ๐ต ) = ( ( 2 ยท ๐‘› ) + 1 ) )
50 49 rexlimdva2 โŠข ( ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โˆง ๐ต โˆˆ โ„ค ) โ†’ ( โˆƒ ๐‘— โˆˆ โ„ค ๐ต = ( 2 ยท ๐‘— ) โ†’ โˆƒ ๐‘› โˆˆ โ„ค ( ๐ด + ๐ต ) = ( ( 2 ยท ๐‘› ) + 1 ) ) )
51 50 expimpd โŠข ( ( ( ๐ด โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โ†’ ( ( ๐ต โˆˆ โ„ค โˆง โˆƒ ๐‘— โˆˆ โ„ค ๐ต = ( 2 ยท ๐‘— ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„ค ( ๐ด + ๐ต ) = ( ( 2 ยท ๐‘› ) + 1 ) ) )
52 51 r19.29an โŠข ( ( ๐ด โˆˆ โ„ค โˆง โˆƒ ๐‘– โˆˆ โ„ค ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โ†’ ( ( ๐ต โˆˆ โ„ค โˆง โˆƒ ๐‘— โˆˆ โ„ค ๐ต = ( 2 ยท ๐‘— ) ) โ†’ โˆƒ ๐‘› โˆˆ โ„ค ( ๐ด + ๐ต ) = ( ( 2 ยท ๐‘› ) + 1 ) ) )
53 12 52 syl5bi โŠข ( ( ๐ด โˆˆ โ„ค โˆง โˆƒ ๐‘– โˆˆ โ„ค ๐ด = ( ( 2 ยท ๐‘– ) + 1 ) ) โ†’ ( ๐ต โˆˆ Even โ†’ โˆƒ ๐‘› โˆˆ โ„ค ( ๐ด + ๐ต ) = ( ( 2 ยท ๐‘› ) + 1 ) ) )
54 8 53 sylbi โŠข ( ๐ด โˆˆ Odd โ†’ ( ๐ต โˆˆ Even โ†’ โˆƒ ๐‘› โˆˆ โ„ค ( ๐ด + ๐ต ) = ( ( 2 ยท ๐‘› ) + 1 ) ) )
55 54 imp โŠข ( ( ๐ด โˆˆ Odd โˆง ๐ต โˆˆ Even ) โ†’ โˆƒ ๐‘› โˆˆ โ„ค ( ๐ด + ๐ต ) = ( ( 2 ยท ๐‘› ) + 1 ) )
56 eqeq1 โŠข ( ๐‘ง = ( ๐ด + ๐ต ) โ†’ ( ๐‘ง = ( ( 2 ยท ๐‘› ) + 1 ) โ†” ( ๐ด + ๐ต ) = ( ( 2 ยท ๐‘› ) + 1 ) ) )
57 56 rexbidv โŠข ( ๐‘ง = ( ๐ด + ๐ต ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„ค ๐‘ง = ( ( 2 ยท ๐‘› ) + 1 ) โ†” โˆƒ ๐‘› โˆˆ โ„ค ( ๐ด + ๐ต ) = ( ( 2 ยท ๐‘› ) + 1 ) ) )
58 dfodd6 โŠข Odd = { ๐‘ง โˆˆ โ„ค โˆฃ โˆƒ ๐‘› โˆˆ โ„ค ๐‘ง = ( ( 2 ยท ๐‘› ) + 1 ) }
59 57 58 elrab2 โŠข ( ( ๐ด + ๐ต ) โˆˆ Odd โ†” ( ( ๐ด + ๐ต ) โˆˆ โ„ค โˆง โˆƒ ๐‘› โˆˆ โ„ค ( ๐ด + ๐ต ) = ( ( 2 ยท ๐‘› ) + 1 ) ) )
60 4 55 59 sylanbrc โŠข ( ( ๐ด โˆˆ Odd โˆง ๐ต โˆˆ Even ) โ†’ ( ๐ด + ๐ต ) โˆˆ Odd )