Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
โข
(โโ(0 / (iโ๐))) = (โโ(0 / (iโ๐))) |
2 | 1 | dfitg 25157 |
. 2
โข
โซ๐ด0 d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค (โโ(0 /
(iโ๐)))),
(โโ(0 / (iโ๐))), 0)))) |
3 | | ax-icn 11118 |
. . . . . . . . . . . . . . 15
โข i โ
โ |
4 | | elfznn0 13543 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0...3) โ ๐ โ
โ0) |
5 | | expcl 13994 |
. . . . . . . . . . . . . . 15
โข ((i
โ โ โง ๐
โ โ0) โ (iโ๐) โ โ) |
6 | 3, 4, 5 | sylancr 588 |
. . . . . . . . . . . . . 14
โข (๐ โ (0...3) โ
(iโ๐) โ
โ) |
7 | | ine0 11598 |
. . . . . . . . . . . . . . 15
โข i โ
0 |
8 | | elfzelz 13450 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0...3) โ ๐ โ
โค) |
9 | | expne0i 14009 |
. . . . . . . . . . . . . . 15
โข ((i
โ โ โง i โ 0 โง ๐ โ โค) โ (iโ๐) โ 0) |
10 | 3, 7, 8, 9 | mp3an12i 1466 |
. . . . . . . . . . . . . 14
โข (๐ โ (0...3) โ
(iโ๐) โ
0) |
11 | 6, 10 | div0d 11938 |
. . . . . . . . . . . . 13
โข (๐ โ (0...3) โ (0 /
(iโ๐)) =
0) |
12 | 11 | fveq2d 6850 |
. . . . . . . . . . . 12
โข (๐ โ (0...3) โ
(โโ(0 / (iโ๐))) = (โโ0)) |
13 | | re0 15046 |
. . . . . . . . . . . 12
โข
(โโ0) = 0 |
14 | 12, 13 | eqtrdi 2789 |
. . . . . . . . . . 11
โข (๐ โ (0...3) โ
(โโ(0 / (iโ๐))) = 0) |
15 | 14 | ifeq1d 4509 |
. . . . . . . . . 10
โข (๐ โ (0...3) โ if((๐ฅ โ ๐ด โง 0 โค (โโ(0 /
(iโ๐)))),
(โโ(0 / (iโ๐))), 0) = if((๐ฅ โ ๐ด โง 0 โค (โโ(0 /
(iโ๐)))), 0,
0)) |
16 | | ifid 4530 |
. . . . . . . . . 10
โข if((๐ฅ โ ๐ด โง 0 โค (โโ(0 /
(iโ๐)))), 0, 0) =
0 |
17 | 15, 16 | eqtrdi 2789 |
. . . . . . . . 9
โข (๐ โ (0...3) โ if((๐ฅ โ ๐ด โง 0 โค (โโ(0 /
(iโ๐)))),
(โโ(0 / (iโ๐))), 0) = 0) |
18 | 17 | mpteq2dv 5211 |
. . . . . . . 8
โข (๐ โ (0...3) โ (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค (โโ(0 /
(iโ๐)))),
(โโ(0 / (iโ๐))), 0)) = (๐ฅ โ โ โฆ 0)) |
19 | | fconstmpt 5698 |
. . . . . . . 8
โข (โ
ร {0}) = (๐ฅ โ
โ โฆ 0) |
20 | 18, 19 | eqtr4di 2791 |
. . . . . . 7
โข (๐ โ (0...3) โ (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค (โโ(0 /
(iโ๐)))),
(โโ(0 / (iโ๐))), 0)) = (โ ร
{0})) |
21 | 20 | fveq2d 6850 |
. . . . . 6
โข (๐ โ (0...3) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(0 /
(iโ๐)))),
(โโ(0 / (iโ๐))), 0))) = (โซ2โ(โ
ร {0}))) |
22 | | itg20 25125 |
. . . . . 6
โข
(โซ2โ(โ ร {0})) = 0 |
23 | 21, 22 | eqtrdi 2789 |
. . . . 5
โข (๐ โ (0...3) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(0 /
(iโ๐)))),
(โโ(0 / (iโ๐))), 0))) = 0) |
24 | 23 | oveq2d 7377 |
. . . 4
โข (๐ โ (0...3) โ
((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(0 /
(iโ๐)))),
(โโ(0 / (iโ๐))), 0)))) = ((iโ๐) ยท 0)) |
25 | 6 | mul01d 11362 |
. . . 4
โข (๐ โ (0...3) โ
((iโ๐) ยท 0) =
0) |
26 | 24, 25 | eqtrd 2773 |
. . 3
โข (๐ โ (0...3) โ
((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(0 /
(iโ๐)))),
(โโ(0 / (iโ๐))), 0)))) = 0) |
27 | 26 | sumeq2i 15592 |
. 2
โข
ฮฃ๐ โ
(0...3)((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(0 /
(iโ๐)))),
(โโ(0 / (iโ๐))), 0)))) = ฮฃ๐ โ (0...3)0 |
28 | | fzfi 13886 |
. . . 4
โข (0...3)
โ Fin |
29 | 28 | olci 865 |
. . 3
โข ((0...3)
โ (โคโฅโ0) โจ (0...3) โ
Fin) |
30 | | sumz 15615 |
. . 3
โข (((0...3)
โ (โคโฅโ0) โจ (0...3) โ Fin) โ
ฮฃ๐ โ (0...3)0 =
0) |
31 | 29, 30 | ax-mp 5 |
. 2
โข
ฮฃ๐ โ
(0...3)0 = 0 |
32 | 2, 27, 31 | 3eqtri 2765 |
1
โข
โซ๐ด0 d๐ฅ = 0 |