Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
โข โ =
โ |
2 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))) โ ๐ฅ โ ๐ด) |
3 | 2 | con3i 154 |
. . . . . . . . . . 11
โข (ยฌ
๐ฅ โ ๐ด โ ยฌ (๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐))))) |
4 | 3 | iffalsed 4501 |
. . . . . . . . . 10
โข (ยฌ
๐ฅ โ ๐ด โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0) = 0) |
5 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))) โ ๐ฅ โ ๐ด) |
6 | 5 | con3i 154 |
. . . . . . . . . . 11
โข (ยฌ
๐ฅ โ ๐ด โ ยฌ (๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐))))) |
7 | 6 | iffalsed 4501 |
. . . . . . . . . 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 7384 |
. . . . . . . . . . . 12
โข (๐ต = ๐ถ โ (โโ(๐ต / (iโ๐))) = (โโ(๐ถ / (iโ๐)))) |
10 | 9 | breq2d 5121 |
. . . . . . . . . . 11
โข (๐ต = ๐ถ โ (0 โค (โโ(๐ต / (iโ๐))) โ 0 โค (โโ(๐ถ / (iโ๐))))) |
11 | 10 | anbi2d 630 |
. . . . . . . . . 10
โข (๐ต = ๐ถ โ ((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))) โ (๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))))) |
12 | 11, 9 | ifbieq1d 4514 |
. . . . . . . . 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 3078 |
. . . . . 6
โข
(โ๐ฅ โ
๐ด ๐ต = ๐ถ โ โ๐ฅ โ โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0) = if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) |
16 | | mpteq12 5201 |
. . . . . 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 6850 |
. . . 4
โข
(โ๐ฅ โ
๐ด ๐ต = ๐ถ โ (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0))) =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))) |
19 | 18 | oveq2d 7377 |
. . 3
โข
(โ๐ฅ โ
๐ด ๐ต = ๐ถ โ ((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0)))) =
((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))))) |
20 | 19 | sumeq2sdv 15597 |
. 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 25157 |
. 2
โข
โซ๐ด๐ต d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))),
0)))) |
23 | | eqid 2733 |
. . 3
โข
(โโ(๐ถ /
(iโ๐))) =
(โโ(๐ถ /
(iโ๐))) |
24 | 23 | dfitg 25157 |
. 2
โข
โซ๐ด๐ถ d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))) |
25 | 20, 22, 24 | 3eqtr4g 2798 |
1
โข
(โ๐ฅ โ
๐ด ๐ต = ๐ถ โ โซ๐ด๐ต d๐ฅ = โซ๐ด๐ถ d๐ฅ) |