Step | Hyp | Ref
| Expression |
1 | | itgmulc2nc.m |
. 2
โข (๐ โ (๐ฅ โ ๐ด โฆ (๐ถ ยท ๐ต)) โ MblFn) |
2 | | ifan 4538 |
. . . . . 6
โข if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) = if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) |
3 | | itgmulc2nc.1 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ถ โ โ) |
4 | 3 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) |
5 | | itgmulc2nc.3 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ
๐ฟ1) |
6 | | iblmbf 25054 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
8 | | itgmulc2nc.2 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) |
9 | 7, 8 | mbfmptcl 24922 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
10 | 4, 9 | mulcld 11109 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐ด) โ (๐ถ ยท ๐ต) โ โ) |
11 | 10 | adantlr 714 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (๐ถ ยท ๐ต) โ โ) |
12 | | elfzelz 13370 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0...3) โ ๐ โ
โค) |
13 | 12 | ad2antlr 726 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ ๐ โ โค) |
14 | | ax-icn 11044 |
. . . . . . . . . . . . . . 15
โข i โ
โ |
15 | | ine0 11524 |
. . . . . . . . . . . . . . 15
โข i โ
0 |
16 | | expclz 13921 |
. . . . . . . . . . . . . . 15
โข ((i
โ โ โง i โ 0 โง ๐ โ โค) โ (iโ๐) โ
โ) |
17 | 14, 15, 16 | mp3an12 1452 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ
(iโ๐) โ
โ) |
18 | 13, 17 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (iโ๐) โ โ) |
19 | | expne0i 13929 |
. . . . . . . . . . . . . . 15
โข ((i
โ โ โง i โ 0 โง ๐ โ โค) โ (iโ๐) โ 0) |
20 | 14, 15, 19 | mp3an12 1452 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ
(iโ๐) โ
0) |
21 | 13, 20 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (iโ๐) โ 0) |
22 | 11, 18, 21 | divcld 11865 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ ((๐ถ ยท ๐ต) / (iโ๐)) โ โ) |
23 | 22 | recld 15013 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (โโ((๐ถ ยท ๐ต) / (iโ๐))) โ โ) |
24 | | 0re 11091 |
. . . . . . . . . . 11
โข 0 โ
โ |
25 | | ifcl 4530 |
. . . . . . . . . . 11
โข
(((โโ((๐ถ
ยท ๐ต) / (iโ๐))) โ โ โง 0
โ โ) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ โ) |
26 | 23, 24, 25 | sylancl 587 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ โ) |
27 | 26 | rexrd 11139 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ
โ*) |
28 | | max1 13033 |
. . . . . . . . . 10
โข ((0
โ โ โง (โโ((๐ถ ยท ๐ต) / (iโ๐))) โ โ) โ 0 โค if(0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) |
29 | 24, 23, 28 | sylancr 588 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ 0 โค if(0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) |
30 | | elxrge0 13303 |
. . . . . . . . 9
โข (if(0
โค (โโ((๐ถ
ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ (0[,]+โ) โ (if(0
โค (โโ((๐ถ
ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ โ* โง 0
โค if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) |
31 | 27, 29, 30 | sylanbrc 584 |
. . . . . . . 8
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ
(0[,]+โ)) |
32 | | 0e0iccpnf 13305 |
. . . . . . . . 9
โข 0 โ
(0[,]+โ) |
33 | 32 | a1i 11 |
. . . . . . . 8
โข (((๐ โง ๐ โ (0...3)) โง ยฌ ๐ฅ โ ๐ด) โ 0 โ
(0[,]+โ)) |
34 | 31, 33 | ifclda 4520 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) โ
(0[,]+โ)) |
35 | 34 | adantr 482 |
. . . . . 6
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) โ
(0[,]+โ)) |
36 | 2, 35 | eqeltrid 2843 |
. . . . 5
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ โ) โ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ
(0[,]+โ)) |
37 | 36 | fmpttd 7058 |
. . . 4
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))),
0)):โโถ(0[,]+โ)) |
38 | 9 | recld 15013 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
39 | 38 | recnd 11117 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
40 | 39 | abscld 15256 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(โโ๐ต)) โ
โ) |
41 | 9 | imcld 15014 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
42 | 41 | recnd 11117 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
43 | 42 | abscld 15256 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(โโ๐ต)) โ
โ) |
44 | 40, 43 | readdcld 11118 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))) โ โ) |
45 | 39 | absge0d 15264 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค
(absโ(โโ๐ต))) |
46 | 42 | absge0d 15264 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค
(absโ(โโ๐ต))) |
47 | 40, 43, 45, 46 | addge0d 11665 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค
((absโ(โโ๐ต)) + (absโ(โโ๐ต)))) |
48 | | elrege0 13300 |
. . . . . . . . . . . 12
โข
(((absโ(โโ๐ต)) + (absโ(โโ๐ต))) โ (0[,)+โ) โ
(((absโ(โโ๐ต)) + (absโ(โโ๐ต))) โ โ โง 0 โค
((absโ(โโ๐ต)) + (absโ(โโ๐ต))))) |
49 | 44, 47, 48 | sylanbrc 584 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))) โ (0[,)+โ)) |
50 | | 0e0icopnf 13304 |
. . . . . . . . . . . 12
โข 0 โ
(0[,)+โ) |
51 | 50 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โง ยฌ ๐ฅ โ ๐ด) โ 0 โ
(0[,)+โ)) |
52 | 49, 51 | ifclda 4520 |
. . . . . . . . . 10
โข (๐ โ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0) โ
(0[,)+โ)) |
53 | 52 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0) โ
(0[,)+โ)) |
54 | 53 | fmpttd 7058 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))),
0)):โโถ(0[,)+โ)) |
55 | | reex 11076 |
. . . . . . . . . . . . . 14
โข โ
โ V |
56 | 55 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
V) |
57 | | elrege0 13300 |
. . . . . . . . . . . . . . . 16
โข
((absโ(โโ๐ต)) โ (0[,)+โ) โ
((absโ(โโ๐ต)) โ โ โง 0 โค
(absโ(โโ๐ต)))) |
58 | 40, 45, 57 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(โโ๐ต)) โ
(0[,)+โ)) |
59 | 58, 51 | ifclda 4520 |
. . . . . . . . . . . . . 14
โข (๐ โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) โ
(0[,)+โ)) |
60 | 59 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) โ
(0[,)+โ)) |
61 | | elrege0 13300 |
. . . . . . . . . . . . . . . 16
โข
((absโ(โโ๐ต)) โ (0[,)+โ) โ
((absโ(โโ๐ต)) โ โ โง 0 โค
(absโ(โโ๐ต)))) |
62 | 43, 46, 61 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(โโ๐ต)) โ
(0[,)+โ)) |
63 | 62, 51 | ifclda 4520 |
. . . . . . . . . . . . . 14
โข (๐ โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) โ
(0[,)+โ)) |
64 | 63 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) โ
(0[,)+โ)) |
65 | | eqidd 2739 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) |
66 | | eqidd 2739 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) |
67 | 56, 60, 64, 65, 66 | offval2 7628 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โf + (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) = (๐ฅ โ โ โฆ (if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)))) |
68 | | iftrue 4491 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) = (absโ(โโ๐ต))) |
69 | | iftrue 4491 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) =
(absโ(โโ๐ต))) |
70 | 68, 69 | oveq12d 7368 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ ๐ด โ (if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) =
((absโ(โโ๐ต)) + (absโ(โโ๐ต)))) |
71 | | iftrue 4491 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0) = ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))) |
72 | 70, 71 | eqtr4d 2781 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ ๐ด โ (if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) |
73 | | 00id 11264 |
. . . . . . . . . . . . . . 15
โข (0 + 0) =
0 |
74 | | iffalse 4494 |
. . . . . . . . . . . . . . . 16
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) = 0) |
75 | | iffalse 4494 |
. . . . . . . . . . . . . . . 16
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) = 0) |
76 | 74, 75 | oveq12d 7368 |
. . . . . . . . . . . . . . 15
โข (ยฌ
๐ฅ โ ๐ด โ (if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = (0 +
0)) |
77 | | iffalse 4494 |
. . . . . . . . . . . . . . 15
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0) = 0) |
78 | 73, 76, 77 | 3eqtr4a 2804 |
. . . . . . . . . . . . . 14
โข (ยฌ
๐ฅ โ ๐ด โ (if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) |
79 | 72, 78 | pm2.61i 182 |
. . . . . . . . . . . . 13
โข (if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0) |
80 | 79 | mpteq2i 5209 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โฆ
(if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) |
81 | 67, 80 | eqtr2di 2795 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) = ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โf + (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)))) |
82 | 81 | fveq2d 6842 |
. . . . . . . . . 10
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
((absโ(โโ๐ต)) + (absโ(โโ๐ต))), 0))) =
(โซ2โ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โf + (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))))) |
83 | | eqid 2738 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) |
84 | 9 | iblcn 25085 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1
โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1))) |
85 | 5, 84 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1)) |
86 | 85 | simpld 496 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
87 | 8, 5, 83, 86, 38 | iblabsnclem 36027 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โ MblFn โง
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
(absโ(โโ๐ต)), 0))) โ โ)) |
88 | 87 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โ MblFn) |
89 | 60 | fmpttd 7058 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)),
0)):โโถ(0[,)+โ)) |
90 | 87 | simprd 497 |
. . . . . . . . . . 11
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
(absโ(โโ๐ต)), 0))) โ โ) |
91 | 64 | fmpttd 7058 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)),
0)):โโถ(0[,)+โ)) |
92 | | eqid 2738 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) |
93 | 85 | simprd 497 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
94 | 8, 5, 92, 93, 41 | iblabsnclem 36027 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โ MblFn โง
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
(absโ(โโ๐ต)), 0))) โ โ)) |
95 | 94 | simprd 497 |
. . . . . . . . . . 11
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
(absโ(โโ๐ต)), 0))) โ โ) |
96 | 88, 89, 90, 91, 95 | itg2addnc 36018 |
. . . . . . . . . 10
โข (๐ โ
(โซ2โ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โf + (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)))) =
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) + (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))))) |
97 | 82, 96 | eqtrd 2778 |
. . . . . . . . 9
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
((absโ(โโ๐ต)) + (absโ(โโ๐ต))), 0))) =
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) + (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))))) |
98 | 90, 95 | readdcld 11118 |
. . . . . . . . 9
โข (๐ โ
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) + (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)))) โ
โ) |
99 | 97, 98 | eqeltrd 2839 |
. . . . . . . 8
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
((absโ(โโ๐ต)) + (absโ(โโ๐ต))), 0))) โ
โ) |
100 | 3 | abscld 15256 |
. . . . . . . . 9
โข (๐ โ (absโ๐ถ) โ
โ) |
101 | 3 | absge0d 15264 |
. . . . . . . . 9
โข (๐ โ 0 โค (absโ๐ถ)) |
102 | | elrege0 13300 |
. . . . . . . . 9
โข
((absโ๐ถ)
โ (0[,)+โ) โ ((absโ๐ถ) โ โ โง 0 โค
(absโ๐ถ))) |
103 | 100, 101,
102 | sylanbrc 584 |
. . . . . . . 8
โข (๐ โ (absโ๐ถ) โ
(0[,)+โ)) |
104 | 54, 99, 103 | itg2mulc 25034 |
. . . . . . 7
โข (๐ โ
(โซ2โ((โ ร {(absโ๐ถ)}) โf ยท (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)))) = ((absโ๐ถ) ยท (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0))))) |
105 | 100 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ โ) โ (absโ๐ถ) โ
โ) |
106 | | fconstmpt 5691 |
. . . . . . . . . . 11
โข (โ
ร {(absโ๐ถ)}) =
(๐ฅ โ โ โฆ
(absโ๐ถ)) |
107 | 106 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ (โ ร
{(absโ๐ถ)}) = (๐ฅ โ โ โฆ
(absโ๐ถ))) |
108 | | eqidd 2739 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0))) |
109 | 56, 105, 53, 107, 108 | offval2 7628 |
. . . . . . . . 9
โข (๐ โ ((โ ร
{(absโ๐ถ)})
โf ยท (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0))) = (๐ฅ โ โ โฆ ((absโ๐ถ) ยท if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)))) |
110 | 71 | oveq2d 7366 |
. . . . . . . . . . . . 13
โข (๐ฅ โ ๐ด โ ((absโ๐ถ) ยท if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) = ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))))) |
111 | | iftrue 4491 |
. . . . . . . . . . . . 13
โข (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0) = ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))))) |
112 | 110, 111 | eqtr4d 2781 |
. . . . . . . . . . . 12
โข (๐ฅ โ ๐ด โ ((absโ๐ถ) ยท if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) = if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0)) |
113 | 112 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโ๐ถ) ยท if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) = if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0)) |
114 | 100 | recnd 11117 |
. . . . . . . . . . . . . 14
โข (๐ โ (absโ๐ถ) โ
โ) |
115 | 114 | mul01d 11288 |
. . . . . . . . . . . . 13
โข (๐ โ ((absโ๐ถ) ยท 0) =
0) |
116 | 115 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ยฌ ๐ฅ โ ๐ด) โ ((absโ๐ถ) ยท 0) = 0) |
117 | 77 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ยฌ ๐ฅ โ ๐ด) โ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0) = 0) |
118 | 117 | oveq2d 7366 |
. . . . . . . . . . . 12
โข ((๐ โง ยฌ ๐ฅ โ ๐ด) โ ((absโ๐ถ) ยท if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) = ((absโ๐ถ) ยท 0)) |
119 | | iffalse 4494 |
. . . . . . . . . . . . 13
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0) = 0) |
120 | 119 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โง ยฌ ๐ฅ โ ๐ด) โ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0) = 0) |
121 | 116, 118,
120 | 3eqtr4d 2788 |
. . . . . . . . . . 11
โข ((๐ โง ยฌ ๐ฅ โ ๐ด) โ ((absโ๐ถ) ยท if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) = if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0)) |
122 | 113, 121 | pm2.61dan 812 |
. . . . . . . . . 10
โข (๐ โ ((absโ๐ถ) ยท if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) = if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0)) |
123 | 122 | mpteq2dv 5206 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ โ โฆ ((absโ๐ถ) ยท if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0))) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0))) |
124 | 109, 123 | eqtrd 2778 |
. . . . . . . 8
โข (๐ โ ((โ ร
{(absโ๐ถ)})
โf ยท (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0))) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0))) |
125 | 124 | fveq2d 6842 |
. . . . . . 7
โข (๐ โ
(โซ2โ((โ ร {(absโ๐ถ)}) โf ยท (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)))) = (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0)))) |
126 | 97 | oveq2d 7366 |
. . . . . . 7
โข (๐ โ ((absโ๐ถ) ยท
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
((absโ(โโ๐ต)) + (absโ(โโ๐ต))), 0)))) = ((absโ๐ถ) ยท
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) + (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)))))) |
127 | 104, 125,
126 | 3eqtr3d 2786 |
. . . . . 6
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ((absโ๐ถ) ยท
((absโ(โโ๐ต)) + (absโ(โโ๐ต)))), 0))) = ((absโ๐ถ) ยท
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) + (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)))))) |
128 | 100, 98 | remulcld 11119 |
. . . . . 6
โข (๐ โ ((absโ๐ถ) ยท
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) + (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))))) โ
โ) |
129 | 127, 128 | eqeltrd 2839 |
. . . . 5
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ((absโ๐ถ) ยท
((absโ(โโ๐ต)) + (absโ(โโ๐ต)))), 0))) โ
โ) |
130 | 129 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ (0...3)) โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ((absโ๐ถ) ยท
((absโ(โโ๐ต)) + (absโ(โโ๐ต)))), 0))) โ
โ) |
131 | 100 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ๐ถ) โ โ) |
132 | 131, 44 | remulcld 11119 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))) โ โ) |
133 | 132 | rexrd 11139 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))) โ
โ*) |
134 | 101 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค (absโ๐ถ)) |
135 | 131, 44, 134, 47 | mulge0d 11666 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค ((absโ๐ถ) ยท
((absโ(โโ๐ต)) + (absโ(โโ๐ต))))) |
136 | | elxrge0 13303 |
. . . . . . . . 9
โข
(((absโ๐ถ)
ยท ((absโ(โโ๐ต)) + (absโ(โโ๐ต)))) โ (0[,]+โ)
โ (((absโ๐ถ)
ยท ((absโ(โโ๐ต)) + (absโ(โโ๐ต)))) โ โ*
โง 0 โค ((absโ๐ถ)
ยท ((absโ(โโ๐ต)) + (absโ(โโ๐ต)))))) |
137 | 133, 135,
136 | sylanbrc 584 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))) โ (0[,]+โ)) |
138 | 32 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ยฌ ๐ฅ โ ๐ด) โ 0 โ
(0[,]+โ)) |
139 | 137, 138 | ifclda 4520 |
. . . . . . 7
โข (๐ โ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0) โ
(0[,]+โ)) |
140 | 139 | ad2antrr 725 |
. . . . . 6
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0) โ
(0[,]+โ)) |
141 | 140 | fmpttd 7058 |
. . . . 5
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))),
0)):โโถ(0[,]+โ)) |
142 | 9 | abscld 15256 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ๐ต) โ โ) |
143 | 131, 142 | remulcld 11119 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโ๐ถ) ยท (absโ๐ต)) โ โ) |
144 | 143 | adantlr 714 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ ((absโ๐ถ) ยท (absโ๐ต)) โ โ) |
145 | 132 | adantlr 714 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))) โ โ) |
146 | 22 | releabsd 15271 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (โโ((๐ถ ยท ๐ต) / (iโ๐))) โค (absโ((๐ถ ยท ๐ต) / (iโ๐)))) |
147 | 11, 18, 21 | absdivd 15275 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (absโ((๐ถ ยท ๐ต) / (iโ๐))) = ((absโ(๐ถ ยท ๐ต)) / (absโ(iโ๐)))) |
148 | | elfznn0 13463 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (0...3) โ ๐ โ
โ0) |
149 | | absexp 15124 |
. . . . . . . . . . . . . . . . . . . 20
โข ((i
โ โ โง ๐
โ โ0) โ (absโ(iโ๐)) = ((absโi)โ๐)) |
150 | 14, 148, 149 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (0...3) โ
(absโ(iโ๐)) =
((absโi)โ๐)) |
151 | | absi 15106 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(absโi) = 1 |
152 | 151 | oveq1i 7360 |
. . . . . . . . . . . . . . . . . . . 20
โข
((absโi)โ๐) = (1โ๐) |
153 | | 1exp 13926 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โค โ
(1โ๐) =
1) |
154 | 12, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (0...3) โ
(1โ๐) =
1) |
155 | 152, 154 | eqtrid 2790 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (0...3) โ
((absโi)โ๐) =
1) |
156 | 150, 155 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (0...3) โ
(absโ(iโ๐)) =
1) |
157 | 156 | oveq2d 7366 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (0...3) โ
((absโ(๐ถ ยท
๐ต)) /
(absโ(iโ๐))) =
((absโ(๐ถ ยท
๐ต)) / 1)) |
158 | 157 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ ((absโ(๐ถ ยท ๐ต)) / (absโ(iโ๐))) = ((absโ(๐ถ ยท ๐ต)) / 1)) |
159 | 10 | abscld 15256 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(๐ถ ยท ๐ต)) โ โ) |
160 | 159 | recnd 11117 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(๐ถ ยท ๐ต)) โ โ) |
161 | 160 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (absโ(๐ถ ยท ๐ต)) โ โ) |
162 | 161 | div1d 11857 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ ((absโ(๐ถ ยท ๐ต)) / 1) = (absโ(๐ถ ยท ๐ต))) |
163 | 147, 158,
162 | 3eqtrd 2782 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (absโ((๐ถ ยท ๐ต) / (iโ๐))) = (absโ(๐ถ ยท ๐ต))) |
164 | 4, 9 | absmuld 15274 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(๐ถ ยท ๐ต)) = ((absโ๐ถ) ยท (absโ๐ต))) |
165 | 164 | adantlr 714 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (absโ(๐ถ ยท ๐ต)) = ((absโ๐ถ) ยท (absโ๐ต))) |
166 | 163, 165 | eqtrd 2778 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (absโ((๐ถ ยท ๐ต) / (iโ๐))) = ((absโ๐ถ) ยท (absโ๐ต))) |
167 | 146, 166 | breqtrd 5130 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (โโ((๐ถ ยท ๐ต) / (iโ๐))) โค ((absโ๐ถ) ยท (absโ๐ต))) |
168 | | mulcl 11069 |
. . . . . . . . . . . . . . . . . 18
โข ((i
โ โ โง (โโ๐ต) โ โ) โ (i ยท
(โโ๐ต)) โ
โ) |
169 | 14, 42, 168 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ ๐ด) โ (i ยท (โโ๐ต)) โ
โ) |
170 | 39, 169 | abstrid 15276 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ((โโ๐ต) + (i ยท
(โโ๐ต)))) โค
((absโ(โโ๐ต)) + (absโ(i ยท
(โโ๐ต))))) |
171 | 9 | replimd 15016 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต = ((โโ๐ต) + (i ยท (โโ๐ต)))) |
172 | 171 | fveq2d 6842 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ๐ต) = (absโ((โโ๐ต) + (i ยท
(โโ๐ต))))) |
173 | | absmul 15114 |
. . . . . . . . . . . . . . . . . . . 20
โข ((i
โ โ โง (โโ๐ต) โ โ) โ (absโ(i
ยท (โโ๐ต))) = ((absโi) ยท
(absโ(โโ๐ต)))) |
174 | 14, 42, 173 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(i ยท
(โโ๐ต))) =
((absโi) ยท (absโ(โโ๐ต)))) |
175 | 151 | oveq1i 7360 |
. . . . . . . . . . . . . . . . . . 19
โข
((absโi) ยท (absโ(โโ๐ต))) = (1 ยท
(absโ(โโ๐ต))) |
176 | 174, 175 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(i ยท
(โโ๐ต))) = (1
ยท (absโ(โโ๐ต)))) |
177 | 43 | recnd 11117 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(โโ๐ต)) โ
โ) |
178 | 177 | mulid2d 11107 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ ๐ด) โ (1 ยท
(absโ(โโ๐ต))) = (absโ(โโ๐ต))) |
179 | 176, 178 | eqtr2d 2779 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(โโ๐ต)) = (absโ(i ยท
(โโ๐ต)))) |
180 | 179 | oveq2d 7366 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))) = ((absโ(โโ๐ต)) + (absโ(i ยท
(โโ๐ต))))) |
181 | 170, 172,
180 | 3brtr4d 5136 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ๐ต) โค ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))) |
182 | 142, 44, 131, 134, 181 | lemul2ad 12029 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโ๐ถ) ยท (absโ๐ต)) โค ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))))) |
183 | 182 | adantlr 714 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ ((absโ๐ถ) ยท (absโ๐ต)) โค ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))))) |
184 | 23, 144, 145, 167, 183 | letrd 11246 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ (โโ((๐ถ ยท ๐ต) / (iโ๐))) โค ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))))) |
185 | 135 | adantlr 714 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ 0 โค ((absโ๐ถ) ยท
((absโ(โโ๐ต)) + (absโ(โโ๐ต))))) |
186 | | breq1 5107 |
. . . . . . . . . . . . 13
โข
((โโ((๐ถ
ยท ๐ต) / (iโ๐))) = if(0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ ((โโ((๐ถ ยท ๐ต) / (iโ๐))) โค ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))))) |
187 | | breq1 5107 |
. . . . . . . . . . . . 13
โข (0 = if(0
โค (โโ((๐ถ
ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โ (0 โค ((absโ๐ถ) ยท
((absโ(โโ๐ต)) + (absโ(โโ๐ต)))) โ if(0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))))) |
188 | 186, 187 | ifboth 4524 |
. . . . . . . . . . . 12
โข
(((โโ((๐ถ
ยท ๐ต) / (iโ๐))) โค ((absโ๐ถ) ยท
((absโ(โโ๐ต)) + (absโ(โโ๐ต)))) โง 0 โค
((absโ๐ถ) ยท
((absโ(โโ๐ต)) + (absโ(โโ๐ต))))) โ if(0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))))) |
189 | 184, 185,
188 | syl2anc 585 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))))) |
190 | | iftrue 4491 |
. . . . . . . . . . . 12
โข (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) = if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) |
191 | 190 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) = if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) |
192 | 111 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0) = ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))))) |
193 | 189, 191,
192 | 3brtr4d 5136 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (0...3)) โง ๐ฅ โ ๐ด) โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) โค if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0)) |
194 | 193 | ex 414 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) โค if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0))) |
195 | | 0le0 12188 |
. . . . . . . . . . 11
โข 0 โค
0 |
196 | 195 | a1i 11 |
. . . . . . . . . 10
โข (ยฌ
๐ฅ โ ๐ด โ 0 โค 0) |
197 | | iffalse 4494 |
. . . . . . . . . 10
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) = 0) |
198 | 196, 197,
119 | 3brtr4d 5136 |
. . . . . . . . 9
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) โค if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0)) |
199 | 194, 198 | pm2.61d1 180 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...3)) โ if(๐ฅ โ ๐ด, if(0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0), 0) โค if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0)) |
200 | 2, 199 | eqbrtrid 5139 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0)) |
201 | 200 | ralrimivw 3146 |
. . . . . 6
โข ((๐ โง ๐ โ (0...3)) โ โ๐ฅ โ โ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0)) |
202 | 55 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ โ โ
V) |
203 | | eqidd 2739 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) |
204 | | eqidd 2739 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0))) |
205 | 202, 36, 140, 203, 204 | ofrfval2 7629 |
. . . . . 6
โข ((๐ โง ๐ โ (0...3)) โ ((๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0)) โ โ๐ฅ โ โ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0) โค if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0))) |
206 | 201, 205 | mpbird 257 |
. . . . 5
โข ((๐ โง ๐ โ (0...3)) โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0))) |
207 | | itg2le 25026 |
. . . . 5
โข (((๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)):โโถ(0[,]+โ) โง
(๐ฅ โ โ โฆ
if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0)):โโถ(0[,]+โ)
โง (๐ฅ โ โ
โฆ if((๐ฅ โ ๐ด โง 0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ๐ถ) ยท ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))), 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โค
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ((absโ๐ถ) ยท
((absโ(โโ๐ต)) + (absโ(โโ๐ต)))), 0)))) |
208 | 37, 141, 206, 207 | syl3anc 1372 |
. . . 4
โข ((๐ โง ๐ โ (0...3)) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โค
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ((absโ๐ถ) ยท
((absโ(โโ๐ต)) + (absโ(โโ๐ต)))), 0)))) |
209 | | itg2lecl 25025 |
. . . 4
โข (((๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ((๐ถ ยท
๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)):โโถ(0[,]+โ) โง
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ((absโ๐ถ) ยท
((absโ(โโ๐ต)) + (absโ(โโ๐ต)))), 0))) โ โ โง
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โค
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ((absโ๐ถ) ยท
((absโ(โโ๐ต)) + (absโ(โโ๐ต)))), 0)))) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โ โ) |
210 | 37, 130, 208, 209 | syl3anc 1372 |
. . 3
โข ((๐ โง ๐ โ (0...3)) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โ โ) |
211 | 210 | ralrimiva 3142 |
. 2
โข (๐ โ โ๐ โ
(0...3)(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โ โ) |
212 | | eqidd 2739 |
. . 3
โข (๐ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) |
213 | | eqidd 2739 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ((๐ถ ยท ๐ต) / (iโ๐))) = (โโ((๐ถ ยท ๐ต) / (iโ๐)))) |
214 | 212, 213,
10 | isibl2 25053 |
. 2
โข (๐ โ ((๐ฅ โ ๐ด โฆ (๐ถ ยท ๐ต)) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (๐ถ ยท ๐ต)) โ MblFn โง โ๐ โ
(0...3)(โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ((๐ถ ยท ๐ต) / (iโ๐)))), (โโ((๐ถ ยท ๐ต) / (iโ๐))), 0))) โ โ))) |
215 | 1, 211, 214 | mpbir2and 712 |
1
โข (๐ โ (๐ฅ โ ๐ด โฆ (๐ถ ยท ๐ต)) โ
๐ฟ1) |