Step | Hyp | Ref
| Expression |
1 | | itgsplit.a |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ
๐ฟ1) |
2 | | iblmbf 25054 |
. . . . . . . . . 10
โข ((๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1 โ (๐ฅ โ ๐ด โฆ ๐ถ) โ MblFn) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ MblFn) |
4 | | ssun1 4131 |
. . . . . . . . . . . 12
โข ๐ด โ (๐ด โช ๐ต) |
5 | | itgsplit.u |
. . . . . . . . . . . 12
โข (๐ โ ๐ = (๐ด โช ๐ต)) |
6 | 4, 5 | sseqtrrid 3996 |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ ๐) |
7 | 6 | sselda 3943 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ฅ โ ๐) |
8 | | itgsplit.c |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐) โ ๐ถ โ ๐) |
9 | 7, 8 | syldan 592 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ ๐) |
10 | 3, 9 | mbfdm2 24923 |
. . . . . . . 8
โข (๐ โ ๐ด โ dom vol) |
11 | 10 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ ๐ด โ dom vol) |
12 | | itgsplit.b |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ ๐ต โฆ ๐ถ) โ
๐ฟ1) |
13 | | iblmbf 25054 |
. . . . . . . . . 10
โข ((๐ฅ โ ๐ต โฆ ๐ถ) โ ๐ฟ1 โ (๐ฅ โ ๐ต โฆ ๐ถ) โ MblFn) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ ๐ต โฆ ๐ถ) โ MblFn) |
15 | | ssun2 4132 |
. . . . . . . . . . . 12
โข ๐ต โ (๐ด โช ๐ต) |
16 | 15, 5 | sseqtrrid 3996 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ ๐) |
17 | 16 | sselda 3943 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ฅ โ ๐) |
18 | 17, 8 | syldan 592 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ถ โ ๐) |
19 | 14, 18 | mbfdm2 24923 |
. . . . . . . 8
โข (๐ โ ๐ต โ dom vol) |
20 | 19 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ ๐ต โ dom vol) |
21 | | itgsplit.i |
. . . . . . . 8
โข (๐ โ (vol*โ(๐ด โฉ ๐ต)) = 0) |
22 | 21 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ (vol*โ(๐ด โฉ ๐ต)) = 0) |
23 | 5 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ ๐ = (๐ด โช ๐ต)) |
24 | 5 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ฅ โ ๐ โ ๐ฅ โ (๐ด โช ๐ต))) |
25 | | elun 4107 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ (๐ด โช ๐ต) โ (๐ฅ โ ๐ด โจ ๐ฅ โ ๐ต)) |
26 | 24, 25 | bitrdi 287 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ฅ โ ๐ โ (๐ฅ โ ๐ด โจ ๐ฅ โ ๐ต))) |
27 | 26 | biimpa 478 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐) โ (๐ฅ โ ๐ด โจ ๐ฅ โ ๐ต)) |
28 | 3, 9 | mbfmptcl 24922 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) |
29 | 14, 18 | mbfmptcl 24922 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ถ โ โ) |
30 | 28, 29 | jaodan 957 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฅ โ ๐ด โจ ๐ฅ โ ๐ต)) โ ๐ถ โ โ) |
31 | 27, 30 | syldan 592 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐) โ ๐ถ โ โ) |
32 | 31 | adantlr 714 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐) โ ๐ถ โ โ) |
33 | | ax-icn 11044 |
. . . . . . . . . . . . . 14
โข i โ
โ |
34 | | elfznn0 13463 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0...3) โ ๐ โ
โ0) |
35 | 34 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (0...3)) โ ๐ โ โ0) |
36 | | expcl 13914 |
. . . . . . . . . . . . . 14
โข ((i
โ โ โง ๐
โ โ0) โ (iโ๐) โ โ) |
37 | 33, 35, 36 | sylancr 588 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (0...3)) โ (iโ๐) โ
โ) |
38 | 37 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐) โ (iโ๐) โ โ) |
39 | | ine0 11524 |
. . . . . . . . . . . . . 14
โข i โ
0 |
40 | | elfzelz 13370 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0...3) โ ๐ โ
โค) |
41 | 40 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (0...3)) โ ๐ โ โค) |
42 | | expne0i 13929 |
. . . . . . . . . . . . . 14
โข ((i
โ โ โง i โ 0 โง ๐ โ โค) โ (iโ๐) โ 0) |
43 | 33, 39, 41, 42 | mp3an12i 1466 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (0...3)) โ (iโ๐) โ 0) |
44 | 43 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐) โ (iโ๐) โ 0) |
45 | 32, 38, 44 | divcld 11865 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐) โ (๐ถ / (iโ๐)) โ โ) |
46 | 45 | recld 15013 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐) โ (โโ(๐ถ / (iโ๐))) โ โ) |
47 | | 0re 11091 |
. . . . . . . . . 10
โข 0 โ
โ |
48 | | ifcl 4530 |
. . . . . . . . . 10
โข
(((โโ(๐ถ /
(iโ๐))) โ โ
โง 0 โ โ) โ if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0) โ โ) |
49 | 46, 47, 48 | sylancl 587 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐) โ if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0) โ โ) |
50 | 49 | rexrd 11139 |
. . . . . . . 8
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐) โ if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0) โ
โ*) |
51 | | max1 13033 |
. . . . . . . . 9
โข ((0
โ โ โง (โโ(๐ถ / (iโ๐))) โ โ) โ 0 โค if(0 โค
(โโ(๐ถ /
(iโ๐))),
(โโ(๐ถ /
(iโ๐))),
0)) |
52 | 47, 46, 51 | sylancr 588 |
. . . . . . . 8
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐) โ 0 โค if(0 โค
(โโ(๐ถ /
(iโ๐))),
(โโ(๐ถ /
(iโ๐))),
0)) |
53 | | elxrge0 13303 |
. . . . . . . 8
โข (if(0
โค (โโ(๐ถ /
(iโ๐))),
(โโ(๐ถ /
(iโ๐))), 0) โ
(0[,]+โ) โ (if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0) โ โ* โง 0
โค if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0))) |
54 | 50, 52, 53 | sylanbrc 584 |
. . . . . . 7
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐) โ if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0) โ
(0[,]+โ)) |
55 | | ifan 4538 |
. . . . . . . 8
โข if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) = if(๐ฅ โ ๐ด, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) |
56 | 55 | mpteq2i 5209 |
. . . . . . 7
โข (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0)) |
57 | | ifan 4538 |
. . . . . . . 8
โข if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) = if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) |
58 | 57 | mpteq2i 5209 |
. . . . . . 7
โข (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0)) |
59 | | ifan 4538 |
. . . . . . . 8
โข if((๐ฅ โ ๐ โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) = if(๐ฅ โ ๐, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) |
60 | 59 | mpteq2i 5209 |
. . . . . . 7
โข (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0)) |
61 | | eqidd 2739 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) |
62 | | eqidd 2739 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ(๐ถ / (iโ๐))) = (โโ(๐ถ / (iโ๐)))) |
63 | 61, 62, 1, 9 | iblitg 25055 |
. . . . . . . 8
โข ((๐ โง ๐ โ โค) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) โ โ) |
64 | 40, 63 | sylan2 594 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) โ โ) |
65 | | eqidd 2739 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) |
66 | | eqidd 2739 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ต) โ (โโ(๐ถ / (iโ๐))) = (โโ(๐ถ / (iโ๐)))) |
67 | 65, 66, 12, 18 | iblitg 25055 |
. . . . . . . 8
โข ((๐ โง ๐ โ โค) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) โ โ) |
68 | 40, 67 | sylan2 594 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) โ โ) |
69 | 11, 20, 22, 23, 54, 56, 58, 60, 64, 68 | itg2split 25036 |
. . . . . 6
โข ((๐ โง ๐ โ (0...3)) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) = ((โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0))) +
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))))) |
70 | 69 | oveq2d 7366 |
. . . . 5
โข ((๐ โง ๐ โ (0...3)) โ ((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))) = ((iโ๐) ยท ((โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0))) +
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))))) |
71 | 63 | recnd 11117 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) โ โ) |
72 | 40, 71 | sylan2 594 |
. . . . . 6
โข ((๐ โง ๐ โ (0...3)) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) โ โ) |
73 | 68 | recnd 11117 |
. . . . . 6
โข ((๐ โง ๐ โ (0...3)) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) โ โ) |
74 | 37, 72, 73 | adddid 11113 |
. . . . 5
โข ((๐ โง ๐ โ (0...3)) โ ((iโ๐) ยท
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) + (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0))))) =
(((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))) + ((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))))) |
75 | 70, 74 | eqtrd 2778 |
. . . 4
โข ((๐ โง ๐ โ (0...3)) โ ((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))) = (((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)))) +
((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))))) |
76 | 75 | sumeq2dv 15523 |
. . 3
โข (๐ โ ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)))) =
ฮฃ๐ โ
(0...3)(((iโ๐)
ยท (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))) + ((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))))) |
77 | | fzfid 13807 |
. . . 4
โข (๐ โ (0...3) โ
Fin) |
78 | 37, 72 | mulcld 11109 |
. . . 4
โข ((๐ โง ๐ โ (0...3)) โ ((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))) โ โ) |
79 | 37, 73 | mulcld 11109 |
. . . 4
โข ((๐ โง ๐ โ (0...3)) โ ((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))) โ โ) |
80 | 77, 78, 79 | fsumadd 15560 |
. . 3
โข (๐ โ ฮฃ๐ โ (0...3)(((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)))) +
((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))))) = (ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)))) +
ฮฃ๐ โ
(0...3)((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))))) |
81 | 76, 80 | eqtrd 2778 |
. 2
โข (๐ โ ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)))) =
(ฮฃ๐ โ
(0...3)((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))) + ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))))) |
82 | | eqid 2738 |
. . 3
โข
(โโ(๐ถ /
(iโ๐))) =
(โโ(๐ถ /
(iโ๐))) |
83 | 82 | dfitg 25056 |
. 2
โข
โซ๐๐ถ d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))) |
84 | 82 | dfitg 25056 |
. . 3
โข
โซ๐ด๐ถ d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))) |
85 | 82 | dfitg 25056 |
. . 3
โข
โซ๐ต๐ถ d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))) |
86 | 84, 85 | oveq12i 7362 |
. 2
โข
(โซ๐ด๐ถ d๐ฅ + โซ๐ต๐ถ d๐ฅ) = (ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)))) +
ฮฃ๐ โ
(0...3)((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))))) |
87 | 81, 83, 86 | 3eqtr4g 2803 |
1
โข (๐ โ โซ๐๐ถ d๐ฅ = (โซ๐ด๐ถ d๐ฅ + โซ๐ต๐ถ d๐ฅ)) |