Step | Hyp | Ref
| Expression |
1 | | itgmulc2.1 |
. . 3
โข (๐ โ ๐ถ โ โ) |
2 | | itgmulc2.2 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) |
3 | | itgmulc2.3 |
. . . 4
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ
๐ฟ1) |
4 | | iblmbf 25054 |
. . . 4
โข ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
5 | 3, 4 | syl 17 |
. . 3
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
6 | 1, 2, 5 | mbfmulc2 24949 |
. 2
โข (๐ โ (๐ฅ โ ๐ด โฆ (๐ถ ยท ๐ต)) โ MblFn) |
7 | | ifan 4538 |
. . . . . 6
โข if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) = if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) |
8 | 1 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) |
9 | 5, 2 | mbfmptcl 24922 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
10 | 8, 9 | mulcld 11109 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐ด) โ (๐ถ ยท ๐ต) โ โ) |
11 | 10 | adantlr 714 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (๐ถ ยท ๐ต) โ โ) |
12 | | ax-icn 11044 |
. . . . . . . . . . . . . 14
โข i โ
โ |
13 | | ine0 11524 |
. . . . . . . . . . . . . 14
โข i โ
0 |
14 | | elfzelz 13370 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0...3) โ ๐ โ
โค) |
15 | 14 | ad2antlr 726 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ ๐ โ โค) |
16 | | expclz 13921 |
. . . . . . . . . . . . . 14
โข ((i
โ โ โง i โ 0 โง ๐ โ โค) โ (iโ๐) โ
โ) |
17 | 12, 13, 15, 16 | mp3an12i 1466 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (iโ๐) โ โ) |
18 | | expne0i 13929 |
. . . . . . . . . . . . . 14
โข ((i
โ โ โง i โ 0 โง ๐ โ โค) โ (iโ๐) โ 0) |
19 | 12, 13, 15, 18 | mp3an12i 1466 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (iโ๐) โ 0) |
20 | 11, 17, 19 | divcld 11865 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ ((๐ถ ยท ๐ต) / (iโ๐)) โ โ) |
21 | 20 | recld 15013 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (โโ((๐ถ ยท ๐ต) / (iโ๐))) โ โ) |
22 | | 0re 11091 |
. . . . . . . . . . 11
โข 0 โ
โ |
23 | | ifcl 4530 |
. . . . . . . . . . 11
โข
(((โโ((๐ถ
ยท ๐ต) / (iโ๐))) โ โ โง 0
โ โ) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ โ) |
24 | 21, 22, 23 | sylancl 587 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ โ) |
25 | 24 | rexrd 11139 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ
โ*) |
26 | | max1 13033 |
. . . . . . . . . 10
โข ((0
โ โ โง (โโ((๐ถ ยท ๐ต) / (iโ๐))) โ โ) โ 0 โค if(0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) |
27 | 22, 21, 26 | sylancr 588 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ 0 โค if(0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) |
28 | | elxrge0 13303 |
. . . . . . . . 9
โข (if(0
โค (โโ((๐ถ
ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ (0[,]+โ) โ (if(0
โค (โโ((๐ถ
ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ โ* โง 0
โค if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) |
29 | 25, 27, 28 | sylanbrc 584 |
. . . . . . . 8
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ
(0[,]+โ)) |
30 | | 0e0iccpnf 13305 |
. . . . . . . . 9
โข 0 โ
(0[,]+โ) |
31 | 30 | a1i 11 |
. . . . . . . 8
โข (((๐ โง ๐ โ (0...3)) โง ยฌ ๐ฅ โ ๐ด) โ 0 โ
(0[,]+โ)) |
32 | 29, 31 | ifclda 4520 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) โ
(0[,]+โ)) |
33 | 32 | adantr 482 |
. . . . . 6
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) โ
(0[,]+โ)) |
34 | 7, 33 | eqeltrid 2843 |
. . . . 5
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ โ) โ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ
(0[,]+โ)) |
35 | 34 | fmpttd 7058 |
. . . 4
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))),
0)):โโถ(0[,]+โ)) |
36 | | reex 11076 |
. . . . . . . . . . 11
โข โ
โ V |
37 | 36 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ โ
V) |
38 | 1 | abscld 15256 |
. . . . . . . . . . 11
โข (๐ โ (absโ๐ถ) โ
โ) |
39 | 38 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ โ) โ (absโ๐ถ) โ
โ) |
40 | 9 | abscld 15256 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ๐ต) โ โ) |
41 | 9 | absge0d 15264 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค (absโ๐ต)) |
42 | | elrege0 13300 |
. . . . . . . . . . . . 13
โข
((absโ๐ต)
โ (0[,)+โ) โ ((absโ๐ต) โ โ โง 0 โค
(absโ๐ต))) |
43 | 40, 41, 42 | sylanbrc 584 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ๐ต) โ (0[,)+โ)) |
44 | | 0e0icopnf 13304 |
. . . . . . . . . . . . 13
โข 0 โ
(0[,)+โ) |
45 | 44 | a1i 11 |
. . . . . . . . . . . 12
โข ((๐ โง ยฌ ๐ฅ โ ๐ด) โ 0 โ
(0[,)+โ)) |
46 | 43, 45 | ifclda 4520 |
. . . . . . . . . . 11
โข (๐ โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) โ
(0[,)+โ)) |
47 | 46 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) โ
(0[,)+โ)) |
48 | | fconstmpt 5691 |
. . . . . . . . . . 11
โข (โ
ร {(absโ๐ถ)}) =
(๐ฅ โ โ โฆ
(absโ๐ถ)) |
49 | 48 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ (โ ร
{(absโ๐ถ)}) = (๐ฅ โ โ โฆ
(absโ๐ถ))) |
50 | | eqidd 2739 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0))) |
51 | 37, 39, 47, 49, 50 | offval2 7628 |
. . . . . . . . 9
โข (๐ โ ((โ ร
{(absโ๐ถ)})
โf ยท (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0))) = (๐ฅ โ โ โฆ ((absโ๐ถ) ยท if(๐ฅ โ ๐ด, (absโ๐ต), 0)))) |
52 | | ovif2 7448 |
. . . . . . . . . . 11
โข
((absโ๐ถ)
ยท if(๐ฅ โ ๐ด, (absโ๐ต), 0)) = if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท (absโ๐ต)), ((absโ๐ถ) ยท 0)) |
53 | 8, 9 | absmuld 15274 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(๐ถ ยท ๐ต)) = ((absโ๐ถ) ยท (absโ๐ต))) |
54 | 53 | ifeq1da 4516 |
. . . . . . . . . . . 12
โข (๐ โ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), ((absโ๐ถ) ยท 0)) = if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท (absโ๐ต)), ((absโ๐ถ) ยท 0))) |
55 | 38 | recnd 11117 |
. . . . . . . . . . . . . 14
โข (๐ โ (absโ๐ถ) โ
โ) |
56 | 55 | mul01d 11288 |
. . . . . . . . . . . . 13
โข (๐ โ ((absโ๐ถ) ยท 0) =
0) |
57 | 56 | ifeq2d 4505 |
. . . . . . . . . . . 12
โข (๐ โ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), ((absโ๐ถ) ยท 0)) = if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)) |
58 | 54, 57 | eqtr3d 2780 |
. . . . . . . . . . 11
โข (๐ โ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท (absโ๐ต)), ((absโ๐ถ) ยท 0)) = if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)) |
59 | 52, 58 | eqtrid 2790 |
. . . . . . . . . 10
โข (๐ โ ((absโ๐ถ) ยท if(๐ฅ โ ๐ด, (absโ๐ต), 0)) = if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)) |
60 | 59 | mpteq2dv 5206 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ โ โฆ ((absโ๐ถ) ยท if(๐ฅ โ ๐ด, (absโ๐ต), 0))) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0))) |
61 | 51, 60 | eqtrd 2778 |
. . . . . . . 8
โข (๐ โ ((โ ร
{(absโ๐ถ)})
โf ยท (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0))) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0))) |
62 | 61 | fveq2d 6842 |
. . . . . . 7
โข (๐ โ
(โซ2โ((โ ร {(absโ๐ถ)}) โf ยท (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0)))) = (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)))) |
63 | 47 | fmpttd 7058 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต),
0)):โโถ(0[,)+โ)) |
64 | 2, 3 | iblabs 25115 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ ๐ด โฆ (absโ๐ต)) โ
๐ฟ1) |
65 | 40, 41 | iblpos 25079 |
. . . . . . . . . 10
โข (๐ โ ((๐ฅ โ ๐ด โฆ (absโ๐ต)) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (absโ๐ต)) โ MblFn โง
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ๐ต), 0))) โ
โ))) |
66 | 64, 65 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ ((๐ฅ โ ๐ด โฆ (absโ๐ต)) โ MblFn โง
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ๐ต), 0))) โ
โ)) |
67 | 66 | simprd 497 |
. . . . . . . 8
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ๐ต), 0))) โ
โ) |
68 | | abscl 15098 |
. . . . . . . . . 10
โข (๐ถ โ โ โ
(absโ๐ถ) โ
โ) |
69 | | absge0 15107 |
. . . . . . . . . 10
โข (๐ถ โ โ โ 0 โค
(absโ๐ถ)) |
70 | | elrege0 13300 |
. . . . . . . . . 10
โข
((absโ๐ถ)
โ (0[,)+โ) โ ((absโ๐ถ) โ โ โง 0 โค
(absโ๐ถ))) |
71 | 68, 69, 70 | sylanbrc 584 |
. . . . . . . . 9
โข (๐ถ โ โ โ
(absโ๐ถ) โ
(0[,)+โ)) |
72 | 1, 71 | syl 17 |
. . . . . . . 8
โข (๐ โ (absโ๐ถ) โ
(0[,)+โ)) |
73 | 63, 67, 72 | itg2mulc 25034 |
. . . . . . 7
โข (๐ โ
(โซ2โ((โ ร {(absโ๐ถ)}) โf ยท (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0)))) = ((absโ๐ถ) ยท (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0))))) |
74 | 62, 73 | eqtr3d 2780 |
. . . . . 6
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0))) = ((absโ๐ถ) ยท (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0))))) |
75 | 38, 67 | remulcld 11119 |
. . . . . 6
โข (๐ โ ((absโ๐ถ) ยท
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ๐ต), 0)))) โ
โ) |
76 | 74, 75 | eqeltrd 2839 |
. . . . 5
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0))) โ โ) |
77 | 76 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ (0...3)) โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0))) โ โ) |
78 | 10 | abscld 15256 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(๐ถ ยท ๐ต)) โ โ) |
79 | 78 | rexrd 11139 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(๐ถ ยท ๐ต)) โ
โ*) |
80 | 10 | absge0d 15264 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค (absโ(๐ถ ยท ๐ต))) |
81 | | elxrge0 13303 |
. . . . . . . . . 10
โข
((absโ(๐ถ
ยท ๐ต)) โ
(0[,]+โ) โ ((absโ(๐ถ ยท ๐ต)) โ โ* โง 0 โค
(absโ(๐ถ ยท
๐ต)))) |
82 | 79, 80, 81 | sylanbrc 584 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(๐ถ ยท ๐ต)) โ (0[,]+โ)) |
83 | 30 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ยฌ ๐ฅ โ ๐ด) โ 0 โ
(0[,]+โ)) |
84 | 82, 83 | ifclda 4520 |
. . . . . . . 8
โข (๐ โ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0) โ
(0[,]+โ)) |
85 | 84 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0) โ
(0[,]+โ)) |
86 | 85 | fmpttd 7058 |
. . . . . 6
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)),
0)):โโถ(0[,]+โ)) |
87 | 86 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)),
0)):โโถ(0[,]+โ)) |
88 | 20 | releabsd 15271 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (โโ((๐ถ ยท ๐ต) / (iโ๐))) โค (absโ((๐ถ ยท ๐ต) / (iโ๐)))) |
89 | 11, 17, 19 | absdivd 15275 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (absโ((๐ถ ยท ๐ต) / (iโ๐))) = ((absโ(๐ถ ยท ๐ต)) / (absโ(iโ๐)))) |
90 | | elfznn0 13463 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (0...3) โ ๐ โ
โ0) |
91 | 90 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ ๐ โ โ0) |
92 | | absexp 15124 |
. . . . . . . . . . . . . . . . 17
โข ((i
โ โ โง ๐
โ โ0) โ (absโ(iโ๐)) = ((absโi)โ๐)) |
93 | 12, 91, 92 | sylancr 588 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (absโ(iโ๐)) = ((absโi)โ๐)) |
94 | | absi 15106 |
. . . . . . . . . . . . . . . . . 18
โข
(absโi) = 1 |
95 | 94 | oveq1i 7360 |
. . . . . . . . . . . . . . . . 17
โข
((absโi)โ๐) = (1โ๐) |
96 | | 1exp 13926 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โค โ
(1โ๐) =
1) |
97 | 15, 96 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (1โ๐) = 1) |
98 | 95, 97 | eqtrid 2790 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ ((absโi)โ๐) = 1) |
99 | 93, 98 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (absโ(iโ๐)) = 1) |
100 | 99 | oveq2d 7366 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ ((absโ(๐ถ ยท ๐ต)) / (absโ(iโ๐))) = ((absโ(๐ถ ยท ๐ต)) / 1)) |
101 | 78 | recnd 11117 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(๐ถ ยท ๐ต)) โ โ) |
102 | 101 | adantlr 714 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (absโ(๐ถ ยท ๐ต)) โ โ) |
103 | 102 | div1d 11857 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ ((absโ(๐ถ ยท ๐ต)) / 1) = (absโ(๐ถ ยท ๐ต))) |
104 | 89, 100, 103 | 3eqtrd 2782 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (absโ((๐ถ ยท ๐ต) / (iโ๐))) = (absโ(๐ถ ยท ๐ต))) |
105 | 88, 104 | breqtrd 5130 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (โโ((๐ถ ยท ๐ต) / (iโ๐))) โค (absโ(๐ถ ยท ๐ต))) |
106 | 80 | adantlr 714 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ 0 โค (absโ(๐ถ ยท ๐ต))) |
107 | | breq1 5107 |
. . . . . . . . . . . . 13
โข
((โโ((๐ถ
ยท ๐ต) / (iโ๐))) = if(0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ ((โโ((๐ถ ยท ๐ต) / (iโ๐))) โค (absโ(๐ถ ยท ๐ต)) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค (absโ(๐ถ ยท ๐ต)))) |
108 | | breq1 5107 |
. . . . . . . . . . . . 13
โข (0 = if(0
โค (โโ((๐ถ
ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ (0 โค (absโ(๐ถ ยท ๐ต)) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค (absโ(๐ถ ยท ๐ต)))) |
109 | 107, 108 | ifboth 4524 |
. . . . . . . . . . . 12
โข
(((โโ((๐ถ
ยท ๐ต) / (iโ๐))) โค (absโ(๐ถ ยท ๐ต)) โง 0 โค (absโ(๐ถ ยท ๐ต))) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค (absโ(๐ถ ยท ๐ต))) |
110 | 105, 106,
109 | syl2anc 585 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค (absโ(๐ถ ยท ๐ต))) |
111 | | iftrue 4491 |
. . . . . . . . . . . 12
โข (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) = if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) |
112 | 111 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) = if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) |
113 | | iftrue 4491 |
. . . . . . . . . . . 12
โข (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0) = (absโ(๐ถ ยท ๐ต))) |
114 | 113 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0) = (absโ(๐ถ ยท ๐ต))) |
115 | 110, 112,
114 | 3brtr4d 5136 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) โค if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)) |
116 | 115 | ex 414 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) โค if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0))) |
117 | | 0le0 12188 |
. . . . . . . . . . 11
โข 0 โค
0 |
118 | 117 | a1i 11 |
. . . . . . . . . 10
โข (ยฌ
๐ฅ โ ๐ด โ 0 โค 0) |
119 | | iffalse 4494 |
. . . . . . . . . 10
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) = 0) |
120 | | iffalse 4494 |
. . . . . . . . . 10
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0) = 0) |
121 | 118, 119,
120 | 3brtr4d 5136 |
. . . . . . . . 9
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) โค if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)) |
122 | 116, 121 | pm2.61d1 180 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...3)) โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) โค if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)) |
123 | 7, 122 | eqbrtrid 5139 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)) |
124 | 123 | ralrimivw 3146 |
. . . . . 6
โข ((๐ โง ๐ โ (0...3)) โ โ๐ฅ โ โ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)) |
125 | 36 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ โ โ
V) |
126 | 85 | adantlr 714 |
. . . . . . 7
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0) โ
(0[,]+โ)) |
127 | | eqidd 2739 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) |
128 | | eqidd 2739 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0))) |
129 | 125, 34, 126, 127, 128 | ofrfval2 7629 |
. . . . . 6
โข ((๐ โง ๐ โ (0...3)) โ ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)) โ โ๐ฅ โ โ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0))) |
130 | 124, 129 | mpbird 257 |
. . . . 5
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0))) |
131 | | itg2le 25026 |
. . . . 5
โข (((๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)):โโถ(0[,]+โ) โง
(๐ฅ โ โ โฆ
if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)):โโถ(0[,]+โ) โง
(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โค
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)))) |
132 | 35, 87, 130, 131 | syl3anc 1372 |
. . . 4
โข ((๐ โง ๐ โ (0...3)) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โค
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)))) |
133 | | itg2lecl 25025 |
. . . 4
โข (((๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)):โโถ(0[,]+โ) โง
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0))) โ โ โง
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โค
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ(๐ถ ยท ๐ต)), 0)))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โ โ) |
134 | 35, 77, 132, 133 | syl3anc 1372 |
. . 3
โข ((๐ โง ๐ โ (0...3)) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โ โ) |
135 | 134 | ralrimiva 3142 |
. 2
โข (๐ โ โ๐ โ
(0...3)(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โ โ) |
136 | | eqidd 2739 |
. . 3
โข (๐ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) |
137 | | eqidd 2739 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ((๐ถ ยท ๐ต) / (iโ๐))) = (โโ((๐ถ ยท ๐ต) / (iโ๐)))) |
138 | 136, 137,
10 | isibl2 25053 |
. 2
โข (๐ โ ((๐ฅ โ ๐ด โฆ (๐ถ ยท ๐ต)) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (๐ถ ยท ๐ต)) โ MblFn โง โ๐ โ
(0...3)(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โ โ))) |
139 | 6, 135, 138 | mpbir2and 712 |
1
โข (๐ โ (๐ฅ โ ๐ด โฆ (๐ถ ยท ๐ต)) โ
๐ฟ1) |