Step | Hyp | Ref
| Expression |
1 | | iftrue 4491 |
. . . . . . . . 9
β’ (π‘ β β β if(π‘ β β,
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))), 0) =
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
2 | 1 | mpteq2ia 5207 |
. . . . . . . 8
β’ (π‘ β β β¦ if(π‘ β β,
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))), 0)) = (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
3 | 2 | fveq2i 6841 |
. . . . . . 7
β’
(β«2β(π‘ β β β¦ if(π‘ β β,
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))), 0))) =
(β«2β(π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) |
4 | | ftc1anc.f |
. . . . . . . . . . . . . 14
β’ (π β πΉ:π·βΆβ) |
5 | 4 | ffvelcdmda 7030 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β π·) β (πΉβπ‘) β β) |
6 | | 0cnd 11082 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ π‘ β π·) β 0 β β) |
7 | 5, 6 | ifclda 4520 |
. . . . . . . . . . . 12
β’ (π β if(π‘ β π·, (πΉβπ‘), 0) β β) |
8 | 7 | recld 15013 |
. . . . . . . . . . 11
β’ (π β (ββif(π‘ β π·, (πΉβπ‘), 0)) β β) |
9 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π‘ β β) β
(ββif(π‘ β
π·, (πΉβπ‘), 0)) β β) |
10 | | ftc1anc.d |
. . . . . . . . . . 11
β’ (π β π· β β) |
11 | | rembl 24826 |
. . . . . . . . . . . 12
β’ β
β dom vol |
12 | 11 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β dom
vol) |
13 | 8 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π·) β (ββif(π‘ β π·, (πΉβπ‘), 0)) β β) |
14 | | eldifn 4086 |
. . . . . . . . . . . . 13
β’ (π‘ β (β β π·) β Β¬ π‘ β π·) |
15 | 14 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β (β β π·)) β Β¬ π‘ β π·) |
16 | | iffalse 4494 |
. . . . . . . . . . . . . 14
β’ (Β¬
π‘ β π· β if(π‘ β π·, (πΉβπ‘), 0) = 0) |
17 | 16 | fveq2d 6842 |
. . . . . . . . . . . . 13
β’ (Β¬
π‘ β π· β (ββif(π‘ β π·, (πΉβπ‘), 0)) = (ββ0)) |
18 | | re0 14971 |
. . . . . . . . . . . . 13
β’
(ββ0) = 0 |
19 | 17, 18 | eqtrdi 2794 |
. . . . . . . . . . . 12
β’ (Β¬
π‘ β π· β (ββif(π‘ β π·, (πΉβπ‘), 0)) = 0) |
20 | 15, 19 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β (β β π·)) β (ββif(π‘ β π·, (πΉβπ‘), 0)) = 0) |
21 | | iftrue 4491 |
. . . . . . . . . . . . . 14
β’ (π‘ β π· β if(π‘ β π·, (πΉβπ‘), 0) = (πΉβπ‘)) |
22 | 21 | fveq2d 6842 |
. . . . . . . . . . . . 13
β’ (π‘ β π· β (ββif(π‘ β π·, (πΉβπ‘), 0)) = (ββ(πΉβπ‘))) |
23 | 22 | mpteq2ia 5207 |
. . . . . . . . . . . 12
β’ (π‘ β π· β¦ (ββif(π‘ β π·, (πΉβπ‘), 0))) = (π‘ β π· β¦ (ββ(πΉβπ‘))) |
24 | 4 | feqmptd 6906 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ = (π‘ β π· β¦ (πΉβπ‘))) |
25 | | ftc1anc.i |
. . . . . . . . . . . . . . 15
β’ (π β πΉ β
πΏ1) |
26 | 24, 25 | eqeltrrd 2840 |
. . . . . . . . . . . . . 14
β’ (π β (π‘ β π· β¦ (πΉβπ‘)) β
πΏ1) |
27 | 5 | iblcn 25085 |
. . . . . . . . . . . . . 14
β’ (π β ((π‘ β π· β¦ (πΉβπ‘)) β πΏ1 β
((π‘ β π· β¦ (ββ(πΉβπ‘))) β πΏ1 β§ (π‘ β π· β¦ (ββ(πΉβπ‘))) β
πΏ1))) |
28 | 26, 27 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (π β ((π‘ β π· β¦ (ββ(πΉβπ‘))) β πΏ1 β§ (π‘ β π· β¦ (ββ(πΉβπ‘))) β
πΏ1)) |
29 | 28 | simpld 496 |
. . . . . . . . . . . 12
β’ (π β (π‘ β π· β¦ (ββ(πΉβπ‘))) β
πΏ1) |
30 | 23, 29 | eqeltrid 2843 |
. . . . . . . . . . 11
β’ (π β (π‘ β π· β¦ (ββif(π‘ β π·, (πΉβπ‘), 0))) β
πΏ1) |
31 | 10, 12, 13, 20, 30 | iblss2 25092 |
. . . . . . . . . 10
β’ (π β (π‘ β β β¦
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β
πΏ1) |
32 | 8 | recnd 11117 |
. . . . . . . . . . . . 13
β’ (π β (ββif(π‘ β π·, (πΉβπ‘), 0)) β β) |
33 | 32 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β β) β
(ββif(π‘ β
π·, (πΉβπ‘), 0)) β β) |
34 | | eqidd 2739 |
. . . . . . . . . . . 12
β’ (π β (π‘ β β β¦
(ββif(π‘ β
π·, (πΉβπ‘), 0))) = (π‘ β β β¦
(ββif(π‘ β
π·, (πΉβπ‘), 0)))) |
35 | | absf 15157 |
. . . . . . . . . . . . . 14
β’
abs:ββΆβ |
36 | 35 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β
abs:ββΆβ) |
37 | 36 | feqmptd 6906 |
. . . . . . . . . . . 12
β’ (π β abs = (π₯ β β β¦ (absβπ₯))) |
38 | | fveq2 6838 |
. . . . . . . . . . . 12
β’ (π₯ = (ββif(π‘ β π·, (πΉβπ‘), 0)) β (absβπ₯) = (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
39 | 33, 34, 37, 38 | fmptco 7070 |
. . . . . . . . . . 11
β’ (π β (abs β (π‘ β β β¦
(ββif(π‘ β
π·, (πΉβπ‘), 0)))) = (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) |
40 | 9 | fmpttd 7058 |
. . . . . . . . . . . 12
β’ (π β (π‘ β β β¦
(ββif(π‘ β
π·, (πΉβπ‘),
0))):ββΆβ) |
41 | | iblmbf 25054 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β πΏ1
β πΉ β
MblFn) |
42 | 25, 41 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ β MblFn) |
43 | 24, 42 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . 16
β’ (π β (π‘ β π· β¦ (πΉβπ‘)) β MblFn) |
44 | 5 | ismbfcn2 24924 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π‘ β π· β¦ (πΉβπ‘)) β MblFn β ((π‘ β π· β¦ (ββ(πΉβπ‘))) β MblFn β§ (π‘ β π· β¦ (ββ(πΉβπ‘))) β MblFn))) |
45 | 43, 44 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (π β ((π‘ β π· β¦ (ββ(πΉβπ‘))) β MblFn β§ (π‘ β π· β¦ (ββ(πΉβπ‘))) β MblFn)) |
46 | 45 | simpld 496 |
. . . . . . . . . . . . . 14
β’ (π β (π‘ β π· β¦ (ββ(πΉβπ‘))) β MblFn) |
47 | 23, 46 | eqeltrid 2843 |
. . . . . . . . . . . . 13
β’ (π β (π‘ β π· β¦ (ββif(π‘ β π·, (πΉβπ‘), 0))) β MblFn) |
48 | 10, 12, 13, 20, 47 | mbfss 24932 |
. . . . . . . . . . . 12
β’ (π β (π‘ β β β¦
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β MblFn) |
49 | | ftc1anclem1 36037 |
. . . . . . . . . . . 12
β’ (((π‘ β β β¦
(ββif(π‘ β
π·, (πΉβπ‘), 0))):ββΆβ β§ (π‘ β β β¦
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β MblFn) β (abs β
(π‘ β β β¦
(ββif(π‘ β
π·, (πΉβπ‘), 0)))) β MblFn) |
50 | 40, 48, 49 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (abs β (π‘ β β β¦
(ββif(π‘ β
π·, (πΉβπ‘), 0)))) β MblFn) |
51 | 39, 50 | eqeltrrd 2840 |
. . . . . . . . . 10
β’ (π β (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β MblFn) |
52 | 9, 31, 51 | iblabsnc 36028 |
. . . . . . . . 9
β’ (π β (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β
πΏ1) |
53 | 32 | abscld 15256 |
. . . . . . . . . . 11
β’ (π β
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β β) |
54 | 53 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π‘ β β) β
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β β) |
55 | 32 | absge0d 15264 |
. . . . . . . . . . 11
β’ (π β 0 β€
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
56 | 55 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π‘ β β) β 0 β€
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
57 | 54, 56 | iblpos 25079 |
. . . . . . . . 9
β’ (π β ((π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β πΏ1 β
((π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β MblFn β§
(β«2β(π‘
β β β¦ if(π‘
β β, (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))), 0))) β
β))) |
58 | 52, 57 | mpbid 231 |
. . . . . . . 8
β’ (π β ((π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β MblFn β§
(β«2β(π‘
β β β¦ if(π‘
β β, (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))), 0))) β
β)) |
59 | 58 | simprd 497 |
. . . . . . 7
β’ (π β
(β«2β(π‘
β β β¦ if(π‘
β β, (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))), 0))) β
β) |
60 | 3, 59 | eqeltrrid 2844 |
. . . . . 6
β’ (π β
(β«2β(π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β β) |
61 | | ltsubrp 12880 |
. . . . . 6
β’
(((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β β β§ π β β+)
β ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))))) |
62 | 60, 61 | sylan 581 |
. . . . 5
β’ ((π β§ π β β+) β
((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))))) |
63 | | rpre 12852 |
. . . . . . 7
β’ (π β β+
β π β
β) |
64 | | resubcl 11399 |
. . . . . . 7
β’
(((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β β β§ π β β) β
((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) β β) |
65 | 60, 63, 64 | syl2an 597 |
. . . . . 6
β’ ((π β§ π β β+) β
((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) β β) |
66 | 60 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β+) β
(β«2β(π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β β) |
67 | 65, 66 | ltnled 11236 |
. . . . 5
β’ ((π β§ π β β+) β
(((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β Β¬
(β«2β(π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β€
((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π))) |
68 | 62, 67 | mpbid 231 |
. . . 4
β’ ((π β§ π β β+) β Β¬
(β«2β(π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β€
((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π)) |
69 | 53 | rexrd 11139 |
. . . . . . . . 9
β’ (π β
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β
β*) |
70 | | elxrge0 13303 |
. . . . . . . . 9
β’
((absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β (0[,]+β) β
((absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β β* β§ 0
β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) |
71 | 69, 55, 70 | sylanbrc 584 |
. . . . . . . 8
β’ (π β
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β
(0[,]+β)) |
72 | 71 | adantr 482 |
. . . . . . 7
β’ ((π β§ π‘ β β) β
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β
(0[,]+β)) |
73 | 72 | fmpttd 7058 |
. . . . . 6
β’ (π β (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘),
0)))):ββΆ(0[,]+β)) |
74 | 73 | adantr 482 |
. . . . 5
β’ ((π β§ π β β+) β (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘),
0)))):ββΆ(0[,]+β)) |
75 | 65 | rexrd 11139 |
. . . . 5
β’ ((π β§ π β β+) β
((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) β
β*) |
76 | | itg2leub 25021 |
. . . . 5
β’ (((π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))):ββΆ(0[,]+β) β§
((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) β β*) β
((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β€
((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) β βπ β dom β«1(π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π)))) |
77 | 74, 75, 76 | syl2anc 585 |
. . . 4
β’ ((π β§ π β β+) β
((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β€
((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) β βπ β dom β«1(π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π)))) |
78 | 68, 77 | mtbid 324 |
. . 3
β’ ((π β§ π β β+) β Β¬
βπ β dom
β«1(π
βr β€ (π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π))) |
79 | | rexanali 3104 |
. . 3
β’
(βπ β dom
β«1(π
βr β€ (π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π)) β Β¬ βπ β dom β«1(π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π))) |
80 | 78, 79 | sylibr 233 |
. 2
β’ ((π β§ π β β+) β
βπ β dom
β«1(π
βr β€ (π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π))) |
81 | 65 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π β§ π β β+) β§ π β dom β«1)
β§ Β¬ (β«1βπ) β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π)) β ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) β β) |
82 | | itg1cl 24971 |
. . . . . . . . 9
β’ (π β dom β«1
β (β«1βπ) β β) |
83 | 82 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π β§ π β β+) β§ π β dom β«1)
β§ Β¬ (β«1βπ) β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π)) β (β«1βπ) β
β) |
84 | | eqid 2738 |
. . . . . . . . . . . 12
β’ (π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) = (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)) |
85 | 84 | i1fpos 24993 |
. . . . . . . . . . 11
β’ (π β dom β«1
β (π‘ β β
β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)) β dom
β«1) |
86 | | 0re 11091 |
. . . . . . . . . . . . . 14
β’ 0 β
β |
87 | | i1ff 24962 |
. . . . . . . . . . . . . . 15
β’ (π β dom β«1
β π:ββΆβ) |
88 | 87 | ffvelcdmda 7030 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β
β) |
89 | | max1 13033 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ (πβπ‘) β β) β 0 β€ if(0 β€
(πβπ‘), (πβπ‘), 0)) |
90 | 86, 88, 89 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π β dom β«1
β§ π‘ β β)
β 0 β€ if(0 β€ (πβπ‘), (πβπ‘), 0)) |
91 | 90 | ralrimiva 3142 |
. . . . . . . . . . . 12
β’ (π β dom β«1
β βπ‘ β
β 0 β€ if(0 β€ (πβπ‘), (πβπ‘), 0)) |
92 | | ax-resscn 11042 |
. . . . . . . . . . . . . . 15
β’ β
β β |
93 | 92 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β dom β«1
β β β β) |
94 | | fvex 6851 |
. . . . . . . . . . . . . . . . 17
β’ (πβπ‘) β V |
95 | | c0ex 11083 |
. . . . . . . . . . . . . . . . 17
β’ 0 β
V |
96 | 94, 95 | ifex 4535 |
. . . . . . . . . . . . . . . 16
β’ if(0 β€
(πβπ‘), (πβπ‘), 0) β V |
97 | 96, 84 | fnmpti 6640 |
. . . . . . . . . . . . . . 15
β’ (π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) Fn β |
98 | 97 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β dom β«1
β (π‘ β β
β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)) Fn β) |
99 | 93, 98 | 0pledm 24959 |
. . . . . . . . . . . . 13
β’ (π β dom β«1
β (0π βr β€ (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)) β (β Γ {0})
βr β€ (π‘
β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)))) |
100 | | reex 11076 |
. . . . . . . . . . . . . . 15
β’ β
β V |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β dom β«1
β β β V) |
102 | 95 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π‘ β β)
β 0 β V) |
103 | | ifcl 4530 |
. . . . . . . . . . . . . . 15
β’ (((πβπ‘) β β β§ 0 β β)
β if(0 β€ (πβπ‘), (πβπ‘), 0) β β) |
104 | 88, 86, 103 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π‘ β β)
β if(0 β€ (πβπ‘), (πβπ‘), 0) β β) |
105 | | fconstmpt 5691 |
. . . . . . . . . . . . . . 15
β’ (β
Γ {0}) = (π‘ β
β β¦ 0) |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β dom β«1
β (β Γ {0}) = (π‘ β β β¦ 0)) |
107 | | eqidd 2739 |
. . . . . . . . . . . . . 14
β’ (π β dom β«1
β (π‘ β β
β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)) = (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) |
108 | 101, 102,
104, 106, 107 | ofrfval2 7629 |
. . . . . . . . . . . . 13
β’ (π β dom β«1
β ((β Γ {0}) βr β€ (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)) β βπ‘ β β 0 β€ if(0 β€ (πβπ‘), (πβπ‘), 0))) |
109 | 99, 108 | bitrd 279 |
. . . . . . . . . . . 12
β’ (π β dom β«1
β (0π βr β€ (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)) β βπ‘ β β 0 β€ if(0 β€ (πβπ‘), (πβπ‘), 0))) |
110 | 91, 109 | mpbird 257 |
. . . . . . . . . . 11
β’ (π β dom β«1
β 0π βr β€ (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) |
111 | | itg2itg1 25023 |
. . . . . . . . . . 11
β’ (((π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) β dom β«1 β§
0π βr β€ (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) β
(β«2β(π‘
β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) = (β«1β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)))) |
112 | 85, 110, 111 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β dom β«1
β (β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) = (β«1β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)))) |
113 | | itg1cl 24971 |
. . . . . . . . . . 11
β’ ((π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) β dom β«1 β
(β«1β(π‘
β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) β β) |
114 | 85, 113 | syl 17 |
. . . . . . . . . 10
β’ (π β dom β«1
β (β«1β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) β β) |
115 | 112, 114 | eqeltrd 2839 |
. . . . . . . . 9
β’ (π β dom β«1
β (β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) β β) |
116 | 115 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π β§ π β β+) β§ π β dom β«1)
β§ Β¬ (β«1βπ) β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π)) β (β«2β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0))) β β) |
117 | | ltnle 11168 |
. . . . . . . . . 10
β’
((((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) β β β§
(β«1βπ)
β β) β (((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«1βπ) β Β¬
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π))) |
118 | 65, 82, 117 | syl2an 597 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ π β dom β«1)
β (((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«1βπ) β Β¬
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π))) |
119 | 118 | biimpar 479 |
. . . . . . . 8
β’ ((((π β§ π β β+) β§ π β dom β«1)
β§ Β¬ (β«1βπ) β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π)) β ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«1βπ)) |
120 | | max2 13035 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ (πβπ‘) β β) β (πβπ‘) β€ if(0 β€ (πβπ‘), (πβπ‘), 0)) |
121 | 86, 88, 120 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β€ if(0 β€ (πβπ‘), (πβπ‘), 0)) |
122 | 121 | ralrimiva 3142 |
. . . . . . . . . . . 12
β’ (π β dom β«1
β βπ‘ β
β (πβπ‘) β€ if(0 β€ (πβπ‘), (πβπ‘), 0)) |
123 | 87 | feqmptd 6906 |
. . . . . . . . . . . . 13
β’ (π β dom β«1
β π = (π‘ β β β¦ (πβπ‘))) |
124 | 101, 88, 104, 123, 107 | ofrfval2 7629 |
. . . . . . . . . . . 12
β’ (π β dom β«1
β (π
βr β€ (π‘
β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)) β βπ‘ β β (πβπ‘) β€ if(0 β€ (πβπ‘), (πβπ‘), 0))) |
125 | 122, 124 | mpbird 257 |
. . . . . . . . . . 11
β’ (π β dom β«1
β π
βr β€ (π‘
β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) |
126 | | itg1le 25000 |
. . . . . . . . . . 11
β’ ((π β dom β«1
β§ (π‘ β β
β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)) β dom β«1 β§
π βr β€
(π‘ β β β¦
if(0 β€ (πβπ‘), (πβπ‘), 0))) β (β«1βπ) β€
(β«1β(π‘
β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)))) |
127 | 85, 125, 126 | mpd3an23 1464 |
. . . . . . . . . 10
β’ (π β dom β«1
β (β«1βπ) β€ (β«1β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)))) |
128 | 127, 112 | breqtrrd 5132 |
. . . . . . . . 9
β’ (π β dom β«1
β (β«1βπ) β€ (β«2β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)))) |
129 | 128 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π β§ π β β+) β§ π β dom β«1)
β§ Β¬ (β«1βπ) β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π)) β (β«1βπ) β€
(β«2β(π‘
β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)))) |
130 | 81, 83, 116, 119, 129 | ltletrd 11249 |
. . . . . . 7
β’ ((((π β§ π β β+) β§ π β dom β«1)
β§ Β¬ (β«1βπ) β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π)) β ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«2β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)))) |
131 | 130 | adantrl 715 |
. . . . . 6
β’ ((((π β§ π β β+) β§ π β dom β«1)
β§ (π
βr β€ (π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π))) β ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«2β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)))) |
132 | | i1fmbf 24961 |
. . . . . . . . . . . . . . . 16
β’ ((π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) β dom β«1 β
(π‘ β β β¦
if(0 β€ (πβπ‘), (πβπ‘), 0)) β MblFn) |
133 | 85, 132 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β dom β«1
β (π‘ β β
β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)) β MblFn) |
134 | 133 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β dom β«1) β (π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) β MblFn) |
135 | | elrege0 13300 |
. . . . . . . . . . . . . . . . 17
β’ (if(0
β€ (πβπ‘), (πβπ‘), 0) β (0[,)+β) β (if(0 β€
(πβπ‘), (πβπ‘), 0) β β β§ 0 β€ if(0 β€
(πβπ‘), (πβπ‘), 0))) |
136 | 104, 90, 135 | sylanbrc 584 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π‘ β β)
β if(0 β€ (πβπ‘), (πβπ‘), 0) β (0[,)+β)) |
137 | 136 | fmpttd 7058 |
. . . . . . . . . . . . . . 15
β’ (π β dom β«1
β (π‘ β β
β¦ if(0 β€ (πβπ‘), (πβπ‘),
0)):ββΆ(0[,)+β)) |
138 | 137 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β dom β«1) β (π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘),
0)):ββΆ(0[,)+β)) |
139 | 115 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β dom β«1) β
(β«2β(π‘
β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) β β) |
140 | 104 | recnd 11117 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β dom β«1
β§ π‘ β β)
β if(0 β€ (πβπ‘), (πβπ‘), 0) β β) |
141 | 140 | negcld 11433 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β dom β«1
β§ π‘ β β)
β -if(0 β€ (πβπ‘), (πβπ‘), 0) β β) |
142 | 140, 141 | ifcld 4531 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β dom β«1
β§ π‘ β β)
β if(0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)) β β) |
143 | | subcl 11334 |
. . . . . . . . . . . . . . . . . . 19
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)) β β) β
((ββif(π‘ β
π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))) β β) |
144 | 32, 142, 143 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β dom β«1 β§ π‘ β β)) β
((ββif(π‘ β
π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))) β β) |
145 | 144 | anassrs 469 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β dom β«1) β§ π‘ β β) β
((ββif(π‘ β
π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))) β β) |
146 | 145 | abscld 15256 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β dom β«1) β§ π‘ β β) β
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))) β β) |
147 | 145 | absge0d 15264 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β dom β«1) β§ π‘ β β) β 0 β€
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))) |
148 | | elrege0 13300 |
. . . . . . . . . . . . . . . 16
β’
((absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))) β (0[,)+β) β
((absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))) β β β§ 0 β€
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) |
149 | 146, 147,
148 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β dom β«1) β§ π‘ β β) β
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))) β
(0[,)+β)) |
150 | 149 | fmpttd 7058 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β dom β«1) β (π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘),
0))))):ββΆ(0[,)+β)) |
151 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π‘ β (π₯ β π· β π‘ β π·)) |
152 | | fveq2 6838 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π‘ β (πΉβπ₯) = (πΉβπ‘)) |
153 | 151, 152 | ifbieq1d 4509 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π‘ β if(π₯ β π·, (πΉβπ₯), 0) = if(π‘ β π·, (πΉβπ‘), 0)) |
154 | 153 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π‘ β (ββif(π₯ β π·, (πΉβπ₯), 0)) = (ββif(π‘ β π·, (πΉβπ‘), 0))) |
155 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0))) = (π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0))) |
156 | | fvex 6851 |
. . . . . . . . . . . . . . . . . . . 20
β’
(ββif(π‘
β π·, (πΉβπ‘), 0)) β V |
157 | 154, 155,
156 | fvmpt 6944 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ β β β ((π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0)))βπ‘) = (ββif(π‘ β π·, (πΉβπ‘), 0))) |
158 | 154 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π‘ β (0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)) β 0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0)))) |
159 | | fveq2 6838 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π‘ β (πβπ₯) = (πβπ‘)) |
160 | 159 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π‘ β (0 β€ (πβπ₯) β 0 β€ (πβπ‘))) |
161 | 160, 159 | ifbieq1d 4509 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π‘ β if(0 β€ (πβπ₯), (πβπ₯), 0) = if(0 β€ (πβπ‘), (πβπ‘), 0)) |
162 | 161 | negeqd 11329 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π‘ β -if(0 β€ (πβπ₯), (πβπ₯), 0) = -if(0 β€ (πβπ‘), (πβπ‘), 0)) |
163 | 158, 161,
162 | ifbieq12d 4513 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π‘ β if(0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0)) = if(0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))) |
164 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β β¦ if(0
β€ (ββif(π₯
β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) = (π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) |
165 | | negex 11333 |
. . . . . . . . . . . . . . . . . . . . 21
β’ -if(0
β€ (πβπ‘), (πβπ‘), 0) β V |
166 | 96, 165 | ifex 4535 |
. . . . . . . . . . . . . . . . . . . 20
β’ if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)) β V |
167 | 163, 164,
166 | fvmpt 6944 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ β β β ((π₯ β β β¦ if(0
β€ (ββif(π₯
β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0)))βπ‘) = if(0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))) |
168 | 157, 167 | oveq12d 7368 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ β β β (((π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0)))βπ‘) β ((π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0)))βπ‘)) = ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))) |
169 | 168 | fveq2d 6842 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ β β β
(absβ(((π₯ β
β β¦ (ββif(π₯ β π·, (πΉβπ₯), 0)))βπ‘) β ((π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0)))βπ‘))) = (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))) |
170 | 169 | mpteq2ia 5207 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β β β¦
(absβ(((π₯ β
β β¦ (ββif(π₯ β π·, (πΉβπ₯), 0)))βπ‘) β ((π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0)))βπ‘)))) = (π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))) |
171 | 170 | fveq2i 6841 |
. . . . . . . . . . . . . . 15
β’
(β«2β(π‘ β β β¦ (absβ(((π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0)))βπ‘) β ((π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0)))βπ‘))))) = (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) |
172 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β
V) |
173 | | fvex 6851 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πβπ₯) β V |
174 | 173, 95 | ifex 4535 |
. . . . . . . . . . . . . . . . . . . . 21
β’ if(0 β€
(πβπ₯), (πβπ₯), 0) β V |
175 | 174, 95 | ifex 4535 |
. . . . . . . . . . . . . . . . . . . 20
β’ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), 0) β V |
176 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β β) β if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), 0) β V) |
177 | | ovex 7383 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (-1
Β· if(0 β€ (πβπ₯), (πβπ₯), 0)) β V |
178 | 95, 177 | ifex 4535 |
. . . . . . . . . . . . . . . . . . . 20
β’ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), 0, (-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0))) β V |
179 | 178 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β β) β if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), 0, (-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0))) β V) |
180 | | ffn 6664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (πΉ:π·βΆβ β πΉ Fn π·) |
181 | | frn 6671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (πΉ:π·βΆβ β ran πΉ β β) |
182 | | ref 14931 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
β:ββΆβ |
183 | | ffn 6664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(β:ββΆβ β β Fn
β) |
184 | 182, 183 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ β Fn
β |
185 | | fnco 6614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((β
Fn β β§ πΉ Fn π· β§ ran πΉ β β) β (β β
πΉ) Fn π·) |
186 | 184, 185 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΉ Fn π· β§ ran πΉ β β) β (β β
πΉ) Fn π·) |
187 | 180, 181,
186 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (πΉ:π·βΆβ β (β β πΉ) Fn π·) |
188 | | elpreima 7004 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((β
β πΉ) Fn π· β (π₯ β (β‘(β β πΉ) β (0[,)+β)) β (π₯ β π· β§ ((β β πΉ)βπ₯) β (0[,)+β)))) |
189 | 4, 187, 188 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π₯ β (β‘(β β πΉ) β (0[,)+β)) β (π₯ β π· β§ ((β β πΉ)βπ₯) β (0[,)+β)))) |
190 | | fco 6688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((β:ββΆβ β§ πΉ:π·βΆβ) β (β β
πΉ):π·βΆβ) |
191 | 182, 4, 190 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β (β β πΉ):π·βΆβ) |
192 | 191 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π₯ β π·) β ((β β πΉ)βπ₯) β β) |
193 | 192 | biantrurd 534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π₯ β π·) β (0 β€ ((β β πΉ)βπ₯) β (((β β πΉ)βπ₯) β β β§ 0 β€ ((β
β πΉ)βπ₯)))) |
194 | | elrege0 13300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((β
β πΉ)βπ₯) β (0[,)+β) β
(((β β πΉ)βπ₯) β β β§ 0 β€ ((β
β πΉ)βπ₯))) |
195 | 193, 194 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π₯ β π·) β (0 β€ ((β β πΉ)βπ₯) β ((β β πΉ)βπ₯) β (0[,)+β))) |
196 | | fvco3 6936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΉ:π·βΆβ β§ π₯ β π·) β ((β β πΉ)βπ₯) = (ββ(πΉβπ₯))) |
197 | 4, 196 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π₯ β π·) β ((β β πΉ)βπ₯) = (ββ(πΉβπ₯))) |
198 | 197 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π₯ β π·) β (0 β€ ((β β πΉ)βπ₯) β 0 β€ (ββ(πΉβπ₯)))) |
199 | 195, 198 | bitr3d 281 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π₯ β π·) β (((β β πΉ)βπ₯) β (0[,)+β) β 0 β€
(ββ(πΉβπ₯)))) |
200 | 199 | pm5.32da 580 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((π₯ β π· β§ ((β β πΉ)βπ₯) β (0[,)+β)) β (π₯ β π· β§ 0 β€ (ββ(πΉβπ₯))))) |
201 | 189, 200 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π₯ β (β‘(β β πΉ) β (0[,)+β)) β (π₯ β π· β§ 0 β€ (ββ(πΉβπ₯))))) |
202 | 201 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π₯ β β) β (π₯ β (β‘(β β πΉ) β (0[,)+β)) β (π₯ β π· β§ 0 β€ (ββ(πΉβπ₯))))) |
203 | | eldif 3919 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ β (β β π·) β (π₯ β β β§ Β¬ π₯ β π·)) |
204 | 203 | baibr 538 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ β β β (Β¬
π₯ β π· β π₯ β (β β π·))) |
205 | | 0le0 12188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 0 β€
0 |
206 | 205, 18 | breqtrri 5131 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 0 β€
(ββ0) |
207 | 206 | biantru 531 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (Β¬
π₯ β π· β (Β¬ π₯ β π· β§ 0 β€
(ββ0))) |
208 | 204, 207 | bitr3di 286 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β β β (π₯ β (β β π·) β (Β¬ π₯ β π· β§ 0 β€
(ββ0)))) |
209 | 208 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π₯ β β) β (π₯ β (β β π·) β (Β¬ π₯ β π· β§ 0 β€
(ββ0)))) |
210 | 202, 209 | orbi12d 918 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β β) β ((π₯ β (β‘(β β πΉ) β (0[,)+β)) β¨ π₯ β (β β π·)) β ((π₯ β π· β§ 0 β€ (ββ(πΉβπ₯))) β¨ (Β¬ π₯ β π· β§ 0 β€
(ββ0))))) |
211 | | elun 4107 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)) β (π₯ β (β‘(β β πΉ) β (0[,)+β)) β¨ π₯ β (β β π·))) |
212 | | fveq2 6838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (if(π₯ β π·, (πΉβπ₯), 0) = (πΉβπ₯) β (ββif(π₯ β π·, (πΉβπ₯), 0)) = (ββ(πΉβπ₯))) |
213 | 212 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (if(π₯ β π·, (πΉβπ₯), 0) = (πΉβπ₯) β (0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)) β 0 β€ (ββ(πΉβπ₯)))) |
214 | | fveq2 6838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (if(π₯ β π·, (πΉβπ₯), 0) = 0 β (ββif(π₯ β π·, (πΉβπ₯), 0)) = (ββ0)) |
215 | 214 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (if(π₯ β π·, (πΉβπ₯), 0) = 0 β (0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)) β 0 β€
(ββ0))) |
216 | 213, 215 | elimif 4522 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)) β ((π₯ β π· β§ 0 β€ (ββ(πΉβπ₯))) β¨ (Β¬ π₯ β π· β§ 0 β€
(ββ0)))) |
217 | 210, 211,
216 | 3bitr4g 314 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β β) β (π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)) β 0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)))) |
218 | 217 | ifbid 4508 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β β) β if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), if(0 β€
(πβπ₯), (πβπ₯), 0), 0) = if(0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), 0)) |
219 | 218 | mpteq2dva 5204 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π₯ β β β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), if(0 β€
(πβπ₯), (πβπ₯), 0), 0)) = (π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), 0))) |
220 | 217 | ifbid 4508 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β β) β if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), 0, (-1
Β· if(0 β€ (πβπ₯), (πβπ₯), 0))) = if(0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)), 0, (-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0)))) |
221 | 220 | mpteq2dva 5204 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π₯ β β β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), 0, (-1
Β· if(0 β€ (πβπ₯), (πβπ₯), 0)))) = (π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), 0, (-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0))))) |
222 | 172, 176,
179, 219, 221 | offval2 7628 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π₯ β β β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), if(0 β€
(πβπ₯), (πβπ₯), 0), 0)) βf + (π₯ β β β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), 0, (-1
Β· if(0 β€ (πβπ₯), (πβπ₯), 0))))) = (π₯ β β β¦ (if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), 0) + if(0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)), 0, (-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0)))))) |
223 | | ovif12 7449 |
. . . . . . . . . . . . . . . . . . . 20
β’ (if(0
β€ (ββif(π₯
β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), 0) + if(0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)), 0, (-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0)))) = if(0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)), (if(0 β€ (πβπ₯), (πβπ₯), 0) + 0), (0 + (-1 Β· if(0 β€
(πβπ₯), (πβπ₯), 0)))) |
224 | 87 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β dom β«1
β§ π₯ β β)
β (πβπ₯) β
β) |
225 | 224 | recnd 11117 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β dom β«1
β§ π₯ β β)
β (πβπ₯) β
β) |
226 | | 0cn 11081 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 0 β
β |
227 | | ifcl 4530 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πβπ₯) β β β§ 0 β β)
β if(0 β€ (πβπ₯), (πβπ₯), 0) β β) |
228 | 225, 226,
227 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β dom β«1
β§ π₯ β β)
β if(0 β€ (πβπ₯), (πβπ₯), 0) β β) |
229 | 228 | addid1d 11289 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β dom β«1
β§ π₯ β β)
β (if(0 β€ (πβπ₯), (πβπ₯), 0) + 0) = if(0 β€ (πβπ₯), (πβπ₯), 0)) |
230 | 228 | mulm1d 11541 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β dom β«1
β§ π₯ β β)
β (-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0)) = -if(0 β€ (πβπ₯), (πβπ₯), 0)) |
231 | 230 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β dom β«1
β§ π₯ β β)
β (0 + (-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0))) = (0 + -if(0 β€ (πβπ₯), (πβπ₯), 0))) |
232 | 228 | negcld 11433 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β dom β«1
β§ π₯ β β)
β -if(0 β€ (πβπ₯), (πβπ₯), 0) β β) |
233 | 232 | addid2d 11290 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β dom β«1
β§ π₯ β β)
β (0 + -if(0 β€ (πβπ₯), (πβπ₯), 0)) = -if(0 β€ (πβπ₯), (πβπ₯), 0)) |
234 | 231, 233 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β dom β«1
β§ π₯ β β)
β (0 + (-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0))) = -if(0 β€ (πβπ₯), (πβπ₯), 0)) |
235 | 229, 234 | ifeq12d 4506 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β dom β«1
β§ π₯ β β)
β if(0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)), (if(0 β€ (πβπ₯), (πβπ₯), 0) + 0), (0 + (-1 Β· if(0 β€
(πβπ₯), (πβπ₯), 0)))) = if(0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) |
236 | 223, 235 | eqtrid 2790 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β dom β«1
β§ π₯ β β)
β (if(0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), 0) + if(0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)), 0, (-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0)))) = if(0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) |
237 | 236 | mpteq2dva 5204 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom β«1
β (π₯ β β
β¦ (if(0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), 0) + if(0 β€ (ββif(π₯ β π·, (πΉβπ₯), 0)), 0, (-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0))))) = (π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0)))) |
238 | 222, 237 | sylan9eq 2798 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β dom β«1) β ((π₯ β β β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), if(0 β€
(πβπ₯), (πβπ₯), 0), 0)) βf + (π₯ β β β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), 0, (-1
Β· if(0 β€ (πβπ₯), (πβπ₯), 0))))) = (π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0)))) |
239 | | 0xr 11136 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 0 β
β* |
240 | | pnfxr 11143 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ +β
β β* |
241 | | 0ltpnf 12972 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 0 <
+β |
242 | | snunioo 13324 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((0
β β* β§ +β β β* β§ 0
< +β) β ({0} βͺ (0(,)+β)) =
(0[,)+β)) |
243 | 239, 240,
241, 242 | mp3an 1462 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ({0}
βͺ (0(,)+β)) = (0[,)+β) |
244 | 243 | imaeq2i 6008 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β‘(β β πΉ) β ({0} βͺ (0(,)+β))) =
(β‘(β β πΉ) β (0[,)+β)) |
245 | | imaundi 6099 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β‘(β β πΉ) β ({0} βͺ (0(,)+β))) =
((β‘(β β πΉ) β {0}) βͺ (β‘(β β πΉ) β (0(,)+β))) |
246 | 244, 245 | eqtr3i 2768 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β‘(β β πΉ) β (0[,)+β)) = ((β‘(β β πΉ) β {0}) βͺ (β‘(β β πΉ) β (0(,)+β))) |
247 | | ismbfcn 24915 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (πΉ:π·βΆβ β (πΉ β MblFn β ((β β πΉ) β MblFn β§ (β
β πΉ) β
MblFn))) |
248 | 4, 247 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (πΉ β MblFn β ((β β πΉ) β MblFn β§ (β
β πΉ) β
MblFn))) |
249 | 42, 248 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((β β πΉ) β MblFn β§ (β
β πΉ) β
MblFn)) |
250 | 249 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (β β πΉ) β MblFn) |
251 | | mbfimasn 24918 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((β
β πΉ) β MblFn
β§ (β β πΉ):π·βΆβ β§ 0 β β)
β (β‘(β β πΉ) β {0}) β dom
vol) |
252 | 86, 251 | mp3an3 1451 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((β
β πΉ) β MblFn
β§ (β β πΉ):π·βΆβ) β (β‘(β β πΉ) β {0}) β dom
vol) |
253 | | mbfima 24916 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((β
β πΉ) β MblFn
β§ (β β πΉ):π·βΆβ) β (β‘(β β πΉ) β (0(,)+β)) β dom
vol) |
254 | | unmbl 24823 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((β‘(β β πΉ) β {0}) β dom vol β§ (β‘(β β πΉ) β (0(,)+β)) β dom vol)
β ((β‘(β β πΉ) β {0}) βͺ (β‘(β β πΉ) β (0(,)+β))) β dom
vol) |
255 | 252, 253,
254 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((β
β πΉ) β MblFn
β§ (β β πΉ):π·βΆβ) β ((β‘(β β πΉ) β {0}) βͺ (β‘(β β πΉ) β (0(,)+β))) β dom
vol) |
256 | 250, 191,
255 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((β‘(β β πΉ) β {0}) βͺ (β‘(β β πΉ) β (0(,)+β))) β dom
vol) |
257 | 246, 256 | eqeltrid 2843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (β‘(β β πΉ) β (0[,)+β)) β dom
vol) |
258 | 4 | fdmd 6675 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β dom πΉ = π·) |
259 | | mbfdm 24912 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πΉ β MblFn β dom πΉ β dom
vol) |
260 | 42, 259 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β dom πΉ β dom vol) |
261 | 258, 260 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π· β dom vol) |
262 | | difmbl 24829 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((β
β dom vol β§ π·
β dom vol) β (β β π·) β dom vol) |
263 | 11, 261, 262 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (β β π·) β dom
vol) |
264 | | unmbl 24823 |
. . . . . . . . . . . . . . . . . . 19
β’ (((β‘(β β πΉ) β (0[,)+β)) β dom vol
β§ (β β π·)
β dom vol) β ((β‘(β
β πΉ) β
(0[,)+β)) βͺ (β β π·)) β dom vol) |
265 | 257, 263,
264 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)) β dom
vol) |
266 | | fveq2 6838 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π‘ = π₯ β (πβπ‘) = (πβπ₯)) |
267 | 266 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π‘ = π₯ β (0 β€ (πβπ‘) β 0 β€ (πβπ₯))) |
268 | 267, 266 | ifbieq1d 4509 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π‘ = π₯ β if(0 β€ (πβπ‘), (πβπ‘), 0) = if(0 β€ (πβπ₯), (πβπ₯), 0)) |
269 | 268, 84, 174 | fvmpt 6944 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ β β β ((π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0))βπ₯) = if(0 β€ (πβπ₯), (πβπ₯), 0)) |
270 | 269 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β β β if(0 β€
(πβπ₯), (πβπ₯), 0) = ((π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))βπ₯)) |
271 | 270 | ifeq1d 4504 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β β β if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), if(0 β€
(πβπ₯), (πβπ₯), 0), 0) = if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), ((π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0))βπ₯), 0)) |
272 | 271 | mpteq2ia 5207 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), if(0 β€
(πβπ₯), (πβπ₯), 0), 0)) = (π₯ β β β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), ((π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0))βπ₯), 0)) |
273 | 272 | i1fres 24992 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) β dom β«1 β§
((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)) β dom vol)
β (π₯ β β
β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), if(0 β€
(πβπ₯), (πβπ₯), 0), 0)) β dom
β«1) |
274 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) β dom β«1 β
(π‘ β β β¦
if(0 β€ (πβπ‘), (πβπ‘), 0)) β dom
β«1) |
275 | | neg1rr 12202 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ -1 β
β |
276 | 275 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) β dom β«1 β -1
β β) |
277 | 274, 276 | i1fmulc 24990 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) β dom β«1 β
((β Γ {-1}) βf Β· (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) β dom
β«1) |
278 | | cmmbl 24820 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)) β dom vol
β (β β ((β‘(β
β πΉ) β
(0[,)+β)) βͺ (β β π·))) β dom vol) |
279 | | ifnot 4537 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ if(Β¬
π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), (-1 Β·
if(0 β€ (πβπ₯), (πβπ₯), 0)), 0) = if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), 0, (-1
Β· if(0 β€ (πβπ₯), (πβπ₯), 0))) |
280 | | eldif 3919 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ β (β β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·))) β (π₯ β β β§ Β¬
π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)))) |
281 | 280 | baibr 538 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β β β (Β¬
π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)) β π₯ β (β β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·))))) |
282 | | tru 1546 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β€ |
283 | | negex 11333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ -1 β
V |
284 | 283 | fconst 6724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (β
Γ {-1}):ββΆ{-1} |
285 | | ffn 6664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((β
Γ {-1}):ββΆ{-1} β (β Γ {-1}) Fn
β) |
286 | 284, 285 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (β€
β (β Γ {-1}) Fn β) |
287 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (β€
β (π‘ β β
β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)) Fn β) |
288 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (β€
β β β V) |
289 | | inidm 4177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (β
β© β) = β |
290 | 283 | fvconst2 7148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π₯ β β β ((β
Γ {-1})βπ₯) =
-1) |
291 | 290 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((β€ β§ π₯
β β) β ((β Γ {-1})βπ₯) = -1) |
292 | 269 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((β€ β§ π₯
β β) β ((π‘
β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))βπ₯) = if(0 β€ (πβπ₯), (πβπ₯), 0)) |
293 | 286, 287,
288, 288, 289, 291, 292 | ofval 7619 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((β€ β§ π₯
β β) β (((β Γ {-1}) βf Β·
(π‘ β β β¦
if(0 β€ (πβπ‘), (πβπ‘), 0)))βπ₯) = (-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0))) |
294 | 282, 293 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ β β β
(((β Γ {-1}) βf Β· (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)))βπ₯) = (-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0))) |
295 | 294 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β β β (-1
Β· if(0 β€ (πβπ₯), (πβπ₯), 0)) = (((β Γ {-1})
βf Β· (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)))βπ₯)) |
296 | 281, 295 | ifbieq1d 4509 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ β β β if(Β¬
π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), (-1 Β·
if(0 β€ (πβπ₯), (πβπ₯), 0)), 0) = if(π₯ β (β β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·))), (((β
Γ {-1}) βf Β· (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)))βπ₯), 0)) |
297 | 279, 296 | eqtr3id 2792 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β β β if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), 0, (-1
Β· if(0 β€ (πβπ₯), (πβπ₯), 0))) = if(π₯ β (β β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·))), (((β
Γ {-1}) βf Β· (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)))βπ₯), 0)) |
298 | 297 | mpteq2ia 5207 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β β β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), 0, (-1
Β· if(0 β€ (πβπ₯), (πβπ₯), 0)))) = (π₯ β β β¦ if(π₯ β (β β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·))), (((β
Γ {-1}) βf Β· (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)))βπ₯), 0)) |
299 | 298 | i1fres 24992 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((β Γ {-1}) βf Β· (π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0))) β dom β«1 β§
(β β ((β‘(β β
πΉ) β (0[,)+β))
βͺ (β β π·)))
β dom vol) β (π₯
β β β¦ if(π₯
β ((β‘(β β πΉ) β (0[,)+β)) βͺ
(β β π·)), 0,
(-1 Β· if(0 β€ (πβπ₯), (πβπ₯), 0)))) β dom
β«1) |
300 | 277, 278,
299 | syl2an 597 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) β dom β«1 β§
((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)) β dom vol)
β (π₯ β β
β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), 0, (-1
Β· if(0 β€ (πβπ₯), (πβπ₯), 0)))) β dom
β«1) |
301 | 273, 300 | i1fadd 24981 |
. . . . . . . . . . . . . . . . . 18
β’ (((π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) β dom β«1 β§
((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)) β dom vol)
β ((π₯ β β
β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), if(0 β€
(πβπ₯), (πβπ₯), 0), 0)) βf + (π₯ β β β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), 0, (-1
Β· if(0 β€ (πβπ₯), (πβπ₯), 0))))) β dom
β«1) |
302 | 85, 265, 301 | syl2anr 598 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β dom β«1) β ((π₯ β β β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), if(0 β€
(πβπ₯), (πβπ₯), 0), 0)) βf + (π₯ β β β¦ if(π₯ β ((β‘(β β πΉ) β (0[,)+β)) βͺ (β
β π·)), 0, (-1
Β· if(0 β€ (πβπ₯), (πβπ₯), 0))))) β dom
β«1) |
303 | 238, 302 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β dom β«1) β (π₯ β β β¦ if(0
β€ (ββif(π₯
β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) β dom
β«1) |
304 | 154 | cbvmptv 5217 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0))) = (π‘ β β β¦
(ββif(π‘ β
π·, (πΉβπ‘), 0))) |
305 | 304, 31 | eqeltrid 2843 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0))) β
πΏ1) |
306 | 9, 304 | fmptd 7057 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯),
0))):ββΆβ) |
307 | 305, 306 | jca 513 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0))) β πΏ1 β§
(π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯),
0))):ββΆβ)) |
308 | 307 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β dom β«1) β ((π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0))) β πΏ1 β§
(π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯),
0))):ββΆβ)) |
309 | | ftc1anclem4 36040 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β β¦ if(0
β€ (ββif(π₯
β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) β dom β«1 β§
(π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0))) β πΏ1 β§
(π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0))):ββΆβ) β
(β«2β(π‘
β β β¦ (absβ(((π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0)))βπ‘) β ((π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0)))βπ‘))))) β β) |
310 | 309 | 3expb 1121 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β β¦ if(0
β€ (ββif(π₯
β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) β dom β«1 β§
((π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0))) β πΏ1 β§
(π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0))):ββΆβ)) β
(β«2β(π‘
β β β¦ (absβ(((π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0)))βπ‘) β ((π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0)))βπ‘))))) β β) |
311 | 303, 308,
310 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β dom β«1) β
(β«2β(π‘
β β β¦ (absβ(((π₯ β β β¦
(ββif(π₯ β
π·, (πΉβπ₯), 0)))βπ‘) β ((π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0)))βπ‘))))) β β) |
312 | 171, 311 | eqeltrrid 2844 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β dom β«1) β
(β«2β(π‘
β β β¦ (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) β β) |
313 | 134, 138,
139, 150, 312 | itg2addnc 36018 |
. . . . . . . . . . . . 13
β’ ((π β§ π β dom β«1) β
(β«2β((π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)) βf + (π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))))) =
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))))) |
314 | 100 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β dom β«1) β β
β V) |
315 | 96 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β dom β«1) β§ π‘ β β) β if(0
β€ (πβπ‘), (πβπ‘), 0) β V) |
316 | | eqidd 2739 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β dom β«1) β (π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) = (π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) |
317 | | eqidd 2739 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β dom β«1) β (π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))) = (π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) |
318 | 314, 315,
146, 316, 317 | offval2 7628 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β dom β«1) β ((π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0)) βf + (π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) = (π‘ β β β¦ (if(0 β€ (πβπ‘), (πβπ‘), 0) + (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))))) |
319 | 318 | fveq2d 6842 |
. . . . . . . . . . . . 13
β’ ((π β§ π β dom β«1) β
(β«2β((π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0)) βf + (π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))))) = (β«2β(π‘ β β β¦ (if(0
β€ (πβπ‘), (πβπ‘), 0) + (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))))) |
320 | 313, 319 | eqtr3d 2780 |
. . . . . . . . . . . 12
β’ ((π β§ π β dom β«1) β
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))))) = (β«2β(π‘ β β β¦ (if(0
β€ (πβπ‘), (πβπ‘), 0) + (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))))) |
321 | 320 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β dom β«1) β§ π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))))) = (β«2β(π‘ β β β¦ (if(0
β€ (πβπ‘), (πβπ‘), 0) + (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))))) |
322 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π‘(π β§ π β dom
β«1) |
323 | | nfcv 2906 |
. . . . . . . . . . . . . . 15
β’
β²π‘π |
324 | | nfcv 2906 |
. . . . . . . . . . . . . . 15
β’
β²π‘
βr β€ |
325 | | nfmpt1 5212 |
. . . . . . . . . . . . . . 15
β’
β²π‘(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
326 | 323, 324,
325 | nfbr 5151 |
. . . . . . . . . . . . . 14
β’
β²π‘ π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
327 | 322, 326 | nfan 1903 |
. . . . . . . . . . . . 13
β’
β²π‘((π β§ π β dom β«1) β§ π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) |
328 | | anass 470 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β dom β«1) β§ π‘ β β) β (π β§ (π β dom β«1 β§ π‘ β
β))) |
329 | 87 | ffnd 6665 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β dom β«1
β π Fn
β) |
330 | | fvex 6851 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β V |
331 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) = (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
332 | 330, 331 | fnmpti 6640 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) Fn β |
333 | 332 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β dom β«1
β (π‘ β β
β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) Fn β) |
334 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) = (πβπ‘)) |
335 | 331 | fvmpt2 6955 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π‘ β β β§
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β V) β ((π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))βπ‘) = (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
336 | 330, 335 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ β β β ((π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))βπ‘) = (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
337 | 336 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β dom β«1
β§ π‘ β β)
β ((π‘ β β
β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))βπ‘) = (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
338 | 329, 333,
101, 101, 289, 334, 337 | ofrval 7620 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β dom β«1
β§ π βr
β€ (π‘ β β
β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ π‘ β β) β (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
339 | 338 | 3com23 1127 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β dom β«1
β§ π‘ β β
β§ π βr
β€ (π‘ β β
β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
340 | 339 | 3expa 1119 |
. . . . . . . . . . . . . . . . 17
β’ (((π β dom β«1
β§ π‘ β β)
β§ π βr
β€ (π‘ β β
β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
341 | 340 | adantll 713 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π‘ β β)) β§ π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
342 | | resubcl 11399 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ if(0 β€ (πβπ‘), (πβπ‘), 0) β β) β
((ββif(π‘ β
π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0)) β β) |
343 | 8, 104, 342 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β dom β«1 β§ π‘ β β)) β
((ββif(π‘ β
π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0)) β β) |
344 | 343 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ 0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) β ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0)) β β) |
345 | | absid 15116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) = (ββif(π‘ β π·, (πΉβπ‘), 0))) |
346 | 8, 345 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) = (ββif(π‘ β π·, (πΉβπ‘), 0))) |
347 | 346 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β ((πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β (πβπ‘) β€ (ββif(π‘ β π·, (πΉβπ‘), 0)))) |
348 | 347 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β (πβπ‘) β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) |
349 | 348 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ 0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) β (πβπ‘) β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) |
350 | 349 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ 0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) β (πβπ‘) β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) |
351 | | breq1 5107 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πβπ‘) = if(0 β€ (πβπ‘), (πβπ‘), 0) β ((πβπ‘) β€ (ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0) β€ (ββif(π‘ β π·, (πΉβπ‘), 0)))) |
352 | | breq1 5107 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (0 = if(0
β€ (πβπ‘), (πβπ‘), 0) β (0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0) β€ (ββif(π‘ β π·, (πΉβπ‘), 0)))) |
353 | 351, 352 | ifboth 4524 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πβπ‘) β€ (ββif(π‘ β π·, (πΉβπ‘), 0)) β§ 0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) β if(0 β€ (πβπ‘), (πβπ‘), 0) β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) |
354 | 350, 353 | sylancom 589 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ 0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) β if(0 β€ (πβπ‘), (πβπ‘), 0) β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) |
355 | | subge0 11602 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ if(0 β€ (πβπ‘), (πβπ‘), 0) β β) β (0 β€
((ββif(π‘ β
π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0) β€ (ββif(π‘ β π·, (πΉβπ‘), 0)))) |
356 | 8, 104, 355 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β dom β«1 β§ π‘ β β)) β (0 β€
((ββif(π‘ β
π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0) β€ (ββif(π‘ β π·, (πΉβπ‘), 0)))) |
357 | 356 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ 0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) β (0 β€
((ββif(π‘ β
π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0) β€ (ββif(π‘ β π·, (πΉβπ‘), 0)))) |
358 | 354, 357 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ 0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) β 0 β€ ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
359 | 344, 358 | absidd 15242 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ 0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) β
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0))) = ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
360 | | iftrue 4491 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)) = if(0 β€ (πβπ‘), (πβπ‘), 0)) |
361 | 360 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)) β ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))) = ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
362 | 361 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)) β
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))) = (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0)))) |
363 | 362 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ 0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) β
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))) = (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0)))) |
364 | 8 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β (ββif(π‘ β π·, (πΉβπ‘), 0)) β β) |
365 | 345 | oveq1d 7365 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β
((absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β if(0 β€ (πβπ‘), (πβπ‘), 0)) = ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
366 | 364, 365 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ 0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) β
((absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β if(0 β€ (πβπ‘), (πβπ‘), 0)) = ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
367 | 359, 363,
366 | 3eqtr4d 2788 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ 0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0))) β
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))) = ((absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
368 | 104 | renegcld 11516 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β dom β«1
β§ π‘ β β)
β -if(0 β€ (πβπ‘), (πβπ‘), 0) β β) |
369 | | resubcl 11399 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ -if(0 β€ (πβπ‘), (πβπ‘), 0) β β) β
((ββif(π‘ β
π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)) β β) |
370 | 8, 368, 369 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π β dom β«1 β§ π‘ β β)) β
((ββif(π‘ β
π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)) β β) |
371 | 370 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β ((ββif(π‘ β π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)) β β) |
372 | 88 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β (πβπ‘) β β) |
373 | 8 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β (ββif(π‘ β π·, (πΉβπ‘), 0)) β β) |
374 | 8 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (π β dom β«1 β§ π‘ β β)) β
(ββif(π‘ β
π·, (πΉβπ‘), 0)) β β) |
375 | | ltnle 11168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ 0 β β)
β ((ββif(π‘
β π·, (πΉβπ‘), 0)) < 0 β Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)))) |
376 | 86, 375 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β
((ββif(π‘ β
π·, (πΉβπ‘), 0)) < 0 β Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)))) |
377 | | ltle 11177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ 0 β β)
β ((ββif(π‘
β π·, (πΉβπ‘), 0)) < 0 β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ 0)) |
378 | 86, 377 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β
((ββif(π‘ β
π·, (πΉβπ‘), 0)) < 0 β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ 0)) |
379 | 376, 378 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β (Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)) β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ 0)) |
380 | 379 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ 0) |
381 | | absnid 15118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§
(ββif(π‘ β
π·, (πΉβπ‘), 0)) β€ 0) β
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) = -(ββif(π‘ β π·, (πΉβπ‘), 0))) |
382 | 380, 381 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) = -(ββif(π‘ β π·, (πΉβπ‘), 0))) |
383 | 382 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β ((πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β (πβπ‘) β€ -(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
384 | 383 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((ββif(π‘ β π·, (πΉβπ‘), 0)) β β β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β (πβπ‘) β€ -(ββif(π‘ β π·, (πΉβπ‘), 0))) |
385 | 384 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((ββif(π‘ β π·, (πΉβπ‘), 0)) β β β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β (πβπ‘) β€ -(ββif(π‘ β π·, (πΉβπ‘), 0))) |
386 | 374, 385 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β (πβπ‘) β€ -(ββif(π‘ β π·, (πΉβπ‘), 0))) |
387 | 372, 373,
386 | lenegcon2d 11672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ -(πβπ‘)) |
388 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β π) |
389 | 86 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β 0 β
β) |
390 | 8, 389 | ltnled 11236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((ββif(π‘ β π·, (πΉβπ‘), 0)) < 0 β Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)))) |
391 | 8, 86, 377 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((ββif(π‘ β π·, (πΉβπ‘), 0)) < 0 β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ 0)) |
392 | 390, 391 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)) β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ 0)) |
393 | 392 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ 0) |
394 | 388, 393 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ 0) |
395 | | negeq 11327 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πβπ‘) = if(0 β€ (πβπ‘), (πβπ‘), 0) β -(πβπ‘) = -if(0 β€ (πβπ‘), (πβπ‘), 0)) |
396 | 395 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πβπ‘) = if(0 β€ (πβπ‘), (πβπ‘), 0) β ((ββif(π‘ β π·, (πΉβπ‘), 0)) β€ -(πβπ‘) β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ -if(0 β€ (πβπ‘), (πβπ‘), 0))) |
397 | | neg0 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ -0 =
0 |
398 | | negeq 11327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (0 = if(0
β€ (πβπ‘), (πβπ‘), 0) β -0 = -if(0 β€ (πβπ‘), (πβπ‘), 0)) |
399 | 397, 398 | eqtr3id 2792 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (0 = if(0
β€ (πβπ‘), (πβπ‘), 0) β 0 = -if(0 β€ (πβπ‘), (πβπ‘), 0)) |
400 | 399 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (0 = if(0
β€ (πβπ‘), (πβπ‘), 0) β ((ββif(π‘ β π·, (πΉβπ‘), 0)) β€ 0 β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ -if(0 β€ (πβπ‘), (πβπ‘), 0))) |
401 | 396, 400 | ifboth 4524 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β€ -(πβπ‘) β§ (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ 0) β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ -if(0 β€ (πβπ‘), (πβπ‘), 0)) |
402 | 387, 394,
401 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ -if(0 β€ (πβπ‘), (πβπ‘), 0)) |
403 | | suble0 11603 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ -if(0 β€ (πβπ‘), (πβπ‘), 0) β β) β
(((ββif(π‘ β
π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)) β€ 0 β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ -if(0 β€ (πβπ‘), (πβπ‘), 0))) |
404 | 8, 368, 403 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π β dom β«1 β§ π‘ β β)) β
(((ββif(π‘ β
π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)) β€ 0 β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ -if(0 β€ (πβπ‘), (πβπ‘), 0))) |
405 | 404 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β (((ββif(π‘ β π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)) β€ 0 β (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ -if(0 β€ (πβπ‘), (πβπ‘), 0))) |
406 | 402, 405 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β ((ββif(π‘ β π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)) β€ 0) |
407 | 371, 406 | absnidd 15233 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0))) = -((ββif(π‘ β π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0))) |
408 | | subneg 11384 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ if(0 β€ (πβπ‘), (πβπ‘), 0) β β) β
((ββif(π‘ β
π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)) = ((ββif(π‘ β π·, (πΉβπ‘), 0)) + if(0 β€ (πβπ‘), (πβπ‘), 0))) |
409 | 408 | negeqd 11329 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ if(0 β€ (πβπ‘), (πβπ‘), 0) β β) β
-((ββif(π‘ β
π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)) = -((ββif(π‘ β π·, (πΉβπ‘), 0)) + if(0 β€ (πβπ‘), (πβπ‘), 0))) |
410 | | negdi2 11393 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ if(0 β€ (πβπ‘), (πβπ‘), 0) β β) β
-((ββif(π‘ β
π·, (πΉβπ‘), 0)) + if(0 β€ (πβπ‘), (πβπ‘), 0)) = (-(ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
411 | 409, 410 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((ββif(π‘
β π·, (πΉβπ‘), 0)) β β β§ if(0 β€ (πβπ‘), (πβπ‘), 0) β β) β
-((ββif(π‘ β
π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)) = (-(ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
412 | 32, 140, 411 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β dom β«1 β§ π‘ β β)) β
-((ββif(π‘ β
π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)) = (-(ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
413 | 412 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β -((ββif(π‘ β π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)) = (-(ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
414 | 407, 413 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0))) = (-(ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
415 | | iffalse 4494 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Β¬ 0
β€ (ββif(π‘
β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)) = -if(0 β€ (πβπ‘), (πβπ‘), 0)) |
416 | 415 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (Β¬ 0
β€ (ββif(π‘
β π·, (πΉβπ‘), 0)) β ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))) = ((ββif(π‘ β π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0))) |
417 | 416 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Β¬ 0
β€ (ββif(π‘
β π·, (πΉβπ‘), 0)) β
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))) = (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)))) |
418 | 417 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))) = (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β -if(0 β€ (πβπ‘), (πβπ‘), 0)))) |
419 | 8, 381 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (ββif(π‘ β π·, (πΉβπ‘), 0)) β€ 0) β
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) = -(ββif(π‘ β π·, (πΉβπ‘), 0))) |
420 | 393, 419 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) = -(ββif(π‘ β π·, (πΉβπ‘), 0))) |
421 | 420 | oveq1d 7365 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β
((absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β if(0 β€ (πβπ‘), (πβπ‘), 0)) = (-(ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
422 | 388, 421 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β
((absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β if(0 β€ (πβπ‘), (πβπ‘), 0)) = (-(ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
423 | 414, 418,
422 | 3eqtr4d 2788 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬ 0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0))) β
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))) = ((absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
424 | 367, 423 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))) = ((absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β if(0 β€ (πβπ‘), (πβπ‘), 0))) |
425 | 424 | oveq2d 7366 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β (if(0 β€ (πβπ‘), (πβπ‘), 0) + (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))) = (if(0 β€ (πβπ‘), (πβπ‘), 0) + ((absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β if(0 β€ (πβπ‘), (πβπ‘), 0)))) |
426 | 53 | recnd 11117 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β β) |
427 | | pncan3 11343 |
. . . . . . . . . . . . . . . . . . 19
β’ ((if(0
β€ (πβπ‘), (πβπ‘), 0) β β β§
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β β) β (if(0 β€
(πβπ‘), (πβπ‘), 0) + ((absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β if(0 β€ (πβπ‘), (πβπ‘), 0))) = (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
428 | 140, 426,
427 | syl2anr 598 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β dom β«1 β§ π‘ β β)) β (if(0
β€ (πβπ‘), (πβπ‘), 0) + ((absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β if(0 β€ (πβπ‘), (πβπ‘), 0))) = (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
429 | 428 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β (if(0 β€ (πβπ‘), (πβπ‘), 0) + ((absβ(ββif(π‘ β π·, (πΉβπ‘), 0))) β if(0 β€ (πβπ‘), (πβπ‘), 0))) = (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
430 | 425, 429 | eqtrd 2778 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π‘ β β)) β§ (πβπ‘) β€ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β (if(0 β€ (πβπ‘), (πβπ‘), 0) + (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))) = (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
431 | 341, 430 | syldan 592 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β dom β«1 β§ π‘ β β)) β§ π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β (if(0 β€ (πβπ‘), (πβπ‘), 0) + (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))) = (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
432 | 328, 431 | sylanb 582 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β dom β«1) β§ π‘ β β) β§ π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β (if(0 β€ (πβπ‘), (πβπ‘), 0) + (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))) = (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
433 | 432 | an32s 651 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β dom β«1) β§ π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β§ π‘ β β) β (if(0 β€ (πβπ‘), (πβπ‘), 0) + (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))) = (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) |
434 | 327, 433 | mpteq2da 5202 |
. . . . . . . . . . . 12
β’ (((π β§ π β dom β«1) β§ π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β (π‘ β β β¦ (if(0 β€ (πβπ‘), (πβπ‘), 0) + (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) = (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) |
435 | 434 | fveq2d 6842 |
. . . . . . . . . . 11
β’ (((π β§ π β dom β«1) β§ π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β
(β«2β(π‘
β β β¦ (if(0 β€ (πβπ‘), (πβπ‘), 0) + (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))))) = (β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))))) |
436 | 321, 435 | eqtrd 2778 |
. . . . . . . . . 10
β’ (((π β§ π β dom β«1) β§ π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))))) = (β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))))) |
437 | 436 | breq1d 5114 |
. . . . . . . . 9
β’ (((π β§ π β dom β«1) β§ π βr β€ (π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β
(((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))))) <
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + π) β (β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) <
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + π))) |
438 | 437 | adantllr 718 |
. . . . . . . 8
β’ ((((π β§ π β β+) β§ π β dom β«1)
β§ π βr
β€ (π‘ β β
β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β
(((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))))) <
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + π) β (β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) <
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + π))) |
439 | 312 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ π β dom β«1)
β (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) β β) |
440 | 63 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ π β dom β«1)
β π β
β) |
441 | 115 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ π β dom β«1)
β (β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) β β) |
442 | 439, 440,
441 | ltadd2d 11245 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ π β dom β«1)
β ((β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) < π β ((β«2β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0))) + (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))))) <
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + π))) |
443 | 442 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π β β+) β§ π β dom β«1)
β§ π βr
β€ (π‘ β β
β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β
((β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) < π β ((β«2β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0))) + (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))))) <
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + π))) |
444 | | ltsubadd 11559 |
. . . . . . . . . . 11
β’
(((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β β β§ π β β β§
(β«2β(π‘
β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) β β) β
(((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«2β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0))) β
(β«2β(π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) <
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + π))) |
445 | 60, 63, 115, 444 | syl3an 1161 |
. . . . . . . . . 10
β’ ((π β§ π β β+ β§ π β dom β«1)
β (((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«2β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0))) β
(β«2β(π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) <
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + π))) |
446 | 445 | 3expa 1119 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ π β dom β«1)
β (((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«2β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0))) β
(β«2β(π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) <
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + π))) |
447 | 446 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π β β+) β§ π β dom β«1)
β§ π βr
β€ (π‘ β β
β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β
(((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«2β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0))) β
(β«2β(π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) <
((β«2β(π‘ β β β¦ if(0 β€ (πβπ‘), (πβπ‘), 0))) + π))) |
448 | 438, 443,
447 | 3bitr4d 311 |
. . . . . . 7
β’ ((((π β§ π β β+) β§ π β dom β«1)
β§ π βr
β€ (π‘ β β
β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β
((β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) < π β ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«2β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0))))) |
449 | 448 | adantrr 716 |
. . . . . 6
β’ ((((π β§ π β β+) β§ π β dom β«1)
β§ (π
βr β€ (π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π))) β ((β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) < π β ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π) < (β«2β(π‘ β β β¦ if(0
β€ (πβπ‘), (πβπ‘), 0))))) |
450 | 131, 449 | mpbird 257 |
. . . . 5
β’ ((((π β§ π β β+) β§ π β dom β«1)
β§ (π
βr β€ (π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π))) β (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) < π) |
451 | 450 | ex 414 |
. . . 4
β’ (((π β§ π β β+) β§ π β dom β«1)
β ((π
βr β€ (π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π)) β (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) < π)) |
452 | 451 | reximdva 3164 |
. . 3
β’ ((π β§ π β β+) β
(βπ β dom
β«1(π
βr β€ (π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π)) β βπ β dom
β«1(β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) < π)) |
453 | | fveq1 6837 |
. . . . . . . . . . . . . 14
β’ (π = (π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) β (πβπ‘) = ((π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0)))βπ‘)) |
454 | 453, 167 | sylan9eq 2798 |
. . . . . . . . . . . . 13
β’ ((π = (π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) β§ π‘ β β) β (πβπ‘) = if(0 β€ (ββif(π‘ β π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))) |
455 | 454 | oveq2d 7366 |
. . . . . . . . . . . 12
β’ ((π = (π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) β§ π‘ β β) β
((ββif(π‘ β
π·, (πΉβπ‘), 0)) β (πβπ‘)) = ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))) |
456 | 455 | fveq2d 6842 |
. . . . . . . . . . 11
β’ ((π = (π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) β§ π‘ β β) β
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β (πβπ‘))) = (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))) |
457 | 456 | mpteq2dva 5204 |
. . . . . . . . . 10
β’ (π = (π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) β (π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β (πβπ‘)))) = (π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) |
458 | 457 | fveq2d 6842 |
. . . . . . . . 9
β’ (π = (π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) β
(β«2β(π‘
β β β¦ (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β (πβπ‘))))) = (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0))))))) |
459 | 458 | breq1d 5114 |
. . . . . . . 8
β’ (π = (π₯ β β β¦ if(0 β€
(ββif(π₯ β
π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) β
((β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β (πβπ‘))))) < π β (β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) < π)) |
460 | 459 | rspcev 3580 |
. . . . . . 7
β’ (((π₯ β β β¦ if(0
β€ (ββif(π₯
β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) β dom β«1 β§
(β«2β(π‘
β β β¦ (absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) < π) β βπ β dom
β«1(β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β (πβπ‘))))) < π) |
461 | 460 | ex 414 |
. . . . . 6
β’ ((π₯ β β β¦ if(0
β€ (ββif(π₯
β π·, (πΉβπ₯), 0)), if(0 β€ (πβπ₯), (πβπ₯), 0), -if(0 β€ (πβπ₯), (πβπ₯), 0))) β dom β«1 β
((β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) < π β βπ β dom
β«1(β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β (πβπ‘))))) < π)) |
462 | 303, 461 | syl 17 |
. . . . 5
β’ ((π β§ π β dom β«1) β
((β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) < π β βπ β dom
β«1(β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β (πβπ‘))))) < π)) |
463 | 462 | rexlimdva 3151 |
. . . 4
β’ (π β (βπ β dom
β«1(β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) < π β βπ β dom
β«1(β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β (πβπ‘))))) < π)) |
464 | 463 | adantr 482 |
. . 3
β’ ((π β§ π β β+) β
(βπ β dom
β«1(β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β if(0 β€
(ββif(π‘ β
π·, (πΉβπ‘), 0)), if(0 β€ (πβπ‘), (πβπ‘), 0), -if(0 β€ (πβπ‘), (πβπ‘), 0)))))) < π β βπ β dom
β«1(β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β (πβπ‘))))) < π)) |
465 | 452, 464 | syld 47 |
. 2
β’ ((π β§ π β β+) β
(βπ β dom
β«1(π
βr β€ (π‘
β β β¦ (absβ(ββif(π‘ β π·, (πΉβπ‘), 0)))) β§ Β¬
(β«1βπ)
β€ ((β«2β(π‘ β β β¦
(absβ(ββif(π‘ β π·, (πΉβπ‘), 0))))) β π)) β βπ β dom
β«1(β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β (πβπ‘))))) < π)) |
466 | 80, 465 | mpd 15 |
1
β’ ((π β§ π β β+) β
βπ β dom
β«1(β«2β(π‘ β β β¦
(absβ((ββif(π‘ β π·, (πΉβπ‘), 0)) β (πβπ‘))))) < π) |