Step | Hyp | Ref
| Expression |
1 | | iblabsnc.m |
. 2
โข (๐ โ (๐ฅ โ ๐ด โฆ (absโ๐ต)) โ MblFn) |
2 | | iblabsnc.2 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ
๐ฟ1) |
3 | | iblmbf 25054 |
. . . . . . . . . . 11
โข ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
5 | | iblabsnc.1 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) |
6 | 4, 5 | mbfmptcl 24922 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
7 | 6 | abscld 15256 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ๐ต) โ โ) |
8 | 7 | rexrd 11139 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ๐ต) โ
โ*) |
9 | 6 | absge0d 15264 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค (absโ๐ต)) |
10 | | elxrge0 13303 |
. . . . . . 7
โข
((absโ๐ต)
โ (0[,]+โ) โ ((absโ๐ต) โ โ* โง 0 โค
(absโ๐ต))) |
11 | 8, 9, 10 | sylanbrc 584 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ๐ต) โ (0[,]+โ)) |
12 | | 0e0iccpnf 13305 |
. . . . . . 7
โข 0 โ
(0[,]+โ) |
13 | 12 | a1i 11 |
. . . . . 6
โข ((๐ โง ยฌ ๐ฅ โ ๐ด) โ 0 โ
(0[,]+โ)) |
14 | 11, 13 | ifclda 4520 |
. . . . 5
โข (๐ โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) โ
(0[,]+โ)) |
15 | 14 | adantr 482 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) โ
(0[,]+โ)) |
16 | 15 | fmpttd 7058 |
. . 3
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต),
0)):โโถ(0[,]+โ)) |
17 | | reex 11076 |
. . . . . . . . 9
โข โ
โ V |
18 | 17 | a1i 11 |
. . . . . . . 8
โข (๐ โ โ โ
V) |
19 | 6 | recld 15013 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
20 | 19 | recnd 11117 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
21 | 20 | abscld 15256 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(โโ๐ต)) โ
โ) |
22 | 20 | absge0d 15264 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค
(absโ(โโ๐ต))) |
23 | | elrege0 13300 |
. . . . . . . . . . 11
โข
((absโ(โโ๐ต)) โ (0[,)+โ) โ
((absโ(โโ๐ต)) โ โ โง 0 โค
(absโ(โโ๐ต)))) |
24 | 21, 22, 23 | sylanbrc 584 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(โโ๐ต)) โ
(0[,)+โ)) |
25 | | 0e0icopnf 13304 |
. . . . . . . . . . 11
โข 0 โ
(0[,)+โ) |
26 | 25 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง ยฌ ๐ฅ โ ๐ด) โ 0 โ
(0[,)+โ)) |
27 | 24, 26 | ifclda 4520 |
. . . . . . . . 9
โข (๐ โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) โ
(0[,)+โ)) |
28 | 27 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) โ
(0[,)+โ)) |
29 | 6 | imcld 15014 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
30 | 29 | recnd 11117 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
31 | 30 | abscld 15256 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(โโ๐ต)) โ
โ) |
32 | 30 | absge0d 15264 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค
(absโ(โโ๐ต))) |
33 | | elrege0 13300 |
. . . . . . . . . . 11
โข
((absโ(โโ๐ต)) โ (0[,)+โ) โ
((absโ(โโ๐ต)) โ โ โง 0 โค
(absโ(โโ๐ต)))) |
34 | 31, 32, 33 | sylanbrc 584 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(โโ๐ต)) โ
(0[,)+โ)) |
35 | 34, 26 | ifclda 4520 |
. . . . . . . . 9
โข (๐ โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) โ
(0[,)+โ)) |
36 | 35 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) โ
(0[,)+โ)) |
37 | | eqidd 2739 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) |
38 | | eqidd 2739 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) |
39 | 18, 28, 36, 37, 38 | offval2 7628 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โf + (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) = (๐ฅ โ โ โฆ (if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)))) |
40 | | iftrue 4491 |
. . . . . . . . . . 11
โข (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) = (absโ(โโ๐ต))) |
41 | | iftrue 4491 |
. . . . . . . . . . 11
โข (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) =
(absโ(โโ๐ต))) |
42 | 40, 41 | oveq12d 7368 |
. . . . . . . . . 10
โข (๐ฅ โ ๐ด โ (if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) =
((absโ(โโ๐ต)) + (absโ(โโ๐ต)))) |
43 | | iftrue 4491 |
. . . . . . . . . 10
โข (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0) = ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))) |
44 | 42, 43 | eqtr4d 2781 |
. . . . . . . . 9
โข (๐ฅ โ ๐ด โ (if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) |
45 | | 00id 11264 |
. . . . . . . . . 10
โข (0 + 0) =
0 |
46 | | iffalse 4494 |
. . . . . . . . . . 11
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) = 0) |
47 | | iffalse 4494 |
. . . . . . . . . . 11
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) = 0) |
48 | 46, 47 | oveq12d 7368 |
. . . . . . . . . 10
โข (ยฌ
๐ฅ โ ๐ด โ (if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = (0 +
0)) |
49 | | iffalse 4494 |
. . . . . . . . . 10
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0) = 0) |
50 | 45, 48, 49 | 3eqtr4a 2804 |
. . . . . . . . 9
โข (ยฌ
๐ฅ โ ๐ด โ (if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) |
51 | 44, 50 | pm2.61i 182 |
. . . . . . . 8
โข (if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0) |
52 | 51 | mpteq2i 5209 |
. . . . . . 7
โข (๐ฅ โ โ โฆ
(if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0) + if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) |
53 | 39, 52 | eqtr2di 2795 |
. . . . . 6
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) = ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โf + (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)))) |
54 | 53 | fveq2d 6842 |
. . . . 5
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
((absโ(โโ๐ต)) + (absโ(โโ๐ต))), 0))) =
(โซ2โ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โf + (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))))) |
55 | | eqid 2738 |
. . . . . . . 8
โข (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) |
56 | 6 | iblcn 25085 |
. . . . . . . . . 10
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1
โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1))) |
57 | 2, 56 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ ((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1)) |
58 | 57 | simpld 496 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
59 | 5, 2, 55, 58, 19 | iblabsnclem 36027 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โ MblFn โง
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
(absโ(โโ๐ต)), 0))) โ โ)) |
60 | 59 | simpld 496 |
. . . . . 6
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โ MblFn) |
61 | 28 | fmpttd 7058 |
. . . . . 6
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)),
0)):โโถ(0[,)+โ)) |
62 | 59 | simprd 497 |
. . . . . 6
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
(absโ(โโ๐ต)), 0))) โ โ) |
63 | 36 | fmpttd 7058 |
. . . . . 6
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)),
0)):โโถ(0[,)+โ)) |
64 | | eqid 2738 |
. . . . . . . 8
โข (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) |
65 | 57 | simprd 497 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
66 | 5, 2, 64, 65, 29 | iblabsnclem 36027 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โ MblFn โง
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
(absโ(โโ๐ต)), 0))) โ โ)) |
67 | 66 | simprd 497 |
. . . . . 6
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
(absโ(โโ๐ต)), 0))) โ โ) |
68 | 60, 61, 62, 63, 67 | itg2addnc 36018 |
. . . . 5
โข (๐ โ
(โซ2โ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)) โf + (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)))) =
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) + (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))))) |
69 | 54, 68 | eqtrd 2778 |
. . . 4
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
((absโ(โโ๐ต)) + (absโ(โโ๐ต))), 0))) =
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) + (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))))) |
70 | 62, 67 | readdcld 11118 |
. . . 4
โข (๐ โ
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0))) + (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ(โโ๐ต)), 0)))) โ
โ) |
71 | 69, 70 | eqeltrd 2839 |
. . 3
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
((absโ(โโ๐ต)) + (absโ(โโ๐ต))), 0))) โ
โ) |
72 | 21, 31 | readdcld 11118 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))) โ โ) |
73 | 72 | rexrd 11139 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))) โ
โ*) |
74 | 21, 31, 22, 32 | addge0d 11665 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค
((absโ(โโ๐ต)) + (absโ(โโ๐ต)))) |
75 | | elxrge0 13303 |
. . . . . . . 8
โข
(((absโ(โโ๐ต)) + (absโ(โโ๐ต))) โ (0[,]+โ) โ
(((absโ(โโ๐ต)) + (absโ(โโ๐ต))) โ โ*
โง 0 โค ((absโ(โโ๐ต)) + (absโ(โโ๐ต))))) |
76 | 73, 74, 75 | sylanbrc 584 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))) โ (0[,]+โ)) |
77 | 76, 13 | ifclda 4520 |
. . . . . 6
โข (๐ โ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0) โ
(0[,]+โ)) |
78 | 77 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0) โ
(0[,]+โ)) |
79 | 78 | fmpttd 7058 |
. . . 4
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))),
0)):โโถ(0[,]+โ)) |
80 | | ax-icn 11044 |
. . . . . . . . . . 11
โข i โ
โ |
81 | | mulcl 11069 |
. . . . . . . . . . 11
โข ((i
โ โ โง (โโ๐ต) โ โ) โ (i ยท
(โโ๐ต)) โ
โ) |
82 | 80, 30, 81 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ (i ยท (โโ๐ต)) โ
โ) |
83 | 20, 82 | abstrid 15276 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ((โโ๐ต) + (i ยท
(โโ๐ต)))) โค
((absโ(โโ๐ต)) + (absโ(i ยท
(โโ๐ต))))) |
84 | | iftrue 4491 |
. . . . . . . . . . 11
โข (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) = (absโ๐ต)) |
85 | 84 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) = (absโ๐ต)) |
86 | 6 | replimd 15016 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต = ((โโ๐ต) + (i ยท (โโ๐ต)))) |
87 | 86 | fveq2d 6842 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ๐ต) = (absโ((โโ๐ต) + (i ยท
(โโ๐ต))))) |
88 | 85, 87 | eqtrd 2778 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) = (absโ((โโ๐ต) + (i ยท
(โโ๐ต))))) |
89 | 43 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0) = ((absโ(โโ๐ต)) +
(absโ(โโ๐ต)))) |
90 | | absmul 15114 |
. . . . . . . . . . . . 13
โข ((i
โ โ โง (โโ๐ต) โ โ) โ (absโ(i
ยท (โโ๐ต))) = ((absโi) ยท
(absโ(โโ๐ต)))) |
91 | 80, 30, 90 | sylancr 588 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(i ยท
(โโ๐ต))) =
((absโi) ยท (absโ(โโ๐ต)))) |
92 | | absi 15106 |
. . . . . . . . . . . . . 14
โข
(absโi) = 1 |
93 | 92 | oveq1i 7360 |
. . . . . . . . . . . . 13
โข
((absโi) ยท (absโ(โโ๐ต))) = (1 ยท
(absโ(โโ๐ต))) |
94 | 31 | recnd 11117 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(โโ๐ต)) โ
โ) |
95 | 94 | mulid2d 11107 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ (1 ยท
(absโ(โโ๐ต))) = (absโ(โโ๐ต))) |
96 | 93, 95 | eqtrid 2790 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโi) ยท
(absโ(โโ๐ต))) = (absโ(โโ๐ต))) |
97 | 91, 96 | eqtr2d 2779 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ(โโ๐ต)) = (absโ(i ยท
(โโ๐ต)))) |
98 | 97 | oveq2d 7366 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))) = ((absโ(โโ๐ต)) + (absโ(i ยท
(โโ๐ต))))) |
99 | 89, 98 | eqtrd 2778 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0) = ((absโ(โโ๐ต)) + (absโ(i ยท
(โโ๐ต))))) |
100 | 83, 88, 99 | 3brtr4d 5136 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) โค if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) |
101 | 100 | ex 414 |
. . . . . . 7
โข (๐ โ (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) โค if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0))) |
102 | | 0le0 12188 |
. . . . . . . . 9
โข 0 โค
0 |
103 | 102 | a1i 11 |
. . . . . . . 8
โข (ยฌ
๐ฅ โ ๐ด โ 0 โค 0) |
104 | | iffalse 4494 |
. . . . . . . 8
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) = 0) |
105 | 103, 104,
49 | 3brtr4d 5136 |
. . . . . . 7
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) โค if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) |
106 | 101, 105 | pm2.61d1 180 |
. . . . . 6
โข (๐ โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) โค if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) |
107 | 106 | ralrimivw 3146 |
. . . . 5
โข (๐ โ โ๐ฅ โ โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) โค if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) |
108 | | eqidd 2739 |
. . . . . 6
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0))) |
109 | | eqidd 2739 |
. . . . . 6
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0))) |
110 | 18, 15, 78, 108, 109 | ofrfval2 7629 |
. . . . 5
โข (๐ โ ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0)) โ โ๐ฅ โ โ if(๐ฅ โ ๐ด, (absโ๐ต), 0) โค if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0))) |
111 | 107, 110 | mpbird 257 |
. . . 4
โข (๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0))) |
112 | | itg2le 25026 |
. . . 4
โข (((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0)):โโถ(0[,]+โ) โง
(๐ฅ โ โ โฆ
if(๐ฅ โ ๐ด,
((absโ(โโ๐ต)) + (absโ(โโ๐ต))),
0)):โโถ(0[,]+โ) โง (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ((absโ(โโ๐ต)) +
(absโ(โโ๐ต))), 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ๐ต), 0))) โค
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
((absโ(โโ๐ต)) + (absโ(โโ๐ต))), 0)))) |
113 | 16, 79, 111, 112 | syl3anc 1372 |
. . 3
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ๐ต), 0))) โค
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
((absโ(โโ๐ต)) + (absโ(โโ๐ต))), 0)))) |
114 | | itg2lecl 25025 |
. . 3
โข (((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, (absโ๐ต), 0)):โโถ(0[,]+โ) โง
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
((absโ(โโ๐ต)) + (absโ(โโ๐ต))), 0))) โ โ โง
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ๐ต), 0))) โค
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด,
((absโ(โโ๐ต)) + (absโ(โโ๐ต))), 0)))) โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ๐ต), 0))) โ
โ) |
115 | 16, 71, 113, 114 | syl3anc 1372 |
. 2
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ๐ต), 0))) โ
โ) |
116 | 7, 9 | iblpos 25079 |
. 2
โข (๐ โ ((๐ฅ โ ๐ด โฆ (absโ๐ต)) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (absโ๐ต)) โ MblFn โง
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, (absโ๐ต), 0))) โ
โ))) |
117 | 1, 115, 116 | mpbir2and 712 |
1
โข (๐ โ (๐ฅ โ ๐ด โฆ (absโ๐ต)) โ
๐ฟ1) |