| Step | Hyp | Ref
| Expression |
|---|
| 1 | | eqid 2733 |
. . . . . 6
โข โ =
โ |
| 2 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))) โ ๐ฅ โ ๐ด) |
| 3 | 2 | con3i 154 |
. . . . . . . . . . 11
โข (ยฌ
๐ฅ โ ๐ด โ ยฌ (๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐))))) |
| 4 | 3 | iffalsed 4540 |
. . . . . . . . . 10
โข (ยฌ
๐ฅ โ ๐ด โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0) = 0) |
| 5 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))) โ ๐ฅ โ ๐ด) |
| 6 | 5 | con3i 154 |
. . . . . . . . . . 11
โข (ยฌ
๐ฅ โ ๐ด โ ยฌ (๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐))))) |
| 7 | 6 | iffalsed 4540 |
. . . . . . . . . 10
โข (ยฌ
๐ฅ โ ๐ด โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) = 0) |
| 8 | 4, 7 | eqtr4d 2776 |
. . . . . . . . 9
โข (ยฌ
๐ฅ โ ๐ด โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0) = if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) |
| 9 | | fvoveq1 7432 |
. . . . . . . . . . . 12
โข (๐ต = ๐ถ โ (โโ(๐ต / (iโ๐))) = (โโ(๐ถ / (iโ๐)))) |
| 10 | 9 | breq2d 5161 |
. . . . . . . . . . 11
โข (๐ต = ๐ถ โ (0 โค (โโ(๐ต / (iโ๐))) โ 0 โค (โโ(๐ถ / (iโ๐))))) |
| 11 | 10 | anbi2d 630 |
. . . . . . . . . 10
โข (๐ต = ๐ถ โ ((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))) โ (๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))))) |
| 12 | 11, 9 | ifbieq1d 4553 |
. . . . . . . . 9
โข (๐ต = ๐ถ โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0) = if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) |
| 13 | 8, 12 | ja 186 |
. . . . . . . 8
โข ((๐ฅ โ ๐ด โ ๐ต = ๐ถ) โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0) = if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) |
| 14 | 13 | a1d 25 |
. . . . . . 7
โข ((๐ฅ โ ๐ด โ ๐ต = ๐ถ) โ (๐ฅ โ โ โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0) = if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) |
| 15 | 14 | ralimi2 3079 |
. . . . . 6
โข
(โ๐ฅ โ
๐ด ๐ต = ๐ถ โ โ๐ฅ โ โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0) = if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) |
| 16 | | mpteq12 5241 |
. . . . . 6
โข ((โ
= โ โง โ๐ฅ
โ โ if((๐ฅ โ
๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0) =
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)) โ
(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0)) = (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0))) |
| 17 | 1, 15, 16 | sylancr 588 |
. . . . 5
โข
(โ๐ฅ โ
๐ด ๐ต = ๐ถ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) |
| 18 | 17 | fveq2d 6896 |
. . . 4
โข
(โ๐ฅ โ
๐ด ๐ต = ๐ถ โ (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0))) =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))) |
| 19 | 18 | oveq2d 7425 |
. . 3
โข
(โ๐ฅ โ
๐ด ๐ต = ๐ถ โ ((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0)))) =
((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))))) |
| 20 | 19 | sumeq2sdv 15650 |
. 2
โข
(โ๐ฅ โ
๐ด ๐ต = ๐ถ โ ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0)))) =
ฮฃ๐ โ
(0...3)((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))))) |
| 21 | | eqid 2733 |
. . 3
โข
(โโ(๐ต /
(iโ๐))) =
(โโ(๐ต /
(iโ๐))) |
| 22 | 21 | dfitg 25287 |
. 2
โข
โซ๐ด๐ต d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))),
0)))) |
| 23 | | eqid 2733 |
. . 3
โข
(โโ(๐ถ /
(iโ๐))) =
(โโ(๐ถ /
(iโ๐))) |
| 24 | 23 | dfitg 25287 |
. 2
โข
โซ๐ด๐ถ d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))) |
| 25 | 20, 22, 24 | 3eqtr4g 2798 |
1
โข
(โ๐ฅ โ
๐ด ๐ต = ๐ถ โ โซ๐ด๐ต d๐ฅ = โซ๐ด๐ถ d๐ฅ) |
