Step | Hyp | Ref
| Expression |
1 | | oddz 45897 |
. . 3
โข (๐ด โ Odd โ ๐ด โ
โค) |
2 | | oddz 45897 |
. . 3
โข (๐ต โ Odd โ ๐ต โ
โค) |
3 | | zaddcl 12550 |
. . 3
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด + ๐ต) โ โค) |
4 | 1, 2, 3 | syl2an 597 |
. 2
โข ((๐ด โ Odd โง ๐ต โ Odd ) โ (๐ด + ๐ต) โ โค) |
5 | | eqeq1 2741 |
. . . . . 6
โข (๐ = ๐ด โ (๐ = ((2 ยท ๐) + 1) โ ๐ด = ((2 ยท ๐) + 1))) |
6 | 5 | rexbidv 3176 |
. . . . 5
โข (๐ = ๐ด โ (โ๐ โ โค ๐ = ((2 ยท ๐) + 1) โ โ๐ โ โค ๐ด = ((2 ยท ๐) + 1))) |
7 | | dfodd6 45903 |
. . . . 5
โข Odd =
{๐ โ โค โฃ
โ๐ โ โค
๐ = ((2 ยท ๐) + 1)} |
8 | 6, 7 | elrab2 3653 |
. . . 4
โข (๐ด โ Odd โ (๐ด โ โค โง
โ๐ โ โค
๐ด = ((2 ยท ๐) + 1))) |
9 | | eqeq1 2741 |
. . . . . . 7
โข (๐ = ๐ต โ (๐ = ((2 ยท ๐) + 1) โ ๐ต = ((2 ยท ๐) + 1))) |
10 | 9 | rexbidv 3176 |
. . . . . 6
โข (๐ = ๐ต โ (โ๐ โ โค ๐ = ((2 ยท ๐) + 1) โ โ๐ โ โค ๐ต = ((2 ยท ๐) + 1))) |
11 | | dfodd6 45903 |
. . . . . 6
โข Odd =
{๐ โ โค โฃ
โ๐ โ โค
๐ = ((2 ยท ๐) + 1)} |
12 | 10, 11 | elrab2 3653 |
. . . . 5
โข (๐ต โ Odd โ (๐ต โ โค โง
โ๐ โ โค
๐ต = ((2 ยท ๐) + 1))) |
13 | | zaddcl 12550 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + ๐) โ โค) |
14 | 13 | ex 414 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (๐ โ โค โ (๐ + ๐) โ โค)) |
15 | 14 | ad3antlr 730 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ โ โค) โง ๐ด = ((2 ยท ๐) + 1)) โง ๐ต โ โค) โ (๐ โ โค โ (๐ + ๐) โ โค)) |
16 | 15 | imp 408 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โ
(๐ + ๐) โ โค) |
17 | 16 | adantr 482 |
. . . . . . . . . . 11
โข
((((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โง
๐ต = ((2 ยท ๐) + 1)) โ (๐ + ๐) โ โค) |
18 | 17 | peano2zd 12617 |
. . . . . . . . . 10
โข
((((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โง
๐ต = ((2 ยท ๐) + 1)) โ ((๐ + ๐) + 1) โ โค) |
19 | | oveq2 7370 |
. . . . . . . . . . . 12
โข (๐ = ((๐ + ๐) + 1) โ (2 ยท ๐) = (2 ยท ((๐ + ๐) + 1))) |
20 | 19 | eqeq2d 2748 |
. . . . . . . . . . 11
โข (๐ = ((๐ + ๐) + 1) โ ((๐ด + ๐ต) = (2 ยท ๐) โ (๐ด + ๐ต) = (2 ยท ((๐ + ๐) + 1)))) |
21 | 20 | adantl 483 |
. . . . . . . . . 10
โข
(((((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โง
๐ต = ((2 ยท ๐) + 1)) โง ๐ = ((๐ + ๐) + 1)) โ ((๐ด + ๐ต) = (2 ยท ๐) โ (๐ด + ๐ต) = (2 ยท ((๐ + ๐) + 1)))) |
22 | | oveq12 7371 |
. . . . . . . . . . . . . 14
โข ((๐ด = ((2 ยท ๐) + 1) โง ๐ต = ((2 ยท ๐) + 1)) โ (๐ด + ๐ต) = (((2 ยท ๐) + 1) + ((2 ยท ๐) + 1))) |
23 | 22 | ex 414 |
. . . . . . . . . . . . 13
โข (๐ด = ((2 ยท ๐) + 1) โ (๐ต = ((2 ยท ๐) + 1) โ (๐ด + ๐ต) = (((2 ยท ๐) + 1) + ((2 ยท ๐) + 1)))) |
24 | 23 | ad3antlr 730 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โ
(๐ต = ((2 ยท ๐) + 1) โ (๐ด + ๐ต) = (((2 ยท ๐) + 1) + ((2 ยท ๐) + 1)))) |
25 | 24 | imp 408 |
. . . . . . . . . . 11
โข
((((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โง
๐ต = ((2 ยท ๐) + 1)) โ (๐ด + ๐ต) = (((2 ยท ๐) + 1) + ((2 ยท ๐) + 1))) |
26 | | zcn 12511 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ ๐ โ
โ) |
27 | | zcn 12511 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โค โ ๐ โ
โ) |
28 | | 2cnd 12238 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ 2 โ
โ) |
29 | 28 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ โง ๐ โ โ) โ (2
โ โ โง ๐
โ โ)) |
30 | 29 | ancoms 460 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ) โ (2
โ โ โง ๐
โ โ)) |
31 | | mulcl 11142 |
. . . . . . . . . . . . . . . . . . 19
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ๐) โ
โ) |
33 | | 1cnd 11157 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ) โ 1 โ
โ) |
34 | | 2cnd 12238 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ 2 โ
โ) |
35 | | mulcl 11142 |
. . . . . . . . . . . . . . . . . . 19
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
36 | 34, 35 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ๐) โ
โ) |
37 | 32, 33, 36, 33 | add4d 11390 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ โ โ) โ (((2
ยท ๐) + 1) + ((2
ยท ๐) + 1)) = (((2
ยท ๐) + (2 ยท
๐)) + (1 +
1))) |
38 | | 2cnd 12238 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ โง ๐ โ โ) โ 2 โ
โ) |
39 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
40 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ โง ๐ โ โ) โ ๐ โ
โ) |
41 | 38, 39, 40 | adddid 11186 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท (๐ + ๐)) = ((2 ยท ๐) + (2 ยท ๐))) |
42 | 41 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ) โ ((2
ยท (๐ + ๐)) + (2 ยท 1)) = (((2
ยท ๐) + (2 ยท
๐)) + (2 ยท
1))) |
43 | | addcl 11140 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + ๐) โ โ) |
44 | 38, 43, 33 | adddid 11186 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ) โ (2
ยท ((๐ + ๐) + 1)) = ((2 ยท (๐ + ๐)) + (2 ยท 1))) |
45 | | 1p1e2 12285 |
. . . . . . . . . . . . . . . . . . . . 21
โข (1 + 1) =
2 |
46 | | 2t1e2 12323 |
. . . . . . . . . . . . . . . . . . . . 21
โข (2
ยท 1) = 2 |
47 | 45, 46 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . . . . 20
โข (1 + 1) =
(2 ยท 1) |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ) โ (1 + 1)
= (2 ยท 1)) |
49 | 48 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ โ) โ (((2
ยท ๐) + (2 ยท
๐)) + (1 + 1)) = (((2
ยท ๐) + (2 ยท
๐)) + (2 ยท
1))) |
50 | 42, 44, 49 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ โ โ) โ (((2
ยท ๐) + (2 ยท
๐)) + (1 + 1)) = (2
ยท ((๐ + ๐) + 1))) |
51 | 37, 50 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ โ โ) โ (((2
ยท ๐) + 1) + ((2
ยท ๐) + 1)) = (2
ยท ((๐ + ๐) + 1))) |
52 | 26, 27, 51 | syl2an 597 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โค โง ๐ โ โค) โ (((2
ยท ๐) + 1) + ((2
ยท ๐) + 1)) = (2
ยท ((๐ + ๐) + 1))) |
53 | 52 | ex 414 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ (๐ โ โค โ (((2
ยท ๐) + 1) + ((2
ยท ๐) + 1)) = (2
ยท ((๐ + ๐) + 1)))) |
54 | 53 | ad3antlr 730 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ โ โค) โง ๐ด = ((2 ยท ๐) + 1)) โง ๐ต โ โค) โ (๐ โ โค โ (((2 ยท ๐) + 1) + ((2 ยท ๐) + 1)) = (2 ยท ((๐ + ๐) + 1)))) |
55 | 54 | imp 408 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โ
(((2 ยท ๐) + 1) + ((2
ยท ๐) + 1)) = (2
ยท ((๐ + ๐) + 1))) |
56 | 55 | adantr 482 |
. . . . . . . . . . 11
โข
((((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โง
๐ต = ((2 ยท ๐) + 1)) โ (((2 ยท
๐) + 1) + ((2 ยท
๐) + 1)) = (2 ยท
((๐ + ๐) + 1))) |
57 | 25, 56 | eqtrd 2777 |
. . . . . . . . . 10
โข
((((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โง
๐ต = ((2 ยท ๐) + 1)) โ (๐ด + ๐ต) = (2 ยท ((๐ + ๐) + 1))) |
58 | 18, 21, 57 | rspcedvd 3586 |
. . . . . . . . 9
โข
((((((๐ด โ
โค โง ๐ โ
โค) โง ๐ด = ((2
ยท ๐) + 1)) โง
๐ต โ โค) โง
๐ โ โค) โง
๐ต = ((2 ยท ๐) + 1)) โ โ๐ โ โค (๐ด + ๐ต) = (2 ยท ๐)) |
59 | 58 | rexlimdva2 3155 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ โ โค) โง ๐ด = ((2 ยท ๐) + 1)) โง ๐ต โ โค) โ (โ๐ โ โค ๐ต = ((2 ยท ๐) + 1) โ โ๐ โ โค (๐ด + ๐ต) = (2 ยท ๐))) |
60 | 59 | expimpd 455 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ โ โค) โง ๐ด = ((2 ยท ๐) + 1)) โ ((๐ต โ โค โง
โ๐ โ โค
๐ต = ((2 ยท ๐) + 1)) โ โ๐ โ โค (๐ด + ๐ต) = (2 ยท ๐))) |
61 | 60 | rexlimdva2 3155 |
. . . . . 6
โข (๐ด โ โค โ
(โ๐ โ โค
๐ด = ((2 ยท ๐) + 1) โ ((๐ต โ โค โง
โ๐ โ โค
๐ต = ((2 ยท ๐) + 1)) โ โ๐ โ โค (๐ด + ๐ต) = (2 ยท ๐)))) |
62 | 61 | imp 408 |
. . . . 5
โข ((๐ด โ โค โง
โ๐ โ โค
๐ด = ((2 ยท ๐) + 1)) โ ((๐ต โ โค โง
โ๐ โ โค
๐ต = ((2 ยท ๐) + 1)) โ โ๐ โ โค (๐ด + ๐ต) = (2 ยท ๐))) |
63 | 12, 62 | biimtrid 241 |
. . . 4
โข ((๐ด โ โค โง
โ๐ โ โค
๐ด = ((2 ยท ๐) + 1)) โ (๐ต โ Odd โ โ๐ โ โค (๐ด + ๐ต) = (2 ยท ๐))) |
64 | 8, 63 | sylbi 216 |
. . 3
โข (๐ด โ Odd โ (๐ต โ Odd โ โ๐ โ โค (๐ด + ๐ต) = (2 ยท ๐))) |
65 | 64 | imp 408 |
. 2
โข ((๐ด โ Odd โง ๐ต โ Odd ) โ
โ๐ โ โค
(๐ด + ๐ต) = (2 ยท ๐)) |
66 | | eqeq1 2741 |
. . . 4
โข (๐ง = (๐ด + ๐ต) โ (๐ง = (2 ยท ๐) โ (๐ด + ๐ต) = (2 ยท ๐))) |
67 | 66 | rexbidv 3176 |
. . 3
โข (๐ง = (๐ด + ๐ต) โ (โ๐ โ โค ๐ง = (2 ยท ๐) โ โ๐ โ โค (๐ด + ๐ต) = (2 ยท ๐))) |
68 | | dfeven4 45904 |
. . 3
โข Even =
{๐ง โ โค โฃ
โ๐ โ โค
๐ง = (2 ยท ๐)} |
69 | 67, 68 | elrab2 3653 |
. 2
โข ((๐ด + ๐ต) โ Even โ ((๐ด + ๐ต) โ โค โง โ๐ โ โค (๐ด + ๐ต) = (2 ยท ๐))) |
70 | 4, 65, 69 | sylanbrc 584 |
1
โข ((๐ด โ Odd โง ๐ต โ Odd ) โ (๐ด + ๐ต) โ Even ) |