Step | Hyp | Ref
| Expression |
1 | | absf 15157 |
. . . . 5
β’
abs:ββΆβ |
2 | 1 | a1i 11 |
. . . 4
β’ (π β
abs:ββΆβ) |
3 | | iblabs.2 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ π΅) β
πΏ1) |
4 | | iblmbf 25054 |
. . . . . 6
β’ ((π₯ β π΄ β¦ π΅) β πΏ1 β (π₯ β π΄ β¦ π΅) β MblFn) |
5 | 3, 4 | syl 17 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) |
6 | | iblabs.1 |
. . . . 5
β’ ((π β§ π₯ β π΄) β π΅ β π) |
7 | 5, 6 | mbfmptcl 24922 |
. . . 4
β’ ((π β§ π₯ β π΄) β π΅ β β) |
8 | 2, 7 | cofmpt 7073 |
. . 3
β’ (π β (abs β (π₯ β π΄ β¦ π΅)) = (π₯ β π΄ β¦ (absβπ΅))) |
9 | 7 | fmpttd 7058 |
. . . 4
β’ (π β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
10 | | ax-resscn 11042 |
. . . . . . 7
β’ β
β β |
11 | | ssid 3965 |
. . . . . . 7
β’ β
β β |
12 | | cncfss 24184 |
. . . . . . 7
β’ ((β
β β β§ β β β) β (ββcnββ) β (ββcnββ)) |
13 | 10, 11, 12 | mp2an 691 |
. . . . . 6
β’
(ββcnββ)
β (ββcnββ) |
14 | | abscncf 24186 |
. . . . . 6
β’ abs
β (ββcnββ) |
15 | 13, 14 | sselii 3940 |
. . . . 5
β’ abs
β (ββcnββ) |
16 | 15 | a1i 11 |
. . . 4
β’ (π β abs β
(ββcnββ)) |
17 | | cncombf 24944 |
. . . 4
β’ (((π₯ β π΄ β¦ π΅) β MblFn β§ (π₯ β π΄ β¦ π΅):π΄βΆβ β§ abs β
(ββcnββ)) β
(abs β (π₯ β
π΄ β¦ π΅)) β MblFn) |
18 | 5, 9, 16, 17 | syl3anc 1372 |
. . 3
β’ (π β (abs β (π₯ β π΄ β¦ π΅)) β MblFn) |
19 | 8, 18 | eqeltrrd 2840 |
. 2
β’ (π β (π₯ β π΄ β¦ (absβπ΅)) β MblFn) |
20 | 7 | abscld 15256 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (absβπ΅) β β) |
21 | 20 | rexrd 11139 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (absβπ΅) β
β*) |
22 | 7 | absge0d 15264 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β 0 β€ (absβπ΅)) |
23 | | elxrge0 13303 |
. . . . . . 7
β’
((absβπ΅)
β (0[,]+β) β ((absβπ΅) β β* β§ 0 β€
(absβπ΅))) |
24 | 21, 22, 23 | sylanbrc 584 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (absβπ΅) β (0[,]+β)) |
25 | | 0e0iccpnf 13305 |
. . . . . . 7
β’ 0 β
(0[,]+β) |
26 | 25 | a1i 11 |
. . . . . 6
β’ ((π β§ Β¬ π₯ β π΄) β 0 β
(0[,]+β)) |
27 | 24, 26 | ifclda 4520 |
. . . . 5
β’ (π β if(π₯ β π΄, (absβπ΅), 0) β
(0[,]+β)) |
28 | 27 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β β) β if(π₯ β π΄, (absβπ΅), 0) β
(0[,]+β)) |
29 | 28 | fmpttd 7058 |
. . 3
β’ (π β (π₯ β β β¦ if(π₯ β π΄, (absβπ΅),
0)):ββΆ(0[,]+β)) |
30 | | reex 11076 |
. . . . . . . . 9
β’ β
β V |
31 | 30 | a1i 11 |
. . . . . . . 8
β’ (π β β β
V) |
32 | 7 | recld 15013 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β (ββπ΅) β β) |
33 | 32 | recnd 11117 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (ββπ΅) β β) |
34 | 33 | abscld 15256 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (absβ(ββπ΅)) β
β) |
35 | 33 | absge0d 15264 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β 0 β€
(absβ(ββπ΅))) |
36 | | elrege0 13300 |
. . . . . . . . . . 11
β’
((absβ(ββπ΅)) β (0[,)+β) β
((absβ(ββπ΅)) β β β§ 0 β€
(absβ(ββπ΅)))) |
37 | 34, 35, 36 | sylanbrc 584 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (absβ(ββπ΅)) β
(0[,)+β)) |
38 | | 0e0icopnf 13304 |
. . . . . . . . . . 11
β’ 0 β
(0[,)+β) |
39 | 38 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ Β¬ π₯ β π΄) β 0 β
(0[,)+β)) |
40 | 37, 39 | ifclda 4520 |
. . . . . . . . 9
β’ (π β if(π₯ β π΄, (absβ(ββπ΅)), 0) β
(0[,)+β)) |
41 | 40 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β if(π₯ β π΄, (absβ(ββπ΅)), 0) β
(0[,)+β)) |
42 | 7 | imcld 15014 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β (ββπ΅) β β) |
43 | 42 | recnd 11117 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (ββπ΅) β β) |
44 | 43 | abscld 15256 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (absβ(ββπ΅)) β
β) |
45 | 43 | absge0d 15264 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β 0 β€
(absβ(ββπ΅))) |
46 | | elrege0 13300 |
. . . . . . . . . . 11
β’
((absβ(ββπ΅)) β (0[,)+β) β
((absβ(ββπ΅)) β β β§ 0 β€
(absβ(ββπ΅)))) |
47 | 44, 45, 46 | sylanbrc 584 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (absβ(ββπ΅)) β
(0[,)+β)) |
48 | 47, 39 | ifclda 4520 |
. . . . . . . . 9
β’ (π β if(π₯ β π΄, (absβ(ββπ΅)), 0) β
(0[,)+β)) |
49 | 48 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β if(π₯ β π΄, (absβ(ββπ΅)), 0) β
(0[,)+β)) |
50 | | eqidd 2739 |
. . . . . . . 8
β’ (π β (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) = (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0))) |
51 | | eqidd 2739 |
. . . . . . . 8
β’ (π β (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) = (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0))) |
52 | 31, 41, 49, 50, 51 | offval2 7628 |
. . . . . . 7
β’ (π β ((π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) βf + (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0))) = (π₯ β β β¦ (if(π₯ β π΄, (absβ(ββπ΅)), 0) + if(π₯ β π΄, (absβ(ββπ΅)), 0)))) |
53 | | iftrue 4491 |
. . . . . . . . . . 11
β’ (π₯ β π΄ β if(π₯ β π΄, (absβ(ββπ΅)), 0) = (absβ(ββπ΅))) |
54 | | iftrue 4491 |
. . . . . . . . . . 11
β’ (π₯ β π΄ β if(π₯ β π΄, (absβ(ββπ΅)), 0) =
(absβ(ββπ΅))) |
55 | 53, 54 | oveq12d 7368 |
. . . . . . . . . 10
β’ (π₯ β π΄ β (if(π₯ β π΄, (absβ(ββπ΅)), 0) + if(π₯ β π΄, (absβ(ββπ΅)), 0)) =
((absβ(ββπ΅)) + (absβ(ββπ΅)))) |
56 | | iftrue 4491 |
. . . . . . . . . 10
β’ (π₯ β π΄ β if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0) = ((absβ(ββπ΅)) +
(absβ(ββπ΅)))) |
57 | 55, 56 | eqtr4d 2781 |
. . . . . . . . 9
β’ (π₯ β π΄ β (if(π₯ β π΄, (absβ(ββπ΅)), 0) + if(π₯ β π΄, (absβ(ββπ΅)), 0)) = if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0)) |
58 | | 00id 11264 |
. . . . . . . . . 10
β’ (0 + 0) =
0 |
59 | | iffalse 4494 |
. . . . . . . . . . 11
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, (absβ(ββπ΅)), 0) = 0) |
60 | | iffalse 4494 |
. . . . . . . . . . 11
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, (absβ(ββπ΅)), 0) = 0) |
61 | 59, 60 | oveq12d 7368 |
. . . . . . . . . 10
β’ (Β¬
π₯ β π΄ β (if(π₯ β π΄, (absβ(ββπ΅)), 0) + if(π₯ β π΄, (absβ(ββπ΅)), 0)) = (0 +
0)) |
62 | | iffalse 4494 |
. . . . . . . . . 10
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0) = 0) |
63 | 58, 61, 62 | 3eqtr4a 2804 |
. . . . . . . . 9
β’ (Β¬
π₯ β π΄ β (if(π₯ β π΄, (absβ(ββπ΅)), 0) + if(π₯ β π΄, (absβ(ββπ΅)), 0)) = if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0)) |
64 | 57, 63 | pm2.61i 182 |
. . . . . . . 8
β’ (if(π₯ β π΄, (absβ(ββπ΅)), 0) + if(π₯ β π΄, (absβ(ββπ΅)), 0)) = if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0) |
65 | 64 | mpteq2i 5209 |
. . . . . . 7
β’ (π₯ β β β¦
(if(π₯ β π΄, (absβ(ββπ΅)), 0) + if(π₯ β π΄, (absβ(ββπ΅)), 0))) = (π₯ β β β¦ if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0)) |
66 | 52, 65 | eqtr2di 2795 |
. . . . . 6
β’ (π β (π₯ β β β¦ if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0)) = ((π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) βf + (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)))) |
67 | 66 | fveq2d 6842 |
. . . . 5
β’ (π β
(β«2β(π₯
β β β¦ if(π₯
β π΄,
((absβ(ββπ΅)) + (absβ(ββπ΅))), 0))) =
(β«2β((π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) βf + (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0))))) |
68 | | eqid 2738 |
. . . . . . . 8
β’ (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) = (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) |
69 | 7 | iblcn 25085 |
. . . . . . . . . 10
β’ (π β ((π₯ β π΄ β¦ π΅) β πΏ1 β
((π₯ β π΄ β¦ (ββπ΅)) β πΏ1
β§ (π₯ β π΄ β¦ (ββπ΅)) β
πΏ1))) |
70 | 3, 69 | mpbid 231 |
. . . . . . . . 9
β’ (π β ((π₯ β π΄ β¦ (ββπ΅)) β πΏ1 β§ (π₯ β π΄ β¦ (ββπ΅)) β
πΏ1)) |
71 | 70 | simpld 496 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ (ββπ΅)) β
πΏ1) |
72 | 6, 3, 68, 71, 32 | iblabslem 25114 |
. . . . . . 7
β’ (π β ((π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) β MblFn β§
(β«2β(π₯
β β β¦ if(π₯
β π΄,
(absβ(ββπ΅)), 0))) β β)) |
73 | 72 | simpld 496 |
. . . . . 6
β’ (π β (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) β MblFn) |
74 | 41 | fmpttd 7058 |
. . . . . 6
β’ (π β (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)),
0)):ββΆ(0[,)+β)) |
75 | 72 | simprd 497 |
. . . . . 6
β’ (π β
(β«2β(π₯
β β β¦ if(π₯
β π΄,
(absβ(ββπ΅)), 0))) β β) |
76 | | eqid 2738 |
. . . . . . . 8
β’ (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) = (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) |
77 | 70 | simprd 497 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ (ββπ΅)) β
πΏ1) |
78 | 6, 3, 76, 77, 42 | iblabslem 25114 |
. . . . . . 7
β’ (π β ((π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) β MblFn β§
(β«2β(π₯
β β β¦ if(π₯
β π΄,
(absβ(ββπ΅)), 0))) β β)) |
79 | 78 | simpld 496 |
. . . . . 6
β’ (π β (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) β
MblFn) |
80 | 49 | fmpttd 7058 |
. . . . . 6
β’ (π β (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)),
0)):ββΆ(0[,)+β)) |
81 | 78 | simprd 497 |
. . . . . 6
β’ (π β
(β«2β(π₯
β β β¦ if(π₯
β π΄,
(absβ(ββπ΅)), 0))) β β) |
82 | 73, 74, 75, 79, 80, 81 | itg2add 25046 |
. . . . 5
β’ (π β
(β«2β((π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)) βf + (π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)))) =
((β«2β(π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0))) + (β«2β(π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0))))) |
83 | 67, 82 | eqtrd 2778 |
. . . 4
β’ (π β
(β«2β(π₯
β β β¦ if(π₯
β π΄,
((absβ(ββπ΅)) + (absβ(ββπ΅))), 0))) =
((β«2β(π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0))) + (β«2β(π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0))))) |
84 | 75, 81 | readdcld 11118 |
. . . 4
β’ (π β
((β«2β(π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0))) + (β«2β(π₯ β β β¦ if(π₯ β π΄, (absβ(ββπ΅)), 0)))) β
β) |
85 | 83, 84 | eqeltrd 2839 |
. . 3
β’ (π β
(β«2β(π₯
β β β¦ if(π₯
β π΄,
((absβ(ββπ΅)) + (absβ(ββπ΅))), 0))) β
β) |
86 | 34, 44 | readdcld 11118 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β ((absβ(ββπ΅)) +
(absβ(ββπ΅))) β β) |
87 | 86 | rexrd 11139 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β ((absβ(ββπ΅)) +
(absβ(ββπ΅))) β
β*) |
88 | 34, 44, 35, 45 | addge0d 11665 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β 0 β€
((absβ(ββπ΅)) + (absβ(ββπ΅)))) |
89 | | elxrge0 13303 |
. . . . . . . 8
β’
(((absβ(ββπ΅)) + (absβ(ββπ΅))) β (0[,]+β) β
(((absβ(ββπ΅)) + (absβ(ββπ΅))) β β*
β§ 0 β€ ((absβ(ββπ΅)) + (absβ(ββπ΅))))) |
90 | 87, 88, 89 | sylanbrc 584 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β ((absβ(ββπ΅)) +
(absβ(ββπ΅))) β (0[,]+β)) |
91 | 90, 26 | ifclda 4520 |
. . . . . 6
β’ (π β if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0) β
(0[,]+β)) |
92 | 91 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β β) β if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0) β
(0[,]+β)) |
93 | 92 | fmpttd 7058 |
. . . 4
β’ (π β (π₯ β β β¦ if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))),
0)):ββΆ(0[,]+β)) |
94 | | ax-icn 11044 |
. . . . . . . . . . . 12
β’ i β
β |
95 | | mulcl 11069 |
. . . . . . . . . . . 12
β’ ((i
β β β§ (ββπ΅) β β) β (i Β·
(ββπ΅)) β
β) |
96 | 94, 43, 95 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (i Β· (ββπ΅)) β
β) |
97 | 33, 96 | abstrid 15276 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (absβ((ββπ΅) + (i Β·
(ββπ΅)))) β€
((absβ(ββπ΅)) + (absβ(i Β·
(ββπ΅))))) |
98 | 7 | replimd 15016 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β π΅ = ((ββπ΅) + (i Β· (ββπ΅)))) |
99 | 98 | fveq2d 6842 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (absβπ΅) = (absβ((ββπ΅) + (i Β·
(ββπ΅))))) |
100 | | absmul 15114 |
. . . . . . . . . . . . 13
β’ ((i
β β β§ (ββπ΅) β β) β (absβ(i
Β· (ββπ΅))) = ((absβi) Β·
(absβ(ββπ΅)))) |
101 | 94, 43, 100 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (absβ(i Β·
(ββπ΅))) =
((absβi) Β· (absβ(ββπ΅)))) |
102 | | absi 15106 |
. . . . . . . . . . . . . 14
β’
(absβi) = 1 |
103 | 102 | oveq1i 7360 |
. . . . . . . . . . . . 13
β’
((absβi) Β· (absβ(ββπ΅))) = (1 Β·
(absβ(ββπ΅))) |
104 | 44 | recnd 11117 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π΄) β (absβ(ββπ΅)) β
β) |
105 | 104 | mulid2d 11107 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β (1 Β·
(absβ(ββπ΅))) = (absβ(ββπ΅))) |
106 | 103, 105 | eqtrid 2790 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β ((absβi) Β·
(absβ(ββπ΅))) = (absβ(ββπ΅))) |
107 | 101, 106 | eqtr2d 2779 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (absβ(ββπ΅)) = (absβ(i Β·
(ββπ΅)))) |
108 | 107 | oveq2d 7366 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β ((absβ(ββπ΅)) +
(absβ(ββπ΅))) = ((absβ(ββπ΅)) + (absβ(i Β·
(ββπ΅))))) |
109 | 97, 99, 108 | 3brtr4d 5136 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (absβπ΅) β€ ((absβ(ββπ΅)) +
(absβ(ββπ΅)))) |
110 | | iftrue 4491 |
. . . . . . . . . 10
β’ (π₯ β π΄ β if(π₯ β π΄, (absβπ΅), 0) = (absβπ΅)) |
111 | 110 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β if(π₯ β π΄, (absβπ΅), 0) = (absβπ΅)) |
112 | 56 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0) = ((absβ(ββπ΅)) +
(absβ(ββπ΅)))) |
113 | 109, 111,
112 | 3brtr4d 5136 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β if(π₯ β π΄, (absβπ΅), 0) β€ if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0)) |
114 | 113 | ex 414 |
. . . . . . 7
β’ (π β (π₯ β π΄ β if(π₯ β π΄, (absβπ΅), 0) β€ if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0))) |
115 | | 0le0 12188 |
. . . . . . . . 9
β’ 0 β€
0 |
116 | 115 | a1i 11 |
. . . . . . . 8
β’ (Β¬
π₯ β π΄ β 0 β€ 0) |
117 | | iffalse 4494 |
. . . . . . . 8
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, (absβπ΅), 0) = 0) |
118 | 116, 117,
62 | 3brtr4d 5136 |
. . . . . . 7
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, (absβπ΅), 0) β€ if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0)) |
119 | 114, 118 | pm2.61d1 180 |
. . . . . 6
β’ (π β if(π₯ β π΄, (absβπ΅), 0) β€ if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0)) |
120 | 119 | ralrimivw 3146 |
. . . . 5
β’ (π β βπ₯ β β if(π₯ β π΄, (absβπ΅), 0) β€ if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0)) |
121 | | eqidd 2739 |
. . . . . 6
β’ (π β (π₯ β β β¦ if(π₯ β π΄, (absβπ΅), 0)) = (π₯ β β β¦ if(π₯ β π΄, (absβπ΅), 0))) |
122 | | eqidd 2739 |
. . . . . 6
β’ (π β (π₯ β β β¦ if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0)) = (π₯ β β β¦ if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0))) |
123 | 31, 28, 92, 121, 122 | ofrfval2 7629 |
. . . . 5
β’ (π β ((π₯ β β β¦ if(π₯ β π΄, (absβπ΅), 0)) βr β€ (π₯ β β β¦ if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0)) β βπ₯ β β if(π₯ β π΄, (absβπ΅), 0) β€ if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0))) |
124 | 120, 123 | mpbird 257 |
. . . 4
β’ (π β (π₯ β β β¦ if(π₯ β π΄, (absβπ΅), 0)) βr β€ (π₯ β β β¦ if(π₯ β π΄, ((absβ(ββπ΅)) +
(absβ(ββπ΅))), 0))) |
125 | | 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)))) |
126 | 29, 93, 124, 125 | syl3anc 1372 |
. . 3
β’ (π β
(β«2β(π₯
β β β¦ if(π₯
β π΄, (absβπ΅), 0))) β€
(β«2β(π₯
β β β¦ if(π₯
β π΄,
((absβ(ββπ΅)) + (absβ(ββπ΅))), 0)))) |
127 | | 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))) β
β) |
128 | 29, 85, 126, 127 | syl3anc 1372 |
. 2
β’ (π β
(β«2β(π₯
β β β¦ if(π₯
β π΄, (absβπ΅), 0))) β
β) |
129 | 20, 22 | iblpos 25079 |
. 2
β’ (π β ((π₯ β π΄ β¦ (absβπ΅)) β πΏ1 β
((π₯ β π΄ β¦ (absβπ΅)) β MblFn β§
(β«2β(π₯
β β β¦ if(π₯
β π΄, (absβπ΅), 0))) β
β))) |
130 | 19, 128, 129 | mpbir2and 712 |
1
β’ (π β (π₯ β π΄ β¦ (absβπ΅)) β
πΏ1) |