Step | Hyp | Ref
| Expression |
1 | | itgeqa.3 |
. . . . 5
โข (๐ โ ๐ด โ โ) |
2 | | itgeqa.4 |
. . . . 5
โข (๐ โ (vol*โ๐ด) = 0) |
3 | | itgeqa.5 |
. . . . 5
โข ((๐ โง ๐ฅ โ (๐ต โ ๐ด)) โ ๐ถ = ๐ท) |
4 | | itgeqa.1 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ถ โ โ) |
5 | | itgeqa.2 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ต) โ ๐ท โ โ) |
6 | 1, 2, 3, 4, 5 | mbfeqa 24929 |
. . . 4
โข (๐ โ ((๐ฅ โ ๐ต โฆ ๐ถ) โ MblFn โ (๐ฅ โ ๐ต โฆ ๐ท) โ MblFn)) |
7 | | ifan 4538 |
. . . . . . . . . 10
โข if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) = if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) |
8 | 4 | adantlr 714 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ ๐ถ โ โ) |
9 | | ax-icn 11044 |
. . . . . . . . . . . . . . . . 17
โข i โ
โ |
10 | | ine0 11524 |
. . . . . . . . . . . . . . . . 17
โข i โ
0 |
11 | | elfzelz 13370 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (0...3) โ ๐ โ
โค) |
12 | 11 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ ๐ โ โค) |
13 | | expclz 13921 |
. . . . . . . . . . . . . . . . 17
โข ((i
โ โ โง i โ 0 โง ๐ โ โค) โ (iโ๐) โ
โ) |
14 | 9, 10, 12, 13 | mp3an12i 1466 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ (iโ๐) โ โ) |
15 | | expne0i 13929 |
. . . . . . . . . . . . . . . . 17
โข ((i
โ โ โง i โ 0 โง ๐ โ โค) โ (iโ๐) โ 0) |
16 | 9, 10, 12, 15 | mp3an12i 1466 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ (iโ๐) โ 0) |
17 | 8, 14, 16 | divcld 11865 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ (๐ถ / (iโ๐)) โ โ) |
18 | 17 | recld 15013 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ (โโ(๐ถ / (iโ๐))) โ โ) |
19 | | 0re 11091 |
. . . . . . . . . . . . . 14
โข 0 โ
โ |
20 | | ifcl 4530 |
. . . . . . . . . . . . . 14
โข
(((โโ(๐ถ /
(iโ๐))) โ โ
โง 0 โ โ) โ if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0) โ โ) |
21 | 18, 19, 20 | sylancl 587 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0) โ โ) |
22 | 21 | rexrd 11139 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0) โ
โ*) |
23 | | max1 13033 |
. . . . . . . . . . . . 13
โข ((0
โ โ โง (โโ(๐ถ / (iโ๐))) โ โ) โ 0 โค if(0 โค
(โโ(๐ถ /
(iโ๐))),
(โโ(๐ถ /
(iโ๐))),
0)) |
24 | 19, 18, 23 | sylancr 588 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ 0 โค if(0 โค
(โโ(๐ถ /
(iโ๐))),
(โโ(๐ถ /
(iโ๐))),
0)) |
25 | | elxrge0 13303 |
. . . . . . . . . . . 12
โข (if(0
โค (โโ(๐ถ /
(iโ๐))),
(โโ(๐ถ /
(iโ๐))), 0) โ
(0[,]+โ) โ (if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0) โ โ* โง 0
โค if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0))) |
26 | 22, 24, 25 | sylanbrc 584 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0) โ
(0[,]+โ)) |
27 | | 0e0iccpnf 13305 |
. . . . . . . . . . . 12
โข 0 โ
(0[,]+โ) |
28 | 27 | a1i 11 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (0...3)) โง ยฌ ๐ฅ โ ๐ต) โ 0 โ
(0[,]+โ)) |
29 | 26, 28 | ifclda 4520 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...3)) โ if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) โ
(0[,]+โ)) |
30 | 7, 29 | eqeltrid 2843 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...3)) โ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) โ
(0[,]+โ)) |
31 | 30 | adantr 482 |
. . . . . . . 8
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ โ) โ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) โ
(0[,]+โ)) |
32 | 31 | fmpttd 7058 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))),
0)):โโถ(0[,]+โ)) |
33 | | ifan 4538 |
. . . . . . . . . 10
โข if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0) = if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ท / (iโ๐))), (โโ(๐ท / (iโ๐))), 0), 0) |
34 | 5 | adantlr 714 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ ๐ท โ โ) |
35 | 34, 14, 16 | divcld 11865 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ (๐ท / (iโ๐)) โ โ) |
36 | 35 | recld 15013 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ (โโ(๐ท / (iโ๐))) โ โ) |
37 | | ifcl 4530 |
. . . . . . . . . . . . . 14
โข
(((โโ(๐ท /
(iโ๐))) โ โ
โง 0 โ โ) โ if(0 โค (โโ(๐ท / (iโ๐))), (โโ(๐ท / (iโ๐))), 0) โ โ) |
38 | 36, 19, 37 | sylancl 587 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ if(0 โค (โโ(๐ท / (iโ๐))), (โโ(๐ท / (iโ๐))), 0) โ โ) |
39 | 38 | rexrd 11139 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ if(0 โค (โโ(๐ท / (iโ๐))), (โโ(๐ท / (iโ๐))), 0) โ
โ*) |
40 | | max1 13033 |
. . . . . . . . . . . . 13
โข ((0
โ โ โง (โโ(๐ท / (iโ๐))) โ โ) โ 0 โค if(0 โค
(โโ(๐ท /
(iโ๐))),
(โโ(๐ท /
(iโ๐))),
0)) |
41 | 19, 36, 40 | sylancr 588 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ 0 โค if(0 โค
(โโ(๐ท /
(iโ๐))),
(โโ(๐ท /
(iโ๐))),
0)) |
42 | | elxrge0 13303 |
. . . . . . . . . . . 12
โข (if(0
โค (โโ(๐ท /
(iโ๐))),
(โโ(๐ท /
(iโ๐))), 0) โ
(0[,]+โ) โ (if(0 โค (โโ(๐ท / (iโ๐))), (โโ(๐ท / (iโ๐))), 0) โ โ* โง 0
โค if(0 โค (โโ(๐ท / (iโ๐))), (โโ(๐ท / (iโ๐))), 0))) |
43 | 39, 41, 42 | sylanbrc 584 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ต) โ if(0 โค (โโ(๐ท / (iโ๐))), (โโ(๐ท / (iโ๐))), 0) โ
(0[,]+โ)) |
44 | 43, 28 | ifclda 4520 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...3)) โ if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ท / (iโ๐))), (โโ(๐ท / (iโ๐))), 0), 0) โ
(0[,]+โ)) |
45 | 33, 44 | eqeltrid 2843 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...3)) โ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0) โ
(0[,]+โ)) |
46 | 45 | adantr 482 |
. . . . . . . 8
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ โ) โ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0) โ
(0[,]+โ)) |
47 | 46 | fmpttd 7058 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))),
0)):โโถ(0[,]+โ)) |
48 | 1 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ ๐ด โ โ) |
49 | 2 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ (vol*โ๐ด) = 0) |
50 | | simpll 766 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (โ โ ๐ด)) โง ๐ฅ โ ๐ต) โ ๐) |
51 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ (โ โ ๐ด)) โง ๐ฅ โ ๐ต) โ ๐ฅ โ ๐ต) |
52 | | eldifn 4086 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ (โ โ ๐ด) โ ยฌ ๐ฅ โ ๐ด) |
53 | 52 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ฅ โ (โ โ ๐ด)) โง ๐ฅ โ ๐ต) โ ยฌ ๐ฅ โ ๐ด) |
54 | 51, 53 | eldifd 3920 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (โ โ ๐ด)) โง ๐ฅ โ ๐ต) โ ๐ฅ โ (๐ต โ ๐ด)) |
55 | 50, 54, 3 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (โ โ ๐ด)) โง ๐ฅ โ ๐ต) โ ๐ถ = ๐ท) |
56 | 55 | fvoveq1d 7372 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (โ โ ๐ด)) โง ๐ฅ โ ๐ต) โ (โโ(๐ถ / (iโ๐))) = (โโ(๐ท / (iโ๐)))) |
57 | 56 | ibllem 25051 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (โ โ ๐ด)) โ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) = if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0)) |
58 | | eldifi 4085 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ (โ โ ๐ด) โ ๐ฅ โ โ) |
59 | 58 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (โ โ ๐ด)) โ ๐ฅ โ โ) |
60 | | fvex 6851 |
. . . . . . . . . . . . . 14
โข
(โโ(๐ถ /
(iโ๐))) โ
V |
61 | | c0ex 11083 |
. . . . . . . . . . . . . 14
โข 0 โ
V |
62 | 60, 61 | ifex 4535 |
. . . . . . . . . . . . 13
โข if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) โ V |
63 | | eqid 2738 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)) = (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)) |
64 | 63 | fvmpt2 6955 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) โ V) โ ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))โ๐ฅ) = if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) |
65 | 59, 62, 64 | sylancl 587 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (โ โ ๐ด)) โ ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))โ๐ฅ) = if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) |
66 | | fvex 6851 |
. . . . . . . . . . . . . 14
โข
(โโ(๐ท /
(iโ๐))) โ
V |
67 | 66, 61 | ifex 4535 |
. . . . . . . . . . . . 13
โข if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0) โ V |
68 | | eqid 2738 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ท /
(iโ๐)))),
(โโ(๐ท /
(iโ๐))), 0)) = (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ท /
(iโ๐)))),
(โโ(๐ท /
(iโ๐))),
0)) |
69 | 68 | fvmpt2 6955 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0) โ V) โ ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))โ๐ฅ) = if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0)) |
70 | 59, 67, 69 | sylancl 587 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (โ โ ๐ด)) โ ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))โ๐ฅ) = if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0)) |
71 | 57, 65, 70 | 3eqtr4d 2788 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (โ โ ๐ด)) โ ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))โ๐ฅ) = ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))โ๐ฅ)) |
72 | 71 | ralrimiva 3142 |
. . . . . . . . . 10
โข (๐ โ โ๐ฅ โ (โ โ ๐ด)((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))โ๐ฅ) = ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))โ๐ฅ)) |
73 | | nfv 1918 |
. . . . . . . . . . 11
โข
โฒ๐ฆ((๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0))โ๐ฅ) = ((๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ท /
(iโ๐)))),
(โโ(๐ท /
(iโ๐))),
0))โ๐ฅ) |
74 | | nffvmpt1 6849 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))โ๐ฆ) |
75 | | nffvmpt1 6849 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))โ๐ฆ) |
76 | 74, 75 | nfeq 2919 |
. . . . . . . . . . 11
โข
โฒ๐ฅ((๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0))โ๐ฆ) = ((๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ท /
(iโ๐)))),
(โโ(๐ท /
(iโ๐))),
0))โ๐ฆ) |
77 | | fveq2 6838 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ฆ โ ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))โ๐ฅ) = ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))โ๐ฆ)) |
78 | | fveq2 6838 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ฆ โ ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))โ๐ฅ) = ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))โ๐ฆ)) |
79 | 77, 78 | eqeq12d 2754 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ฆ โ (((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))โ๐ฅ) = ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))โ๐ฅ) โ ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))โ๐ฆ) = ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))โ๐ฆ))) |
80 | 73, 76, 79 | cbvralw 3288 |
. . . . . . . . . 10
โข
(โ๐ฅ โ
(โ โ ๐ด)((๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0))โ๐ฅ) = ((๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ท /
(iโ๐)))),
(โโ(๐ท /
(iโ๐))),
0))โ๐ฅ) โ
โ๐ฆ โ (โ
โ ๐ด)((๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0))โ๐ฆ) = ((๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ท /
(iโ๐)))),
(โโ(๐ท /
(iโ๐))),
0))โ๐ฆ)) |
81 | 72, 80 | sylib 217 |
. . . . . . . . 9
โข (๐ โ โ๐ฆ โ (โ โ ๐ด)((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))โ๐ฆ) = ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))โ๐ฆ)) |
82 | 81 | r19.21bi 3233 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ (โ โ ๐ด)) โ ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))โ๐ฆ) = ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))โ๐ฆ)) |
83 | 82 | adantlr 714 |
. . . . . . 7
โข (((๐ โง ๐ โ (0...3)) โง ๐ฆ โ (โ โ ๐ด)) โ ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))โ๐ฆ) = ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))โ๐ฆ)) |
84 | 32, 47, 48, 49, 83 | itg2eqa 25032 |
. . . . . 6
โข ((๐ โง ๐ โ (0...3)) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) = (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ท /
(iโ๐)))),
(โโ(๐ท /
(iโ๐))),
0)))) |
85 | 84 | eleq1d 2823 |
. . . . 5
โข ((๐ โง ๐ โ (0...3)) โ
((โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) โ โ โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))) โ โ)) |
86 | 85 | ralbidva 3171 |
. . . 4
โข (๐ โ (โ๐ โ
(0...3)(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) โ โ โ โ๐ โ
(0...3)(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))) โ โ)) |
87 | 6, 86 | anbi12d 632 |
. . 3
โข (๐ โ (((๐ฅ โ ๐ต โฆ ๐ถ) โ MblFn โง โ๐ โ
(0...3)(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) โ โ) โ ((๐ฅ โ ๐ต โฆ ๐ท) โ MblFn โง โ๐ โ
(0...3)(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))) โ โ))) |
88 | | eqidd 2739 |
. . . 4
โข (๐ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) |
89 | | eqidd 2739 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ต) โ (โโ(๐ถ / (iโ๐))) = (โโ(๐ถ / (iโ๐)))) |
90 | 88, 89, 4 | isibl2 25053 |
. . 3
โข (๐ โ ((๐ฅ โ ๐ต โฆ ๐ถ) โ ๐ฟ1 โ
((๐ฅ โ ๐ต โฆ ๐ถ) โ MblFn โง โ๐ โ
(0...3)(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) โ โ))) |
91 | | eqidd 2739 |
. . . 4
โข (๐ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))) |
92 | | eqidd 2739 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ต) โ (โโ(๐ท / (iโ๐))) = (โโ(๐ท / (iโ๐)))) |
93 | 91, 92, 5 | isibl2 25053 |
. . 3
โข (๐ โ ((๐ฅ โ ๐ต โฆ ๐ท) โ ๐ฟ1 โ
((๐ฅ โ ๐ต โฆ ๐ท) โ MblFn โง โ๐ โ
(0...3)(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))) โ โ))) |
94 | 87, 90, 93 | 3bitr4d 311 |
. 2
โข (๐ โ ((๐ฅ โ ๐ต โฆ ๐ถ) โ ๐ฟ1 โ (๐ฅ โ ๐ต โฆ ๐ท) โ
๐ฟ1)) |
95 | 84 | oveq2d 7366 |
. . . 4
โข ((๐ โง ๐ โ (0...3)) โ ((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))) = ((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ท /
(iโ๐)))),
(โโ(๐ท /
(iโ๐))),
0))))) |
96 | 95 | sumeq2dv 15523 |
. . 3
โข (๐ โ ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)))) =
ฮฃ๐ โ
(0...3)((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ท / (iโ๐)))), (โโ(๐ท / (iโ๐))), 0))))) |
97 | | eqid 2738 |
. . . 4
โข
(โโ(๐ถ /
(iโ๐))) =
(โโ(๐ถ /
(iโ๐))) |
98 | 97 | dfitg 25056 |
. . 3
โข
โซ๐ต๐ถ d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))) |
99 | | eqid 2738 |
. . . 4
โข
(โโ(๐ท /
(iโ๐))) =
(โโ(๐ท /
(iโ๐))) |
100 | 99 | dfitg 25056 |
. . 3
โข
โซ๐ต๐ท d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ท /
(iโ๐)))),
(โโ(๐ท /
(iโ๐))),
0)))) |
101 | 96, 98, 100 | 3eqtr4g 2803 |
. 2
โข (๐ โ โซ๐ต๐ถ d๐ฅ = โซ๐ต๐ท d๐ฅ) |
102 | 94, 101 | jca 513 |
1
โข (๐ โ (((๐ฅ โ ๐ต โฆ ๐ถ) โ ๐ฟ1 โ (๐ฅ โ ๐ต โฆ ๐ท) โ ๐ฟ1) โง
โซ๐ต๐ถ d๐ฅ = โซ๐ต๐ท d๐ฅ)) |