Step | Hyp | Ref
| Expression |
1 | | oddz 46597 |
. . 3
โข (๐ด โ Odd โ ๐ด โ
โค) |
2 | | evenz 46596 |
. . 3
โข (๐ต โ Even โ ๐ต โ
โค) |
3 | | zaddcl 12606 |
. . 3
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด + ๐ต) โ โค) |
4 | 1, 2, 3 | syl2an 594 |
. 2
โข ((๐ด โ Odd โง ๐ต โ Even ) โ (๐ด + ๐ต) โ โค) |
5 | | eqeq1 2734 |
. . . . . 6
โข (๐ = ๐ด โ (๐ = ((2 ยท ๐) + 1) โ ๐ด = ((2 ยท ๐) + 1))) |
6 | 5 | rexbidv 3176 |
. . . . 5
โข (๐ = ๐ด โ (โ๐ โ โค ๐ = ((2 ยท ๐) + 1) โ โ๐ โ โค ๐ด = ((2 ยท ๐) + 1))) |
7 | | dfodd6 46603 |
. . . . 5
โข Odd =
{๐ โ โค โฃ
โ๐ โ โค
๐ = ((2 ยท ๐) + 1)} |
8 | 6, 7 | elrab2 3685 |
. . . 4
โข (๐ด โ Odd โ (๐ด โ โค โง
โ๐ โ โค
๐ด = ((2 ยท ๐) + 1))) |
9 | | eqeq1 2734 |
. . . . . . 7
โข (๐ = ๐ต โ (๐ = (2 ยท ๐) โ ๐ต = (2 ยท ๐))) |
10 | 9 | rexbidv 3176 |
. . . . . 6
โข (๐ = ๐ต โ (โ๐ โ โค ๐ = (2 ยท ๐) โ โ๐ โ โค ๐ต = (2 ยท ๐))) |
11 | | dfeven4 46604 |
. . . . . 6
โข Even =
{๐ โ โค โฃ
โ๐ โ โค
๐ = (2 ยท ๐)} |
12 | 10, 11 | elrab2 3685 |
. . . . 5
โข (๐ต โ Even โ (๐ต โ โค โง
โ๐ โ โค
๐ต = (2 ยท ๐))) |
13 | | zaddcl 12606 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + ๐) โ โค) |
14 | 13 | ex 411 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐ โ โค โ (๐ + ๐) โ โค)) |
15 | 14 | ad3antlr 727 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ โ โค) โง ๐ด = ((2 ยท ๐) + 1)) โง ๐ต โ โค) โ (๐ โ โค โ (๐ + ๐) โ โค)) |
16 | 15 | imp 405 |
. . . . . . . . . 10
โข
(((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โ
(๐ + ๐) โ โค) |
17 | 16 | adantr 479 |
. . . . . . . . 9
โข
((((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โง
๐ต = (2 ยท ๐)) โ (๐ + ๐) โ โค) |
18 | | oveq2 7419 |
. . . . . . . . . . . 12
โข (๐ = (๐ + ๐) โ (2 ยท ๐) = (2 ยท (๐ + ๐))) |
19 | 18 | oveq1d 7426 |
. . . . . . . . . . 11
โข (๐ = (๐ + ๐) โ ((2 ยท ๐) + 1) = ((2 ยท (๐ + ๐)) + 1)) |
20 | 19 | eqeq2d 2741 |
. . . . . . . . . 10
โข (๐ = (๐ + ๐) โ ((๐ด + ๐ต) = ((2 ยท ๐) + 1) โ (๐ด + ๐ต) = ((2 ยท (๐ + ๐)) + 1))) |
21 | 20 | adantl 480 |
. . . . . . . . 9
โข
(((((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โง
๐ต = (2 ยท ๐)) โง ๐ = (๐ + ๐)) โ ((๐ด + ๐ต) = ((2 ยท ๐) + 1) โ (๐ด + ๐ต) = ((2 ยท (๐ + ๐)) + 1))) |
22 | | oveq12 7420 |
. . . . . . . . . . . . 13
โข ((๐ด = ((2 ยท ๐) + 1) โง ๐ต = (2 ยท ๐)) โ (๐ด + ๐ต) = (((2 ยท ๐) + 1) + (2 ยท ๐))) |
23 | 22 | ex 411 |
. . . . . . . . . . . 12
โข (๐ด = ((2 ยท ๐) + 1) โ (๐ต = (2 ยท ๐) โ (๐ด + ๐ต) = (((2 ยท ๐) + 1) + (2 ยท ๐)))) |
24 | 23 | ad3antlr 727 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โ
(๐ต = (2 ยท ๐) โ (๐ด + ๐ต) = (((2 ยท ๐) + 1) + (2 ยท ๐)))) |
25 | 24 | imp 405 |
. . . . . . . . . 10
โข
((((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โง
๐ต = (2 ยท ๐)) โ (๐ด + ๐ต) = (((2 ยท ๐) + 1) + (2 ยท ๐))) |
26 | | 2cnd 12294 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐ โ โค) โ 2 โ
โ) |
27 | | zcn 12567 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โค โ ๐ โ
โ) |
28 | 27 | adantl 480 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โ
โ) |
29 | 26, 28 | mulcld 11238 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง ๐ โ โค) โ (2
ยท ๐) โ
โ) |
30 | 29 | ancoms 457 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ๐ โ โค) โ (2
ยท ๐) โ
โ) |
31 | | 1cnd 11213 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ๐ โ โค) โ 1 โ
โ) |
32 | | 2cnd 12294 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โค โ 2 โ
โ) |
33 | | zcn 12567 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โค โ ๐ โ
โ) |
34 | | mulcl 11196 |
. . . . . . . . . . . . . . . . 17
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
35 | 32, 33, 34 | syl2an 594 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ๐ โ โค) โ (2
ยท ๐) โ
โ) |
36 | 30, 31, 35 | add32d 11445 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) + (2
ยท ๐)) = (((2
ยท ๐) + (2 ยท
๐)) + 1)) |
37 | | 2cnd 12294 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐ โ โค) โ 2 โ
โ) |
38 | 27 | adantr 479 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โ
โ) |
39 | 33 | adantl 480 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โ
โ) |
40 | 37, 38, 39 | adddid 11242 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง ๐ โ โค) โ (2
ยท (๐ + ๐)) = ((2 ยท ๐) + (2 ยท ๐))) |
41 | 40 | eqcomd 2736 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ๐ โ โค) โ ((2
ยท ๐) + (2 ยท
๐)) = (2 ยท (๐ + ๐))) |
42 | 41 | oveq1d 7426 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + (2 ยท
๐)) + 1) = ((2 ยท
(๐ + ๐)) + 1)) |
43 | 36, 42 | eqtrd 2770 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) + (2
ยท ๐)) = ((2 ยท
(๐ + ๐)) + 1)) |
44 | 43 | ex 411 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ (๐ โ โค โ (((2
ยท ๐) + 1) + (2
ยท ๐)) = ((2 ยท
(๐ + ๐)) + 1))) |
45 | 44 | ad3antlr 727 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ โ โค) โง ๐ด = ((2 ยท ๐) + 1)) โง ๐ต โ โค) โ (๐ โ โค โ (((2 ยท ๐) + 1) + (2 ยท ๐)) = ((2 ยท (๐ + ๐)) + 1))) |
46 | 45 | imp 405 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โ
(((2 ยท ๐) + 1) + (2
ยท ๐)) = ((2 ยท
(๐ + ๐)) + 1)) |
47 | 46 | adantr 479 |
. . . . . . . . . 10
โข
((((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โง
๐ต = (2 ยท ๐)) โ (((2 ยท ๐) + 1) + (2 ยท ๐)) = ((2 ยท (๐ + ๐)) + 1)) |
48 | 25, 47 | eqtrd 2770 |
. . . . . . . . 9
โข
((((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โง
๐ต = (2 ยท ๐)) โ (๐ด + ๐ต) = ((2 ยท (๐ + ๐)) + 1)) |
49 | 17, 21, 48 | rspcedvd 3613 |
. . . . . . . 8
โข
((((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โง
๐ต = (2 ยท ๐)) โ โ๐ โ โค (๐ด + ๐ต) = ((2 ยท ๐) + 1)) |
50 | 49 | rexlimdva2 3155 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ โ โค) โง ๐ด = ((2 ยท ๐) + 1)) โง ๐ต โ โค) โ (โ๐ โ โค ๐ต = (2 ยท ๐) โ โ๐ โ โค (๐ด + ๐ต) = ((2 ยท ๐) + 1))) |
51 | 50 | expimpd 452 |
. . . . . 6
โข (((๐ด โ โค โง ๐ โ โค) โง ๐ด = ((2 ยท ๐) + 1)) โ ((๐ต โ โค โง
โ๐ โ โค
๐ต = (2 ยท ๐)) โ โ๐ โ โค (๐ด + ๐ต) = ((2 ยท ๐) + 1))) |
52 | 51 | r19.29an 3156 |
. . . . 5
โข ((๐ด โ โค โง
โ๐ โ โค
๐ด = ((2 ยท ๐) + 1)) โ ((๐ต โ โค โง
โ๐ โ โค
๐ต = (2 ยท ๐)) โ โ๐ โ โค (๐ด + ๐ต) = ((2 ยท ๐) + 1))) |
53 | 12, 52 | biimtrid 241 |
. . . 4
โข ((๐ด โ โค โง
โ๐ โ โค
๐ด = ((2 ยท ๐) + 1)) โ (๐ต โ Even โ โ๐ โ โค (๐ด + ๐ต) = ((2 ยท ๐) + 1))) |
54 | 8, 53 | sylbi 216 |
. . 3
โข (๐ด โ Odd โ (๐ต โ Even โ โ๐ โ โค (๐ด + ๐ต) = ((2 ยท ๐) + 1))) |
55 | 54 | imp 405 |
. 2
โข ((๐ด โ Odd โง ๐ต โ Even ) โ
โ๐ โ โค
(๐ด + ๐ต) = ((2 ยท ๐) + 1)) |
56 | | eqeq1 2734 |
. . . 4
โข (๐ง = (๐ด + ๐ต) โ (๐ง = ((2 ยท ๐) + 1) โ (๐ด + ๐ต) = ((2 ยท ๐) + 1))) |
57 | 56 | rexbidv 3176 |
. . 3
โข (๐ง = (๐ด + ๐ต) โ (โ๐ โ โค ๐ง = ((2 ยท ๐) + 1) โ โ๐ โ โค (๐ด + ๐ต) = ((2 ยท ๐) + 1))) |
58 | | dfodd6 46603 |
. . 3
โข Odd =
{๐ง โ โค โฃ
โ๐ โ โค
๐ง = ((2 ยท ๐) + 1)} |
59 | 57, 58 | elrab2 3685 |
. 2
โข ((๐ด + ๐ต) โ Odd โ ((๐ด + ๐ต) โ โค โง โ๐ โ โค (๐ด + ๐ต) = ((2 ยท ๐) + 1))) |
60 | 4, 55, 59 | sylanbrc 581 |
1
โข ((๐ด โ Odd โง ๐ต โ Even ) โ (๐ด + ๐ต) โ Odd ) |