Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
โข โ =
โ |
2 | | itgeq1f.1 |
. . . . . . . 8
โข
โฒ๐ฅ๐ด |
3 | | itgeq1f.2 |
. . . . . . . 8
โข
โฒ๐ฅ๐ต |
4 | 2, 3 | nfeq 2917 |
. . . . . . 7
โข
โฒ๐ฅ ๐ด = ๐ต |
5 | | eleq2 2823 |
. . . . . . . . . 10
โข (๐ด = ๐ต โ (๐ฅ โ ๐ด โ ๐ฅ โ ๐ต)) |
6 | 5 | anbi1d 631 |
. . . . . . . . 9
โข (๐ด = ๐ต โ ((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))) โ (๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))))) |
7 | 6 | ifbid 4513 |
. . . . . . . 8
โข (๐ด = ๐ต โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) = if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) |
8 | 7 | a1d 25 |
. . . . . . 7
โข (๐ด = ๐ต โ (๐ฅ โ โ โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) = if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) |
9 | 4, 8 | ralrimi 3239 |
. . . . . 6
โข (๐ด = ๐ต โ โ๐ฅ โ โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) = if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) |
10 | | mpteq12 5201 |
. . . . . 6
โข ((โ
= โ โง โ๐ฅ
โ โ if((๐ฅ โ
๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0) =
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)) โ
(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)) = (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0))) |
11 | 1, 9, 10 | sylancr 588 |
. . . . 5
โข (๐ด = ๐ต โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) |
12 | 11 | fveq2d 6850 |
. . . 4
โข (๐ด = ๐ต โ (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0))) =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))) |
13 | 12 | oveq2d 7377 |
. . 3
โข (๐ด = ๐ต โ ((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)))) =
((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))))) |
14 | 13 | sumeq2sdv 15597 |
. 2
โข (๐ด = ๐ต โ ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)))) =
ฮฃ๐ โ
(0...3)((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))))) |
15 | | eqid 2733 |
. . 3
โข
(โโ(๐ถ /
(iโ๐))) =
(โโ(๐ถ /
(iโ๐))) |
16 | 15 | dfitg 25157 |
. 2
โข
โซ๐ด๐ถ d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))) |
17 | 15 | dfitg 25157 |
. 2
โข
โซ๐ต๐ถ d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))) |
18 | 14, 16, 17 | 3eqtr4g 2798 |
1
โข (๐ด = ๐ต โ โซ๐ด๐ถ d๐ฅ = โซ๐ต๐ถ d๐ฅ) |