Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . . . . 10
โข ((๐ โ (0...3) โง ๐ฅ โ โ) โ ๐ฅ โ
โ) |
2 | 1 | biantrud 533 |
. . . . . . . . 9
โข ((๐ โ (0...3) โง ๐ฅ โ โ) โ (๐ฅ โ ๐ด โ (๐ฅ โ ๐ด โง ๐ฅ โ โ))) |
3 | | elin 3930 |
. . . . . . . . 9
โข (๐ฅ โ (๐ด โฉ โ) โ (๐ฅ โ ๐ด โง ๐ฅ โ โ)) |
4 | 2, 3 | bitr4di 289 |
. . . . . . . 8
โข ((๐ โ (0...3) โง ๐ฅ โ โ) โ (๐ฅ โ ๐ด โ ๐ฅ โ (๐ด โฉ โ))) |
5 | 4 | anbi1d 631 |
. . . . . . 7
โข ((๐ โ (0...3) โง ๐ฅ โ โ) โ ((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))) โ (๐ฅ โ (๐ด โฉ โ) โง 0 โค
(โโ(๐ต /
(iโ๐)))))) |
6 | 5 | ifbid 4513 |
. . . . . 6
โข ((๐ โ (0...3) โง ๐ฅ โ โ) โ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0) =
if((๐ฅ โ (๐ด โฉ โ) โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))),
0)) |
7 | 6 | mpteq2dva 5209 |
. . . . 5
โข (๐ โ (0...3) โ (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0)) = (๐ฅ โ โ โฆ
if((๐ฅ โ (๐ด โฉ โ) โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))),
0))) |
8 | 7 | fveq2d 6850 |
. . . 4
โข (๐ โ (0...3) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0))) = (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ (๐ด โฉ โ) โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))),
0)))) |
9 | 8 | oveq2d 7377 |
. . 3
โข (๐ โ (0...3) โ
((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0)))) = ((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ (๐ด โฉ โ) โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))),
0))))) |
10 | 9 | sumeq2i 15592 |
. 2
โข
ฮฃ๐ โ
(0...3)((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0)))) = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ (๐ด โฉ โ) โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))),
0)))) |
11 | | eqid 2733 |
. . 3
โข
(โโ(๐ต /
(iโ๐))) =
(โโ(๐ต /
(iโ๐))) |
12 | 11 | dfitg 25157 |
. 2
โข
โซ๐ด๐ต d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))),
0)))) |
13 | 11 | dfitg 25157 |
. 2
โข
โซ(๐ด โฉ
โ)๐ต d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ (๐ด โฉ โ) โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))),
0)))) |
14 | 10, 12, 13 | 3eqtr4i 2771 |
1
โข
โซ๐ด๐ต d๐ฅ = โซ(๐ด โฉ โ)๐ต d๐ฅ |