Step | Hyp | Ref
| Expression |
1 | | 0cn 11152 |
. . . . . . . . 9
โข 0 โ
โ |
2 | | ifcl 4532 |
. . . . . . . . 9
โข ((๐ด โ โ โง 0 โ
โ) โ if(๐, ๐ด, 0) โ
โ) |
3 | 1, 2 | mpan2 690 |
. . . . . . . 8
โข (๐ด โ โ โ if(๐, ๐ด, 0) โ โ) |
4 | 3 | ad2antrr 725 |
. . . . . . 7
โข (((๐ด โ โ โง ๐) โง ๐) โ if(๐, ๐ด, 0) โ โ) |
5 | | simpll 766 |
. . . . . . 7
โข (((๐ด โ โ โง ๐) โง ๐) โ ๐ด โ โ) |
6 | 4, 5, 5 | add12d 11386 |
. . . . . 6
โข (((๐ด โ โ โง ๐) โง ๐) โ (if(๐, ๐ด, 0) + (๐ด + ๐ด)) = (๐ด + (if(๐, ๐ด, 0) + ๐ด))) |
7 | 5, 4, 5 | addassd 11182 |
. . . . . 6
โข (((๐ด โ โ โง ๐) โง ๐) โ ((๐ด + if(๐, ๐ด, 0)) + ๐ด) = (๐ด + (if(๐, ๐ด, 0) + ๐ด))) |
8 | 6, 7 | eqtr4d 2776 |
. . . . 5
โข (((๐ด โ โ โง ๐) โง ๐) โ (if(๐, ๐ด, 0) + (๐ด + ๐ด)) = ((๐ด + if(๐, ๐ด, 0)) + ๐ด)) |
9 | | pm5.501 367 |
. . . . . . . . 9
โข (๐ โ (๐ โ (๐ โ ๐))) |
10 | 9 | adantl 483 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐) โง ๐) โ (๐ โ (๐ โ ๐))) |
11 | 10 | bicomd 222 |
. . . . . . 7
โข (((๐ด โ โ โง ๐) โง ๐) โ ((๐ โ ๐) โ ๐)) |
12 | 11 | ifbid 4510 |
. . . . . 6
โข (((๐ด โ โ โง ๐) โง ๐) โ if((๐ โ ๐), ๐ด, 0) = if(๐, ๐ด, 0)) |
13 | | animorrl 980 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐) โง ๐) โ (๐ โจ ๐)) |
14 | | iftrue 4493 |
. . . . . . . 8
โข ((๐ โจ ๐) โ if((๐ โจ ๐), (2 ยท ๐ด), 0) = (2 ยท ๐ด)) |
15 | 13, 14 | syl 17 |
. . . . . . 7
โข (((๐ด โ โ โง ๐) โง ๐) โ if((๐ โจ ๐), (2 ยท ๐ด), 0) = (2 ยท ๐ด)) |
16 | 5 | 2timesd 12401 |
. . . . . . 7
โข (((๐ด โ โ โง ๐) โง ๐) โ (2 ยท ๐ด) = (๐ด + ๐ด)) |
17 | 15, 16 | eqtrd 2773 |
. . . . . 6
โข (((๐ด โ โ โง ๐) โง ๐) โ if((๐ โจ ๐), (2 ยท ๐ด), 0) = (๐ด + ๐ด)) |
18 | 12, 17 | oveq12d 7376 |
. . . . 5
โข (((๐ด โ โ โง ๐) โง ๐) โ (if((๐ โ ๐), ๐ด, 0) + if((๐ โจ ๐), (2 ยท ๐ด), 0)) = (if(๐, ๐ด, 0) + (๐ด + ๐ด))) |
19 | | iftrue 4493 |
. . . . . . . 8
โข (๐ โ if(๐, ๐ด, 0) = ๐ด) |
20 | 19 | adantl 483 |
. . . . . . 7
โข (((๐ด โ โ โง ๐) โง ๐) โ if(๐, ๐ด, 0) = ๐ด) |
21 | 20 | oveq1d 7373 |
. . . . . 6
โข (((๐ด โ โ โง ๐) โง ๐) โ (if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) = (๐ด + if(๐, ๐ด, 0))) |
22 | 21 | oveq1d 7373 |
. . . . 5
โข (((๐ด โ โ โง ๐) โง ๐) โ ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + ๐ด) = ((๐ด + if(๐, ๐ด, 0)) + ๐ด)) |
23 | 8, 18, 22 | 3eqtr4d 2783 |
. . . 4
โข (((๐ด โ โ โง ๐) โง ๐) โ (if((๐ โ ๐), ๐ด, 0) + if((๐ โจ ๐), (2 ยท ๐ด), 0)) = ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + ๐ด)) |
24 | | iffalse 4496 |
. . . . . . . . 9
โข (ยฌ
๐ โ if(๐, ๐ด, 0) = 0) |
25 | 24 | adantl 483 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ if(๐, ๐ด, 0) = 0) |
26 | 25 | oveq1d 7373 |
. . . . . . 7
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ (if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) = (0 + if(๐, ๐ด, 0))) |
27 | 3 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ if(๐, ๐ด, 0) โ โ) |
28 | 27 | addid2d 11361 |
. . . . . . 7
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ (0 + if(๐, ๐ด, 0)) = if(๐, ๐ด, 0)) |
29 | 26, 28 | eqtrd 2773 |
. . . . . 6
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ (if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) = if(๐, ๐ด, 0)) |
30 | 29 | oveq1d 7373 |
. . . . 5
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + ๐ด) = (if(๐, ๐ด, 0) + ๐ด)) |
31 | | 2cnd 12236 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ 2 โ
โ) |
32 | | id 22 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ ๐ด โ
โ) |
33 | 31, 32 | mulcld 11180 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (2
ยท ๐ด) โ
โ) |
34 | 33 | addid2d 11361 |
. . . . . . . . . 10
โข (๐ด โ โ โ (0 + (2
ยท ๐ด)) = (2 ยท
๐ด)) |
35 | | 2times 12294 |
. . . . . . . . . 10
โข (๐ด โ โ โ (2
ยท ๐ด) = (๐ด + ๐ด)) |
36 | 34, 35 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ด โ โ โ (0 + (2
ยท ๐ด)) = (๐ด + ๐ด)) |
37 | 36 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐) โ (0 + (2 ยท ๐ด)) = (๐ด + ๐ด)) |
38 | | iftrue 4493 |
. . . . . . . . . 10
โข (๐ โ if(๐, 0, ๐ด) = 0) |
39 | 38 | adantl 483 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐) โ if(๐, 0, ๐ด) = 0) |
40 | | iftrue 4493 |
. . . . . . . . . 10
โข (๐ โ if(๐, (2 ยท ๐ด), 0) = (2 ยท ๐ด)) |
41 | 40 | adantl 483 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐) โ if(๐, (2 ยท ๐ด), 0) = (2 ยท ๐ด)) |
42 | 39, 41 | oveq12d 7376 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐) โ (if(๐, 0, ๐ด) + if(๐, (2 ยท ๐ด), 0)) = (0 + (2 ยท ๐ด))) |
43 | | iftrue 4493 |
. . . . . . . . . 10
โข (๐ โ if(๐, ๐ด, 0) = ๐ด) |
44 | 43 | adantl 483 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐) โ if(๐, ๐ด, 0) = ๐ด) |
45 | 44 | oveq1d 7373 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐) โ (if(๐, ๐ด, 0) + ๐ด) = (๐ด + ๐ด)) |
46 | 37, 42, 45 | 3eqtr4d 2783 |
. . . . . . 7
โข ((๐ด โ โ โง ๐) โ (if(๐, 0, ๐ด) + if(๐, (2 ยท ๐ด), 0)) = (if(๐, ๐ด, 0) + ๐ด)) |
47 | | simpl 484 |
. . . . . . . . 9
โข ((๐ด โ โ โง ยฌ
๐) โ ๐ด โ โ) |
48 | | 0cnd 11153 |
. . . . . . . . 9
โข ((๐ด โ โ โง ยฌ
๐) โ 0 โ
โ) |
49 | 47, 48 | addcomd 11362 |
. . . . . . . 8
โข ((๐ด โ โ โง ยฌ
๐) โ (๐ด + 0) = (0 + ๐ด)) |
50 | | iffalse 4496 |
. . . . . . . . . 10
โข (ยฌ
๐ โ if(๐, 0, ๐ด) = ๐ด) |
51 | 50 | adantl 483 |
. . . . . . . . 9
โข ((๐ด โ โ โง ยฌ
๐) โ if(๐, 0, ๐ด) = ๐ด) |
52 | | iffalse 4496 |
. . . . . . . . . 10
โข (ยฌ
๐ โ if(๐, (2 ยท ๐ด), 0) = 0) |
53 | 52 | adantl 483 |
. . . . . . . . 9
โข ((๐ด โ โ โง ยฌ
๐) โ if(๐, (2 ยท ๐ด), 0) = 0) |
54 | 51, 53 | oveq12d 7376 |
. . . . . . . 8
โข ((๐ด โ โ โง ยฌ
๐) โ (if(๐, 0, ๐ด) + if(๐, (2 ยท ๐ด), 0)) = (๐ด + 0)) |
55 | | iffalse 4496 |
. . . . . . . . . 10
โข (ยฌ
๐ โ if(๐, ๐ด, 0) = 0) |
56 | 55 | adantl 483 |
. . . . . . . . 9
โข ((๐ด โ โ โง ยฌ
๐) โ if(๐, ๐ด, 0) = 0) |
57 | 56 | oveq1d 7373 |
. . . . . . . 8
โข ((๐ด โ โ โง ยฌ
๐) โ (if(๐, ๐ด, 0) + ๐ด) = (0 + ๐ด)) |
58 | 49, 54, 57 | 3eqtr4d 2783 |
. . . . . . 7
โข ((๐ด โ โ โง ยฌ
๐) โ (if(๐, 0, ๐ด) + if(๐, (2 ยท ๐ด), 0)) = (if(๐, ๐ด, 0) + ๐ด)) |
59 | 46, 58 | pm2.61dan 812 |
. . . . . 6
โข (๐ด โ โ โ (if(๐, 0, ๐ด) + if(๐, (2 ยท ๐ด), 0)) = (if(๐, ๐ด, 0) + ๐ด)) |
60 | 59 | ad2antrr 725 |
. . . . 5
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ (if(๐, 0, ๐ด) + if(๐, (2 ยท ๐ด), 0)) = (if(๐, ๐ด, 0) + ๐ด)) |
61 | | ifnot 4539 |
. . . . . . 7
โข if(ยฌ
๐, ๐ด, 0) = if(๐, 0, ๐ด) |
62 | | nbn2 371 |
. . . . . . . . 9
โข (ยฌ
๐ โ (ยฌ ๐ โ (๐ โ ๐))) |
63 | 62 | adantl 483 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ (ยฌ ๐ โ (๐ โ ๐))) |
64 | 63 | ifbid 4510 |
. . . . . . 7
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ if(ยฌ ๐, ๐ด, 0) = if((๐ โ ๐), ๐ด, 0)) |
65 | 61, 64 | eqtr3id 2787 |
. . . . . 6
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ if(๐, 0, ๐ด) = if((๐ โ ๐), ๐ด, 0)) |
66 | | biorf 936 |
. . . . . . . 8
โข (ยฌ
๐ โ (๐ โ (๐ โจ ๐))) |
67 | 66 | adantl 483 |
. . . . . . 7
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ (๐ โ (๐ โจ ๐))) |
68 | 67 | ifbid 4510 |
. . . . . 6
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ if(๐, (2 ยท ๐ด), 0) = if((๐ โจ ๐), (2 ยท ๐ด), 0)) |
69 | 65, 68 | oveq12d 7376 |
. . . . 5
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ (if(๐, 0, ๐ด) + if(๐, (2 ยท ๐ด), 0)) = (if((๐ โ ๐), ๐ด, 0) + if((๐ โจ ๐), (2 ยท ๐ด), 0))) |
70 | 30, 60, 69 | 3eqtr2rd 2780 |
. . . 4
โข (((๐ด โ โ โง ๐) โง ยฌ ๐) โ (if((๐ โ ๐), ๐ด, 0) + if((๐ โจ ๐), (2 ยท ๐ด), 0)) = ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + ๐ด)) |
71 | 23, 70 | pm2.61dan 812 |
. . 3
โข ((๐ด โ โ โง ๐) โ (if((๐ โ ๐), ๐ด, 0) + if((๐ โจ ๐), (2 ยท ๐ด), 0)) = ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + ๐ด)) |
72 | | hadrot 1603 |
. . . . . . 7
โข
(hadd(๐, ๐, ๐) โ hadd(๐, ๐, ๐)) |
73 | | had1 1605 |
. . . . . . 7
โข (๐ โ (hadd(๐, ๐, ๐) โ (๐ โ ๐))) |
74 | 72, 73 | bitr3id 285 |
. . . . . 6
โข (๐ โ (hadd(๐, ๐, ๐) โ (๐ โ ๐))) |
75 | 74 | adantl 483 |
. . . . 5
โข ((๐ด โ โ โง ๐) โ (hadd(๐, ๐, ๐) โ (๐ โ ๐))) |
76 | 75 | ifbid 4510 |
. . . 4
โข ((๐ด โ โ โง ๐) โ if(hadd(๐, ๐, ๐), ๐ด, 0) = if((๐ โ ๐), ๐ด, 0)) |
77 | | cad1 1619 |
. . . . . 6
โข (๐ โ (cadd(๐, ๐, ๐) โ (๐ โจ ๐))) |
78 | 77 | adantl 483 |
. . . . 5
โข ((๐ด โ โ โง ๐) โ (cadd(๐, ๐, ๐) โ (๐ โจ ๐))) |
79 | 78 | ifbid 4510 |
. . . 4
โข ((๐ด โ โ โง ๐) โ if(cadd(๐, ๐, ๐), (2 ยท ๐ด), 0) = if((๐ โจ ๐), (2 ยท ๐ด), 0)) |
80 | 76, 79 | oveq12d 7376 |
. . 3
โข ((๐ด โ โ โง ๐) โ (if(hadd(๐, ๐, ๐), ๐ด, 0) + if(cadd(๐, ๐, ๐), (2 ยท ๐ด), 0)) = (if((๐ โ ๐), ๐ด, 0) + if((๐ โจ ๐), (2 ยท ๐ด), 0))) |
81 | | iftrue 4493 |
. . . . 5
โข (๐ โ if(๐, ๐ด, 0) = ๐ด) |
82 | 81 | adantl 483 |
. . . 4
โข ((๐ด โ โ โง ๐) โ if(๐, ๐ด, 0) = ๐ด) |
83 | 82 | oveq2d 7374 |
. . 3
โข ((๐ด โ โ โง ๐) โ ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + if(๐, ๐ด, 0)) = ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + ๐ด)) |
84 | 71, 80, 83 | 3eqtr4d 2783 |
. 2
โข ((๐ด โ โ โง ๐) โ (if(hadd(๐, ๐, ๐), ๐ด, 0) + if(cadd(๐, ๐, ๐), (2 ยท ๐ด), 0)) = ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + if(๐, ๐ด, 0))) |
85 | 19 | adantl 483 |
. . . . . 6
โข (((๐ด โ โ โง ยฌ
๐) โง ๐) โ if(๐, ๐ด, 0) = ๐ด) |
86 | 85 | oveq1d 7373 |
. . . . 5
โข (((๐ด โ โ โง ยฌ
๐) โง ๐) โ (if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) = (๐ด + if(๐, ๐ด, 0))) |
87 | 44 | oveq2d 7374 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐) โ (๐ด + if(๐, ๐ด, 0)) = (๐ด + ๐ด)) |
88 | 37, 42, 87 | 3eqtr4d 2783 |
. . . . . . 7
โข ((๐ด โ โ โง ๐) โ (if(๐, 0, ๐ด) + if(๐, (2 ยท ๐ด), 0)) = (๐ด + if(๐, ๐ด, 0))) |
89 | 53, 56 | eqtr4d 2776 |
. . . . . . . 8
โข ((๐ด โ โ โง ยฌ
๐) โ if(๐, (2 ยท ๐ด), 0) = if(๐, ๐ด, 0)) |
90 | 51, 89 | oveq12d 7376 |
. . . . . . 7
โข ((๐ด โ โ โง ยฌ
๐) โ (if(๐, 0, ๐ด) + if(๐, (2 ยท ๐ด), 0)) = (๐ด + if(๐, ๐ด, 0))) |
91 | 88, 90 | pm2.61dan 812 |
. . . . . 6
โข (๐ด โ โ โ (if(๐, 0, ๐ด) + if(๐, (2 ยท ๐ด), 0)) = (๐ด + if(๐, ๐ด, 0))) |
92 | 91 | ad2antrr 725 |
. . . . 5
โข (((๐ด โ โ โง ยฌ
๐) โง ๐) โ (if(๐, 0, ๐ด) + if(๐, (2 ยท ๐ด), 0)) = (๐ด + if(๐, ๐ด, 0))) |
93 | 9 | adantl 483 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ยฌ
๐) โง ๐) โ (๐ โ (๐ โ ๐))) |
94 | 93 | notbid 318 |
. . . . . . . . 9
โข (((๐ด โ โ โง ยฌ
๐) โง ๐) โ (ยฌ ๐ โ ยฌ (๐ โ ๐))) |
95 | | df-xor 1511 |
. . . . . . . . 9
โข ((๐ โป ๐) โ ยฌ (๐ โ ๐)) |
96 | 94, 95 | bitr4di 289 |
. . . . . . . 8
โข (((๐ด โ โ โง ยฌ
๐) โง ๐) โ (ยฌ ๐ โ (๐ โป ๐))) |
97 | 96 | ifbid 4510 |
. . . . . . 7
โข (((๐ด โ โ โง ยฌ
๐) โง ๐) โ if(ยฌ ๐, ๐ด, 0) = if((๐ โป ๐), ๐ด, 0)) |
98 | 61, 97 | eqtr3id 2787 |
. . . . . 6
โข (((๐ด โ โ โง ยฌ
๐) โง ๐) โ if(๐, 0, ๐ด) = if((๐ โป ๐), ๐ด, 0)) |
99 | | ibar 530 |
. . . . . . . 8
โข (๐ โ (๐ โ (๐ โง ๐))) |
100 | 99 | adantl 483 |
. . . . . . 7
โข (((๐ด โ โ โง ยฌ
๐) โง ๐) โ (๐ โ (๐ โง ๐))) |
101 | 100 | ifbid 4510 |
. . . . . 6
โข (((๐ด โ โ โง ยฌ
๐) โง ๐) โ if(๐, (2 ยท ๐ด), 0) = if((๐ โง ๐), (2 ยท ๐ด), 0)) |
102 | 98, 101 | oveq12d 7376 |
. . . . 5
โข (((๐ด โ โ โง ยฌ
๐) โง ๐) โ (if(๐, 0, ๐ด) + if(๐, (2 ยท ๐ด), 0)) = (if((๐ โป ๐), ๐ด, 0) + if((๐ โง ๐), (2 ยท ๐ด), 0))) |
103 | 86, 92, 102 | 3eqtr2rd 2780 |
. . . 4
โข (((๐ด โ โ โง ยฌ
๐) โง ๐) โ (if((๐ โป ๐), ๐ด, 0) + if((๐ โง ๐), (2 ยท ๐ด), 0)) = (if(๐, ๐ด, 0) + if(๐, ๐ด, 0))) |
104 | | simplll 774 |
. . . . . . 7
โข ((((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โง ๐) โ ๐ด โ โ) |
105 | | 0cnd 11153 |
. . . . . . 7
โข ((((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โง ยฌ ๐) โ 0 โ โ) |
106 | 104, 105 | ifclda 4522 |
. . . . . 6
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ if(๐, ๐ด, 0) โ โ) |
107 | | 0cnd 11153 |
. . . . . 6
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ 0 โ
โ) |
108 | 106, 107 | addcomd 11362 |
. . . . 5
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ (if(๐, ๐ด, 0) + 0) = (0 + if(๐, ๐ด, 0))) |
109 | 62 | adantl 483 |
. . . . . . . . 9
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ (ยฌ ๐ โ (๐ โ ๐))) |
110 | 109 | con1bid 356 |
. . . . . . . 8
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ (ยฌ (๐ โ ๐) โ ๐)) |
111 | 95, 110 | bitrid 283 |
. . . . . . 7
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ ((๐ โป ๐) โ ๐)) |
112 | 111 | ifbid 4510 |
. . . . . 6
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ if((๐ โป ๐), ๐ด, 0) = if(๐, ๐ด, 0)) |
113 | | simpr 486 |
. . . . . . . 8
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ ยฌ ๐) |
114 | 113 | intnanrd 491 |
. . . . . . 7
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ ยฌ (๐ โง ๐)) |
115 | | iffalse 4496 |
. . . . . . 7
โข (ยฌ
(๐ โง ๐) โ if((๐ โง ๐), (2 ยท ๐ด), 0) = 0) |
116 | 114, 115 | syl 17 |
. . . . . 6
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ if((๐ โง ๐), (2 ยท ๐ด), 0) = 0) |
117 | 112, 116 | oveq12d 7376 |
. . . . 5
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ (if((๐ โป ๐), ๐ด, 0) + if((๐ โง ๐), (2 ยท ๐ด), 0)) = (if(๐, ๐ด, 0) + 0)) |
118 | 24 | adantl 483 |
. . . . . 6
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ if(๐, ๐ด, 0) = 0) |
119 | 118 | oveq1d 7373 |
. . . . 5
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ (if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) = (0 + if(๐, ๐ด, 0))) |
120 | 108, 117,
119 | 3eqtr4d 2783 |
. . . 4
โข (((๐ด โ โ โง ยฌ
๐) โง ยฌ ๐) โ (if((๐ โป ๐), ๐ด, 0) + if((๐ โง ๐), (2 ยท ๐ด), 0)) = (if(๐, ๐ด, 0) + if(๐, ๐ด, 0))) |
121 | 103, 120 | pm2.61dan 812 |
. . 3
โข ((๐ด โ โ โง ยฌ
๐) โ (if((๐ โป ๐), ๐ด, 0) + if((๐ โง ๐), (2 ยท ๐ด), 0)) = (if(๐, ๐ด, 0) + if(๐, ๐ด, 0))) |
122 | | had0 1606 |
. . . . . . 7
โข (ยฌ
๐ โ (hadd(๐, ๐, ๐) โ (๐ โป ๐))) |
123 | 72, 122 | bitr3id 285 |
. . . . . 6
โข (ยฌ
๐ โ (hadd(๐, ๐, ๐) โ (๐ โป ๐))) |
124 | 123 | adantl 483 |
. . . . 5
โข ((๐ด โ โ โง ยฌ
๐) โ (hadd(๐, ๐, ๐) โ (๐ โป ๐))) |
125 | 124 | ifbid 4510 |
. . . 4
โข ((๐ด โ โ โง ยฌ
๐) โ if(hadd(๐, ๐, ๐), ๐ด, 0) = if((๐ โป ๐), ๐ด, 0)) |
126 | | cad0 1620 |
. . . . . 6
โข (ยฌ
๐ โ (cadd(๐, ๐, ๐) โ (๐ โง ๐))) |
127 | 126 | adantl 483 |
. . . . 5
โข ((๐ด โ โ โง ยฌ
๐) โ (cadd(๐, ๐, ๐) โ (๐ โง ๐))) |
128 | 127 | ifbid 4510 |
. . . 4
โข ((๐ด โ โ โง ยฌ
๐) โ if(cadd(๐, ๐, ๐), (2 ยท ๐ด), 0) = if((๐ โง ๐), (2 ยท ๐ด), 0)) |
129 | 125, 128 | oveq12d 7376 |
. . 3
โข ((๐ด โ โ โง ยฌ
๐) โ (if(hadd(๐, ๐, ๐), ๐ด, 0) + if(cadd(๐, ๐, ๐), (2 ยท ๐ด), 0)) = (if((๐ โป ๐), ๐ด, 0) + if((๐ โง ๐), (2 ยท ๐ด), 0))) |
130 | | iffalse 4496 |
. . . . 5
โข (ยฌ
๐ โ if(๐, ๐ด, 0) = 0) |
131 | 130 | oveq2d 7374 |
. . . 4
โข (ยฌ
๐ โ ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + if(๐, ๐ด, 0)) = ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + 0)) |
132 | | ifcl 4532 |
. . . . . . 7
โข ((๐ด โ โ โง 0 โ
โ) โ if(๐, ๐ด, 0) โ
โ) |
133 | 1, 132 | mpan2 690 |
. . . . . 6
โข (๐ด โ โ โ if(๐, ๐ด, 0) โ โ) |
134 | 133, 3 | addcld 11179 |
. . . . 5
โข (๐ด โ โ โ (if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) โ โ) |
135 | 134 | addid1d 11360 |
. . . 4
โข (๐ด โ โ โ
((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + 0) = (if(๐, ๐ด, 0) + if(๐, ๐ด, 0))) |
136 | 131, 135 | sylan9eqr 2795 |
. . 3
โข ((๐ด โ โ โง ยฌ
๐) โ ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + if(๐, ๐ด, 0)) = (if(๐, ๐ด, 0) + if(๐, ๐ด, 0))) |
137 | 121, 129,
136 | 3eqtr4d 2783 |
. 2
โข ((๐ด โ โ โง ยฌ
๐) โ (if(hadd(๐, ๐, ๐), ๐ด, 0) + if(cadd(๐, ๐, ๐), (2 ยท ๐ด), 0)) = ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + if(๐, ๐ด, 0))) |
138 | 84, 137 | pm2.61dan 812 |
1
โข (๐ด โ โ โ
(if(hadd(๐, ๐, ๐), ๐ด, 0) + if(cadd(๐, ๐, ๐), (2 ยท ๐ด), 0)) = ((if(๐, ๐ด, 0) + if(๐, ๐ด, 0)) + if(๐, ๐ด, 0))) |