Step | Hyp | Ref
| Expression |
1 | | ftc1anc.g |
. . 3
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) |
2 | | ftc1anc.a |
. . 3
β’ (π β π΄ β β) |
3 | | ftc1anc.b |
. . 3
β’ (π β π΅ β β) |
4 | | ftc1anc.le |
. . 3
β’ (π β π΄ β€ π΅) |
5 | | ftc1anc.s |
. . 3
β’ (π β (π΄(,)π΅) β π·) |
6 | | ftc1anc.d |
. . 3
β’ (π β π· β β) |
7 | | ftc1anc.i |
. . 3
β’ (π β πΉ β
πΏ1) |
8 | | ftc1anc.f |
. . 3
β’ (π β πΉ:π·βΆβ) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | ftc1anclem7 36043 |
. 2
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) < ((π¦ / 2) + (π¦ / 2))) |
10 | | simplll 774 |
. . . 4
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β (π β§ (π β dom β«1 β§ π β dom
β«1))) |
11 | | 3simpa 1149 |
. . . 4
β’ ((π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€) β (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) |
12 | | ioossre 13254 |
. . . . . . . . 9
β’ (π’(,)π€) β β |
13 | 12 | a1i 11 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (π’(,)π€) β
β) |
14 | | rembl 24826 |
. . . . . . . . 9
β’ β
β dom vol |
15 | 14 | a1i 11 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β β β dom vol) |
16 | | fvex 6851 |
. . . . . . . . . 10
β’
(absβ((πβπ‘) + (i Β· (πβπ‘)))) β V |
17 | | c0ex 11083 |
. . . . . . . . . 10
β’ 0 β
V |
18 | 16, 17 | ifex 4535 |
. . . . . . . . 9
β’ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β V |
19 | 18 | a1i 11 |
. . . . . . . 8
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β (π’(,)π€)) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β V) |
20 | | eldifn 4086 |
. . . . . . . . . 10
β’ (π‘ β (β β (π’(,)π€)) β Β¬ π‘ β (π’(,)π€)) |
21 | 20 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β (β
β (π’(,)π€))) β Β¬ π‘ β (π’(,)π€)) |
22 | 21 | iffalsed 4496 |
. . . . . . . 8
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β (β
β (π’(,)π€))) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) = 0) |
23 | | iftrue 4491 |
. . . . . . . . . . . 12
β’ (π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) = (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
24 | 23 | mpteq2ia 5207 |
. . . . . . . . . . 11
β’ (π‘ β (π’(,)π€) β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) = (π‘ β (π’(,)π€) β¦ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
25 | | resmpt 5988 |
. . . . . . . . . . . 12
β’ ((π’(,)π€) β β β ((π‘ β β β¦ (absβ((πβπ‘) + (i Β· (πβπ‘))))) βΎ (π’(,)π€)) = (π‘ β (π’(,)π€) β¦ (absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
26 | 12, 25 | ax-mp 5 |
. . . . . . . . . . 11
β’ ((π‘ β β β¦
(absβ((πβπ‘) + (i Β· (πβπ‘))))) βΎ (π’(,)π€)) = (π‘ β (π’(,)π€) β¦ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
27 | 24, 26 | eqtr4i 2769 |
. . . . . . . . . 10
β’ (π‘ β (π’(,)π€) β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) = ((π‘ β β β¦ (absβ((πβπ‘) + (i Β· (πβπ‘))))) βΎ (π’(,)π€)) |
28 | | i1ff 24962 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom β«1
β π:ββΆβ) |
29 | 28 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β
β) |
30 | 29 | recnd 11117 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β
β) |
31 | | ax-icn 11044 |
. . . . . . . . . . . . . . . . 17
β’ i β
β |
32 | | i1ff 24962 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β dom β«1
β π:ββΆβ) |
33 | 32 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β
β) |
34 | 33 | recnd 11117 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β
β) |
35 | | mulcl 11069 |
. . . . . . . . . . . . . . . . 17
β’ ((i
β β β§ (πβπ‘) β β) β (i Β· (πβπ‘)) β β) |
36 | 31, 34, 35 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π‘ β β)
β (i Β· (πβπ‘)) β β) |
37 | | addcl 11067 |
. . . . . . . . . . . . . . . 16
β’ (((πβπ‘) β β β§ (i Β· (πβπ‘)) β β) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
38 | 30, 36, 37 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ (((π β dom β«1
β§ π‘ β β)
β§ (π β dom
β«1 β§ π‘
β β)) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
39 | 38 | anandirs 678 |
. . . . . . . . . . . . . 14
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
40 | | reex 11076 |
. . . . . . . . . . . . . . . 16
β’ β
β V |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β β β V) |
42 | 29 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (πβπ‘) β β) |
43 | 36 | adantll 713 |
. . . . . . . . . . . . . . 15
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (i Β· (πβπ‘)) β β) |
44 | 28 | feqmptd 6906 |
. . . . . . . . . . . . . . . 16
β’ (π β dom β«1
β π = (π‘ β β β¦ (πβπ‘))) |
45 | 44 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β π
= (π‘ β β β¦
(πβπ‘))) |
46 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom β«1
β β β V) |
47 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π‘ β β)
β i β β) |
48 | | fconstmpt 5691 |
. . . . . . . . . . . . . . . . . 18
β’ (β
Γ {i}) = (π‘ β
β β¦ i) |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom β«1
β (β Γ {i}) = (π‘ β β β¦ i)) |
50 | 32 | feqmptd 6906 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom β«1
β π = (π‘ β β β¦ (πβπ‘))) |
51 | 46, 47, 33, 49, 50 | offval2 7628 |
. . . . . . . . . . . . . . . 16
β’ (π β dom β«1
β ((β Γ {i}) βf Β· π) = (π‘ β β β¦ (i Β· (πβπ‘)))) |
52 | 51 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β ((β Γ {i}) βf Β·
π) = (π‘ β β β¦ (i Β· (πβπ‘)))) |
53 | 41, 42, 43, 45, 52 | offval2 7628 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π β dom
β«1) β (π βf + ((β Γ {i})
βf Β· π)) = (π‘ β β β¦ ((πβπ‘) + (i Β· (πβπ‘))))) |
54 | | absf 15157 |
. . . . . . . . . . . . . . . 16
β’
abs:ββΆβ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β abs:ββΆβ) |
56 | 55 | feqmptd 6906 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π β dom
β«1) β abs = (π₯ β β β¦ (absβπ₯))) |
57 | | fveq2 6838 |
. . . . . . . . . . . . . 14
β’ (π₯ = ((πβπ‘) + (i Β· (πβπ‘))) β (absβπ₯) = (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
58 | 39, 53, 56, 57 | fmptco 7070 |
. . . . . . . . . . . . 13
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β (π βf + ((β Γ {i})
βf Β· π))) = (π‘ β β β¦ (absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
59 | | ftc1anclem3 36039 |
. . . . . . . . . . . . 13
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β (π βf + ((β Γ {i})
βf Β· π))) β dom
β«1) |
60 | 58, 59 | eqeltrrd 2840 |
. . . . . . . . . . . 12
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ (absβ((πβπ‘) + (i Β· (πβπ‘))))) β dom
β«1) |
61 | | i1fmbf 24961 |
. . . . . . . . . . . 12
β’ ((π‘ β β β¦
(absβ((πβπ‘) + (i Β· (πβπ‘))))) β dom β«1 β
(π‘ β β β¦
(absβ((πβπ‘) + (i Β· (πβπ‘))))) β MblFn) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . 11
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ (absβ((πβπ‘) + (i Β· (πβπ‘))))) β MblFn) |
63 | | ioombl 24851 |
. . . . . . . . . . 11
β’ (π’(,)π€) β dom vol |
64 | | mbfres 24930 |
. . . . . . . . . . 11
β’ (((π‘ β β β¦
(absβ((πβπ‘) + (i Β· (πβπ‘))))) β MblFn β§ (π’(,)π€) β dom vol) β ((π‘ β β β¦ (absβ((πβπ‘) + (i Β· (πβπ‘))))) βΎ (π’(,)π€)) β MblFn) |
65 | 62, 63, 64 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β dom β«1
β§ π β dom
β«1) β ((π‘ β β β¦ (absβ((πβπ‘) + (i Β· (πβπ‘))))) βΎ (π’(,)π€)) β MblFn) |
66 | 27, 65 | eqeltrid 2843 |
. . . . . . . . 9
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β (π’(,)π€) β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β MblFn) |
67 | 66 | adantl 483 |
. . . . . . . 8
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (π‘ β (π’(,)π€) β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β MblFn) |
68 | 13, 15, 19, 22, 67 | mbfss 24932 |
. . . . . . 7
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (π‘ β β
β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β MblFn) |
69 | 68 | adantr 482 |
. . . . . 6
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β MblFn) |
70 | 39 | abscld 15256 |
. . . . . . . . . 10
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
71 | 39 | absge0d 15264 |
. . . . . . . . . 10
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β 0 β€ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
72 | | elrege0 13300 |
. . . . . . . . . 10
β’
((absβ((πβπ‘) + (i Β· (πβπ‘)))) β (0[,)+β) β
((absβ((πβπ‘) + (i Β· (πβπ‘)))) β β β§ 0 β€
(absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
73 | 70, 71, 72 | sylanbrc 584 |
. . . . . . . . 9
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β (0[,)+β)) |
74 | | 0e0icopnf 13304 |
. . . . . . . . 9
β’ 0 β
(0[,)+β) |
75 | | ifcl 4530 |
. . . . . . . . 9
β’
(((absβ((πβπ‘) + (i Β· (πβπ‘)))) β (0[,)+β) β§ 0 β
(0[,)+β)) β if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β
(0[,)+β)) |
76 | 73, 74, 75 | sylancl 587 |
. . . . . . . 8
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β
(0[,)+β)) |
77 | 76 | fmpttd 7058 |
. . . . . . 7
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))),
0)):ββΆ(0[,)+β)) |
78 | 77 | ad2antlr 726 |
. . . . . 6
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))),
0)):ββΆ(0[,)+β)) |
79 | 70 | rexrd 11139 |
. . . . . . . . . . 11
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β
β*) |
80 | | elxrge0 13303 |
. . . . . . . . . . 11
β’
((absβ((πβπ‘) + (i Β· (πβπ‘)))) β (0[,]+β) β
((absβ((πβπ‘) + (i Β· (πβπ‘)))) β β* β§ 0 β€
(absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
81 | 79, 71, 80 | sylanbrc 584 |
. . . . . . . . . 10
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β (0[,]+β)) |
82 | | 0e0iccpnf 13305 |
. . . . . . . . . 10
β’ 0 β
(0[,]+β) |
83 | | ifcl 4530 |
. . . . . . . . . 10
β’
(((absβ((πβπ‘) + (i Β· (πβπ‘)))) β (0[,]+β) β§ 0 β
(0[,]+β)) β if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β
(0[,]+β)) |
84 | 81, 82, 83 | sylancl 587 |
. . . . . . . . 9
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β
(0[,]+β)) |
85 | 84 | fmpttd 7058 |
. . . . . . . 8
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))),
0)):ββΆ(0[,]+β)) |
86 | 85 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))),
0)):ββΆ(0[,]+β)) |
87 | | ifcl 4530 |
. . . . . . . . . . 11
β’
(((absβ((πβπ‘) + (i Β· (πβπ‘)))) β (0[,]+β) β§ 0 β
(0[,]+β)) β if(π‘
β π·,
(absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β
(0[,]+β)) |
88 | 81, 82, 87 | sylancl 587 |
. . . . . . . . . 10
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β if(π‘
β π·,
(absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β
(0[,]+β)) |
89 | 88 | fmpttd 7058 |
. . . . . . . . 9
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))),
0)):ββΆ(0[,]+β)) |
90 | | ffn 6664 |
. . . . . . . . . . . . . . 15
β’ (π:ββΆβ β
π Fn
β) |
91 | | frn 6671 |
. . . . . . . . . . . . . . . 16
β’ (π:ββΆβ β
ran π β
β) |
92 | | ax-resscn 11042 |
. . . . . . . . . . . . . . . 16
β’ β
β β |
93 | 91, 92 | sstrdi 3955 |
. . . . . . . . . . . . . . 15
β’ (π:ββΆβ β
ran π β
β) |
94 | | ffn 6664 |
. . . . . . . . . . . . . . . . 17
β’
(abs:ββΆβ β abs Fn β) |
95 | 54, 94 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ abs Fn
β |
96 | | fnco 6614 |
. . . . . . . . . . . . . . . 16
β’ ((abs Fn
β β§ π Fn β
β§ ran π β
β) β (abs β π) Fn β) |
97 | 95, 96 | mp3an1 1449 |
. . . . . . . . . . . . . . 15
β’ ((π Fn β β§ ran π β β) β (abs
β π) Fn
β) |
98 | 90, 93, 97 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π:ββΆβ β
(abs β π) Fn
β) |
99 | 28, 98 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β dom β«1
β (abs β π) Fn
β) |
100 | 99 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β π) Fn β) |
101 | | ffn 6664 |
. . . . . . . . . . . . . . 15
β’ (π:ββΆβ β
π Fn
β) |
102 | | frn 6671 |
. . . . . . . . . . . . . . . 16
β’ (π:ββΆβ β
ran π β
β) |
103 | 102, 92 | sstrdi 3955 |
. . . . . . . . . . . . . . 15
β’ (π:ββΆβ β
ran π β
β) |
104 | | fnco 6614 |
. . . . . . . . . . . . . . . 16
β’ ((abs Fn
β β§ π Fn β
β§ ran π β
β) β (abs β π) Fn β) |
105 | 95, 104 | mp3an1 1449 |
. . . . . . . . . . . . . . 15
β’ ((π Fn β β§ ran π β β) β (abs
β π) Fn
β) |
106 | 101, 103,
105 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π:ββΆβ β
(abs β π) Fn
β) |
107 | 32, 106 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β dom β«1
β (abs β π) Fn
β) |
108 | 107 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β π) Fn β) |
109 | | inidm 4177 |
. . . . . . . . . . . 12
β’ (β
β© β) = β |
110 | 28 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β dom β«1
β§ π β dom
β«1) β π:ββΆβ) |
111 | | fvco3 6936 |
. . . . . . . . . . . . 13
β’ ((π:ββΆβ β§
π‘ β β) β
((abs β π)βπ‘) = (absβ(πβπ‘))) |
112 | 110, 111 | sylan 581 |
. . . . . . . . . . . 12
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β ((abs β π)βπ‘) = (absβ(πβπ‘))) |
113 | 32 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β dom β«1
β§ π β dom
β«1) β π:ββΆβ) |
114 | | fvco3 6936 |
. . . . . . . . . . . . 13
β’ ((π:ββΆβ β§
π‘ β β) β
((abs β π)βπ‘) = (absβ(πβπ‘))) |
115 | 113, 114 | sylan 581 |
. . . . . . . . . . . 12
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β ((abs β π)βπ‘) = (absβ(πβπ‘))) |
116 | 100, 108,
41, 41, 109, 112, 115 | offval 7617 |
. . . . . . . . . . 11
β’ ((π β dom β«1
β§ π β dom
β«1) β ((abs β π) βf + (abs β π)) = (π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘))))) |
117 | 30 | addid1d 11289 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π‘ β β)
β ((πβπ‘) + 0) = (πβπ‘)) |
118 | 117 | mpteq2dva 5204 |
. . . . . . . . . . . . . . . 16
β’ (π β dom β«1
β (π‘ β β
β¦ ((πβπ‘) + 0)) = (π‘ β β β¦ (πβπ‘))) |
119 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom β«1
β β β V) |
120 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π‘ β β)
β 0 β V) |
121 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β dom β«1
β§ π‘ β β)
β i β β) |
122 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β dom β«1
β (β Γ {i}) = (π‘ β β β¦ i)) |
123 | | fconstmpt 5691 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β
Γ {0}) = (π‘ β
β β¦ 0) |
124 | 123 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β dom β«1
β (β Γ {0}) = (π‘ β β β¦ 0)) |
125 | 119, 121,
120, 122, 124 | offval2 7628 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom β«1
β ((β Γ {i}) βf Β· (β Γ
{0})) = (π‘ β β
β¦ (i Β· 0))) |
126 | | it0e0 12309 |
. . . . . . . . . . . . . . . . . . 19
β’ (i
Β· 0) = 0 |
127 | 126 | mpteq2i 5209 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ β β β¦ (i
Β· 0)) = (π‘ β
β β¦ 0) |
128 | 125, 127 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom β«1
β ((β Γ {i}) βf Β· (β Γ
{0})) = (π‘ β β
β¦ 0)) |
129 | 119, 29, 120, 44, 128 | offval2 7628 |
. . . . . . . . . . . . . . . 16
β’ (π β dom β«1
β (π
βf + ((β Γ {i}) βf Β·
(β Γ {0}))) = (π‘ β β β¦ ((πβπ‘) + 0))) |
130 | 118, 129,
44 | 3eqtr4d 2788 |
. . . . . . . . . . . . . . 15
β’ (π β dom β«1
β (π
βf + ((β Γ {i}) βf Β·
(β Γ {0}))) = π) |
131 | 130 | coeq2d 5815 |
. . . . . . . . . . . . . 14
β’ (π β dom β«1
β (abs β (π
βf + ((β Γ {i}) βf Β·
(β Γ {0})))) = (abs β π)) |
132 | | i1f0 24973 |
. . . . . . . . . . . . . . 15
β’ (β
Γ {0}) β dom β«1 |
133 | | ftc1anclem3 36039 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ (β Γ {0}) β dom β«1) β (abs β
(π βf +
((β Γ {i}) βf Β· (β Γ {0}))))
β dom β«1) |
134 | 132, 133 | mpan2 690 |
. . . . . . . . . . . . . 14
β’ (π β dom β«1
β (abs β (π
βf + ((β Γ {i}) βf Β·
(β Γ {0})))) β dom β«1) |
135 | 131, 134 | eqeltrrd 2840 |
. . . . . . . . . . . . 13
β’ (π β dom β«1
β (abs β π)
β dom β«1) |
136 | 135 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β π) β dom
β«1) |
137 | | coeq2 5811 |
. . . . . . . . . . . . . . 15
β’ (π = π β (abs β π) = (abs β π)) |
138 | 137 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π = π β ((abs β π) β dom β«1 β (abs
β π) β dom
β«1)) |
139 | 138, 135 | vtoclga 3533 |
. . . . . . . . . . . . 13
β’ (π β dom β«1
β (abs β π)
β dom β«1) |
140 | 139 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β π) β dom
β«1) |
141 | 136, 140 | i1fadd 24981 |
. . . . . . . . . . 11
β’ ((π β dom β«1
β§ π β dom
β«1) β ((abs β π) βf + (abs β π)) β dom
β«1) |
142 | 116, 141 | eqeltrrd 2840 |
. . . . . . . . . 10
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘)))) β dom
β«1) |
143 | 30 | abscld 15256 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(πβπ‘)) β β) |
144 | 30 | absge0d 15264 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π‘ β β)
β 0 β€ (absβ(πβπ‘))) |
145 | | elrege0 13300 |
. . . . . . . . . . . . . . . 16
β’
((absβ(πβπ‘)) β (0[,)+β) β
((absβ(πβπ‘)) β β β§ 0 β€
(absβ(πβπ‘)))) |
146 | 143, 144,
145 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(πβπ‘)) β (0[,)+β)) |
147 | 34 | abscld 15256 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(πβπ‘)) β β) |
148 | 34 | absge0d 15264 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π‘ β β)
β 0 β€ (absβ(πβπ‘))) |
149 | | elrege0 13300 |
. . . . . . . . . . . . . . . 16
β’
((absβ(πβπ‘)) β (0[,)+β) β
((absβ(πβπ‘)) β β β§ 0 β€
(absβ(πβπ‘)))) |
150 | 147, 148,
149 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(πβπ‘)) β (0[,)+β)) |
151 | | ge0addcl 13306 |
. . . . . . . . . . . . . . 15
β’
(((absβ(πβπ‘)) β (0[,)+β) β§
(absβ(πβπ‘)) β (0[,)+β)) β
((absβ(πβπ‘)) + (absβ(πβπ‘))) β (0[,)+β)) |
152 | 146, 150,
151 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ (((π β dom β«1
β§ π‘ β β)
β§ (π β dom
β«1 β§ π‘
β β)) β ((absβ(πβπ‘)) + (absβ(πβπ‘))) β (0[,)+β)) |
153 | 152 | anandirs 678 |
. . . . . . . . . . . . 13
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β ((absβ(πβπ‘)) + (absβ(πβπ‘))) β (0[,)+β)) |
154 | 153 | fmpttd 7058 |
. . . . . . . . . . . 12
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘)))):ββΆ(0[,)+β)) |
155 | | 0plef 24958 |
. . . . . . . . . . . 12
β’ ((π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘)))):ββΆ(0[,)+β) β
((π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘)))):ββΆβ β§
0π βr β€ (π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘)))))) |
156 | 154, 155 | sylib 217 |
. . . . . . . . . . 11
β’ ((π β dom β«1
β§ π β dom
β«1) β ((π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘)))):ββΆβ β§
0π βr β€ (π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘)))))) |
157 | 156 | simprd 497 |
. . . . . . . . . 10
β’ ((π β dom β«1
β§ π β dom
β«1) β 0π βr β€ (π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘))))) |
158 | | itg2itg1 25023 |
. . . . . . . . . . 11
β’ (((π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘)))) β dom β«1 β§
0π βr β€ (π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘))))) β (β«2β(π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘))))) = (β«1β(π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘)))))) |
159 | | itg1cl 24971 |
. . . . . . . . . . . 12
β’ ((π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘)))) β dom β«1 β
(β«1β(π‘
β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘))))) β β) |
160 | 159 | adantr 482 |
. . . . . . . . . . 11
β’ (((π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘)))) β dom β«1 β§
0π βr β€ (π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘))))) β (β«1β(π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘))))) β β) |
161 | 158, 160 | eqeltrd 2839 |
. . . . . . . . . 10
β’ (((π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘)))) β dom β«1 β§
0π βr β€ (π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘))))) β (β«2β(π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘))))) β β) |
162 | 142, 157,
161 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β dom β«1
β§ π β dom
β«1) β (β«2β(π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘))))) β β) |
163 | | icossicc 13282 |
. . . . . . . . . . 11
β’
(0[,)+β) β (0[,]+β) |
164 | | fss 6681 |
. . . . . . . . . . 11
β’ (((π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘)))):ββΆ(0[,)+β) β§
(0[,)+β) β (0[,]+β)) β (π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘)))):ββΆ(0[,]+β)) |
165 | 154, 163,
164 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘)))):ββΆ(0[,]+β)) |
166 | | 0re 11091 |
. . . . . . . . . . . . . 14
β’ 0 β
β |
167 | | ifcl 4530 |
. . . . . . . . . . . . . 14
β’
(((absβ((πβπ‘) + (i Β· (πβπ‘)))) β β β§ 0 β β)
β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β β) |
168 | 70, 166, 167 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β if(π‘
β π·,
(absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β β) |
169 | | readdcl 11068 |
. . . . . . . . . . . . . . 15
β’
(((absβ(πβπ‘)) β β β§ (absβ(πβπ‘)) β β) β ((absβ(πβπ‘)) + (absβ(πβπ‘))) β β) |
170 | 143, 147,
169 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ (((π β dom β«1
β§ π‘ β β)
β§ (π β dom
β«1 β§ π‘
β β)) β ((absβ(πβπ‘)) + (absβ(πβπ‘))) β β) |
171 | 170 | anandirs 678 |
. . . . . . . . . . . . 13
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β ((absβ(πβπ‘)) + (absβ(πβπ‘))) β β) |
172 | 70 | leidd 11655 |
. . . . . . . . . . . . . 14
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
173 | | breq1 5107 |
. . . . . . . . . . . . . . 15
β’
((absβ((πβπ‘) + (i Β· (πβπ‘)))) = if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β ((absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ (absβ((πβπ‘) + (i Β· (πβπ‘)))) β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ (absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
174 | | breq1 5107 |
. . . . . . . . . . . . . . 15
β’ (0 =
if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β (0 β€ (absβ((πβπ‘) + (i Β· (πβπ‘)))) β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ (absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
175 | 173, 174 | ifboth 4524 |
. . . . . . . . . . . . . 14
β’
(((absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ (absβ((πβπ‘) + (i Β· (πβπ‘)))) β§ 0 β€ (absβ((πβπ‘) + (i Β· (πβπ‘))))) β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
176 | 172, 71, 175 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β if(π‘
β π·,
(absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
177 | | abstri 15150 |
. . . . . . . . . . . . . . . 16
β’ (((πβπ‘) β β β§ (i Β· (πβπ‘)) β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ ((absβ(πβπ‘)) + (absβ(i Β· (πβπ‘))))) |
178 | 30, 36, 177 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ (((π β dom β«1
β§ π‘ β β)
β§ (π β dom
β«1 β§ π‘
β β)) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ ((absβ(πβπ‘)) + (absβ(i Β· (πβπ‘))))) |
179 | 178 | anandirs 678 |
. . . . . . . . . . . . . 14
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ ((absβ(πβπ‘)) + (absβ(i Β· (πβπ‘))))) |
180 | | absmul 15114 |
. . . . . . . . . . . . . . . . . . 19
β’ ((i
β β β§ (πβπ‘) β β) β (absβ(i
Β· (πβπ‘))) = ((absβi) Β·
(absβ(πβπ‘)))) |
181 | 31, 34, 180 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(i Β· (πβπ‘))) = ((absβi) Β·
(absβ(πβπ‘)))) |
182 | | absi 15106 |
. . . . . . . . . . . . . . . . . . 19
β’
(absβi) = 1 |
183 | 182 | oveq1i 7360 |
. . . . . . . . . . . . . . . . . 18
β’
((absβi) Β· (absβ(πβπ‘))) = (1 Β· (absβ(πβπ‘))) |
184 | 181, 183 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(i Β· (πβπ‘))) = (1 Β· (absβ(πβπ‘)))) |
185 | 147 | recnd 11117 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(πβπ‘)) β β) |
186 | 185 | mulid2d 11107 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π‘ β β)
β (1 Β· (absβ(πβπ‘))) = (absβ(πβπ‘))) |
187 | 184, 186 | eqtrd 2778 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(i Β· (πβπ‘))) = (absβ(πβπ‘))) |
188 | 187 | adantll 713 |
. . . . . . . . . . . . . . 15
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ(i Β· (πβπ‘))) = (absβ(πβπ‘))) |
189 | 188 | oveq2d 7366 |
. . . . . . . . . . . . . 14
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β ((absβ(πβπ‘)) + (absβ(i Β· (πβπ‘)))) = ((absβ(πβπ‘)) + (absβ(πβπ‘)))) |
190 | 179, 189 | breqtrd 5130 |
. . . . . . . . . . . . 13
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ ((absβ(πβπ‘)) + (absβ(πβπ‘)))) |
191 | 168, 70, 171, 176, 190 | letrd 11246 |
. . . . . . . . . . . 12
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β if(π‘
β π·,
(absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ ((absβ(πβπ‘)) + (absβ(πβπ‘)))) |
192 | 191 | ralrimiva 3142 |
. . . . . . . . . . 11
β’ ((π β dom β«1
β§ π β dom
β«1) β βπ‘ β β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ ((absβ(πβπ‘)) + (absβ(πβπ‘)))) |
193 | | eqidd 2739 |
. . . . . . . . . . . 12
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) = (π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
194 | | eqidd 2739 |
. . . . . . . . . . . 12
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘)))) = (π‘ β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘))))) |
195 | 41, 168, 171, 193, 194 | ofrfval2 7629 |
. . . . . . . . . . 11
β’ ((π β dom β«1
β§ π β dom
β«1) β ((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βr β€ (π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘)))) β βπ‘ β β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ ((absβ(πβπ‘)) + (absβ(πβπ‘))))) |
196 | 192, 195 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βr β€ (π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘))))) |
197 | | itg2le 25026 |
. . . . . . . . . 10
β’ (((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)):ββΆ(0[,]+β) β§
(π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘)))):ββΆ(0[,]+β) β§
(π‘ β β β¦
if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βr β€ (π‘ β β β¦
((absβ(πβπ‘)) + (absβ(πβπ‘))))) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β€
(β«2β(π‘
β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘)))))) |
198 | 89, 165, 196, 197 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β dom β«1
β§ π β dom
β«1) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β€
(β«2β(π‘
β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘)))))) |
199 | | itg2lecl 25025 |
. . . . . . . . 9
β’ (((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)):ββΆ(0[,]+β) β§
(β«2β(π‘
β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘))))) β β β§
(β«2β(π‘
β β β¦ if(π‘
β π·,
(absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β€
(β«2β(π‘
β β β¦ ((absβ(πβπ‘)) + (absβ(πβπ‘)))))) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
200 | 89, 162, 198, 199 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β dom β«1
β§ π β dom
β«1) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
201 | 200 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
202 | 89 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))),
0)):ββΆ(0[,]+β)) |
203 | | breq1 5107 |
. . . . . . . . . . 11
β’
((absβ((πβπ‘) + (i Β· (πβπ‘)))) = if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β ((absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
204 | | breq1 5107 |
. . . . . . . . . . 11
β’ (0 =
if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β (0 β€ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
205 | | elioore 13223 |
. . . . . . . . . . . . . . 15
β’ (π‘ β (π’(,)π€) β π‘ β β) |
206 | 205, 172 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β (π’(,)π€)) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
207 | 206 | adantll 713 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β (π’(,)π€)) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
208 | 207 | adantlr 714 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
209 | 2 | rexrd 11139 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΄ β
β*) |
210 | 3 | rexrd 11139 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΅ β
β*) |
211 | 209, 210 | jca 513 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΄ β β* β§ π΅ β
β*)) |
212 | | df-icc 13200 |
. . . . . . . . . . . . . . . . . . . . 21
β’ [,] =
(π₯ β
β*, π¦
β β* β¦ {π‘ β β* β£ (π₯ β€ π‘ β§ π‘ β€ π¦)}) |
213 | 212 | elixx3g 13206 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π’ β (π΄[,]π΅) β ((π΄ β β* β§ π΅ β β*
β§ π’ β
β*) β§ (π΄ β€ π’ β§ π’ β€ π΅))) |
214 | 213 | simprbi 498 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ β (π΄[,]π΅) β (π΄ β€ π’ β§ π’ β€ π΅)) |
215 | 214 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ β (π΄[,]π΅) β π΄ β€ π’) |
216 | 212 | elixx3g 13206 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ β (π΄[,]π΅) β ((π΄ β β* β§ π΅ β β*
β§ π€ β
β*) β§ (π΄ β€ π€ β§ π€ β€ π΅))) |
217 | 216 | simprbi 498 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ β (π΄[,]π΅) β (π΄ β€ π€ β§ π€ β€ π΅)) |
218 | 217 | simprd 497 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β (π΄[,]π΅) β π€ β€ π΅) |
219 | 215, 218 | anim12i 614 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅)) β (π΄ β€ π’ β§ π€ β€ π΅)) |
220 | | ioossioo 13287 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β*
β§ π΅ β
β*) β§ (π΄ β€ π’ β§ π€ β€ π΅)) β (π’(,)π€) β (π΄(,)π΅)) |
221 | 211, 219,
220 | syl2an 597 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π’(,)π€) β (π΄(,)π΅)) |
222 | 5 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π΄(,)π΅) β π·) |
223 | 221, 222 | sstrd 3953 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π’(,)π€) β π·) |
224 | 223 | sselda 3943 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β π‘ β π·) |
225 | | iftrue 4491 |
. . . . . . . . . . . . . 14
β’ (π‘ β π· β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) = (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
226 | 224, 225 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) = (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
227 | 226 | adantllr 718 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) = (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
228 | 208, 227 | breqtrrd 5132 |
. . . . . . . . . . 11
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) |
229 | | breq2 5108 |
. . . . . . . . . . . . 13
β’
((absβ((πβπ‘) + (i Β· (πβπ‘)))) = if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β (0 β€ (absβ((πβπ‘) + (i Β· (πβπ‘)))) β 0 β€ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
230 | | breq2 5108 |
. . . . . . . . . . . . 13
β’ (0 =
if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β (0 β€ 0 β 0 β€
if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
231 | 6 | sselda 3943 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π‘ β π·) β π‘ β β) |
232 | 231 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β π‘ β β) |
233 | 71 | adantll 713 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β β)
β 0 β€ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
234 | 232, 233 | syldan 592 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β 0 β€
(absβ((πβπ‘) + (i Β· (πβπ‘))))) |
235 | | 0le0 12188 |
. . . . . . . . . . . . . 14
β’ 0 β€
0 |
236 | 235 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ Β¬ π‘ β π·) β 0 β€
0) |
237 | 229, 230,
234, 236 | ifbothda 4523 |
. . . . . . . . . . . 12
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β 0 β€ if(π‘ β
π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) |
238 | 237 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ Β¬ π‘ β (π’(,)π€)) β 0 β€ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) |
239 | 203, 204,
228, 238 | ifbothda 4523 |
. . . . . . . . . 10
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) |
240 | 239 | ralrimivw 3146 |
. . . . . . . . 9
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) |
241 | 40 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β
V) |
242 | 18 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β β) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β V) |
243 | 16, 17 | ifex 4535 |
. . . . . . . . . . . 12
β’ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β V |
244 | 243 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β β) β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β V) |
245 | | eqidd 2739 |
. . . . . . . . . . 11
β’ (π β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) = (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
246 | | eqidd 2739 |
. . . . . . . . . . 11
β’ (π β (π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) = (π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
247 | 241, 242,
244, 245, 246 | ofrfval2 7629 |
. . . . . . . . . 10
β’ (π β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βr β€ (π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
248 | 247 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βr β€ (π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
249 | 240, 248 | mpbird 257 |
. . . . . . . 8
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βr β€ (π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
250 | | itg2le 25026 |
. . . . . . . 8
β’ (((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)):ββΆ(0[,]+β) β§
(π‘ β β β¦
if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)):ββΆ(0[,]+β) β§
(π‘ β β β¦
if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βr β€ (π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β€
(β«2β(π‘
β β β¦ if(π‘
β π·,
(absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)))) |
251 | 86, 202, 249, 250 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β€
(β«2β(π‘
β β β¦ if(π‘
β π·,
(absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)))) |
252 | | itg2lecl 25025 |
. . . . . . 7
β’ (((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)):ββΆ(0[,]+β) β§
(β«2β(π‘
β β β¦ if(π‘
β π·,
(absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β β§
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β€
(β«2β(π‘
β β β¦ if(π‘
β π·,
(absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
253 | 86, 201, 251, 252 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
254 | 8 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π‘ β π·) β (πΉβπ‘) β β) |
255 | 254 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β π·) β (πΉβπ‘) β β) |
256 | 224, 255 | syldan 592 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (πΉβπ‘) β β) |
257 | 256 | adantllr 718 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (πΉβπ‘) β β) |
258 | 205, 39 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β (π’(,)π€)) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
259 | 258 | adantll 713 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β (π’(,)π€)) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
260 | 259 | adantlr 714 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
261 | 257, 260 | subcld 11446 |
. . . . . . . . . . 11
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
262 | 261 | abscld 15256 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β β) |
263 | 261 | absge0d 15264 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β 0 β€ (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
264 | | elrege0 13300 |
. . . . . . . . . 10
β’
((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β (0[,)+β) β
((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β β β§ 0 β€
(absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))))) |
265 | 262, 263,
264 | sylanbrc 584 |
. . . . . . . . 9
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β (0[,)+β)) |
266 | 74 | a1i 11 |
. . . . . . . . 9
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ Β¬ π‘ β (π’(,)π€)) β 0 β
(0[,)+β)) |
267 | 265, 266 | ifclda 4520 |
. . . . . . . 8
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β
(0[,)+β)) |
268 | 267 | adantr 482 |
. . . . . . 7
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β β) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β
(0[,)+β)) |
269 | 268 | fmpttd 7058 |
. . . . . 6
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))),
0)):ββΆ(0[,)+β)) |
270 | 262 | rexrd 11139 |
. . . . . . . . . . 11
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β
β*) |
271 | | elxrge0 13303 |
. . . . . . . . . . 11
β’
((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β (0[,]+β) β
((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β β* β§ 0 β€
(absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))))) |
272 | 270, 263,
271 | sylanbrc 584 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β (0[,]+β)) |
273 | 82 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ Β¬ π‘ β (π’(,)π€)) β 0 β
(0[,]+β)) |
274 | 272, 273 | ifclda 4520 |
. . . . . . . . 9
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β
(0[,]+β)) |
275 | 274 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β β) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β
(0[,]+β)) |
276 | 275 | fmpttd 7058 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))),
0)):ββΆ(0[,]+β)) |
277 | | recncf 24187 |
. . . . . . . . . . . . 13
β’ β
β (ββcnββ) |
278 | | prid1g 4720 |
. . . . . . . . . . . . 13
β’ (β
β (ββcnββ)
β β β {β, β}) |
279 | 277, 278 | ax-mp 5 |
. . . . . . . . . . . 12
β’ β
β {β, β} |
280 | | ftc1anclem2 36038 |
. . . . . . . . . . . 12
β’ ((πΉ:π·βΆβ β§ πΉ β πΏ1 β§ β
β {β, β}) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) β β) |
281 | 279, 280 | mp3an3 1451 |
. . . . . . . . . . 11
β’ ((πΉ:π·βΆβ β§ πΉ β πΏ1) β
(β«2β(π‘
β β β¦ if(π‘
β π·,
(absβ(ββ(πΉβπ‘))), 0))) β β) |
282 | 8, 7, 281 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β
(β«2β(π‘
β β β¦ if(π‘
β π·,
(absβ(ββ(πΉβπ‘))), 0))) β β) |
283 | | imcncf 24188 |
. . . . . . . . . . . . 13
β’ β
β (ββcnββ) |
284 | | prid2g 4721 |
. . . . . . . . . . . . 13
β’ (β
β (ββcnββ)
β β β {β, β}) |
285 | 283, 284 | ax-mp 5 |
. . . . . . . . . . . 12
β’ β
β {β, β} |
286 | | ftc1anclem2 36038 |
. . . . . . . . . . . 12
β’ ((πΉ:π·βΆβ β§ πΉ β πΏ1 β§ β
β {β, β}) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) β β) |
287 | 285, 286 | mp3an3 1451 |
. . . . . . . . . . 11
β’ ((πΉ:π·βΆβ β§ πΉ β πΏ1) β
(β«2β(π‘
β β β¦ if(π‘
β π·,
(absβ(ββ(πΉβπ‘))), 0))) β β) |
288 | 8, 7, 287 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β
(β«2β(π‘
β β β¦ if(π‘
β π·,
(absβ(ββ(πΉβπ‘))), 0))) β β) |
289 | 282, 288 | readdcld 11118 |
. . . . . . . . 9
β’ (π β
((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) β β) |
290 | 289 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) β β) |
291 | 201, 290 | readdcld 11118 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + ((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))))) β β) |
292 | | ge0addcl 13306 |
. . . . . . . . . . . . 13
β’ ((π₯ β (0[,)+β) β§
π¦ β (0[,)+β))
β (π₯ + π¦) β
(0[,)+β)) |
293 | 292 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π₯ β
(0[,)+β) β§ π¦
β (0[,)+β))) β (π₯ + π¦) β (0[,)+β)) |
294 | | ifcl 4530 |
. . . . . . . . . . . . . . 15
β’
(((absβ((πβπ‘) + (i Β· (πβπ‘)))) β (0[,)+β) β§ 0 β
(0[,)+β)) β if(π‘
β π·,
(absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β
(0[,)+β)) |
295 | 73, 74, 294 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β if(π‘
β π·,
(absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β
(0[,)+β)) |
296 | 295 | fmpttd 7058 |
. . . . . . . . . . . . 13
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))),
0)):ββΆ(0[,)+β)) |
297 | 296 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (π‘ β β
β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))),
0)):ββΆ(0[,)+β)) |
298 | 292 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β (0[,)+β) β§ π¦ β (0[,)+β))) β
(π₯ + π¦) β (0[,)+β)) |
299 | 254 | recld 15013 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π‘ β π·) β (ββ(πΉβπ‘)) β β) |
300 | 299 | recnd 11117 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π‘ β π·) β (ββ(πΉβπ‘)) β β) |
301 | 300 | abscld 15256 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π‘ β π·) β (absβ(ββ(πΉβπ‘))) β β) |
302 | 300 | absge0d 15264 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π‘ β π·) β 0 β€
(absβ(ββ(πΉβπ‘)))) |
303 | | elrege0 13300 |
. . . . . . . . . . . . . . . . . 18
β’
((absβ(ββ(πΉβπ‘))) β (0[,)+β) β
((absβ(ββ(πΉβπ‘))) β β β§ 0 β€
(absβ(ββ(πΉβπ‘))))) |
304 | 301, 302,
303 | sylanbrc 584 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π‘ β π·) β (absβ(ββ(πΉβπ‘))) β (0[,)+β)) |
305 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ π‘ β π·) β 0 β
(0[,)+β)) |
306 | 304, 305 | ifclda 4520 |
. . . . . . . . . . . . . . . 16
β’ (π β if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) β
(0[,)+β)) |
307 | 306 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π‘ β β) β if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) β
(0[,)+β)) |
308 | 307 | fmpttd 7058 |
. . . . . . . . . . . . . 14
β’ (π β (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))),
0)):ββΆ(0[,)+β)) |
309 | 254 | imcld 15014 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π‘ β π·) β (ββ(πΉβπ‘)) β β) |
310 | 309 | recnd 11117 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π‘ β π·) β (ββ(πΉβπ‘)) β β) |
311 | 310 | abscld 15256 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π‘ β π·) β (absβ(ββ(πΉβπ‘))) β β) |
312 | 310 | absge0d 15264 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π‘ β π·) β 0 β€
(absβ(ββ(πΉβπ‘)))) |
313 | | elrege0 13300 |
. . . . . . . . . . . . . . . . . 18
β’
((absβ(ββ(πΉβπ‘))) β (0[,)+β) β
((absβ(ββ(πΉβπ‘))) β β β§ 0 β€
(absβ(ββ(πΉβπ‘))))) |
314 | 311, 312,
313 | sylanbrc 584 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π‘ β π·) β (absβ(ββ(πΉβπ‘))) β (0[,)+β)) |
315 | 314, 305 | ifclda 4520 |
. . . . . . . . . . . . . . . 16
β’ (π β if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) β
(0[,)+β)) |
316 | 315 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π‘ β β) β if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) β
(0[,)+β)) |
317 | 316 | fmpttd 7058 |
. . . . . . . . . . . . . 14
β’ (π β (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))),
0)):ββΆ(0[,)+β)) |
318 | 298, 308,
317, 241, 241, 109 | off 7626 |
. . . . . . . . . . . . 13
β’ (π β ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))),
0))):ββΆ(0[,)+β)) |
319 | 318 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β ((π‘ β β
β¦ if(π‘ β π·,
(absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))),
0))):ββΆ(0[,)+β)) |
320 | 40 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β β β V) |
321 | 293, 297,
319, 320, 320, 109 | off 7626 |
. . . . . . . . . . 11
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β ((π‘ β β
β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))),
0)))):ββΆ(0[,)+β)) |
322 | | fss 6681 |
. . . . . . . . . . 11
β’ ((((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))):ββΆ(0[,)+β)
β§ (0[,)+β) β (0[,]+β)) β ((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))),
0)))):ββΆ(0[,]+β)) |
323 | 321, 163,
322 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β ((π‘ β β
β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))),
0)))):ββΆ(0[,]+β)) |
324 | 323 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))),
0)))):ββΆ(0[,]+β)) |
325 | | 0xr 11136 |
. . . . . . . . . . . . . 14
β’ 0 β
β* |
326 | 325 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ Β¬ π‘ β (π’(,)π€)) β 0 β
β*) |
327 | 270, 326 | ifclda 4520 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β
β*) |
328 | 254 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (πΉβπ‘) β β) |
329 | 39 | adantll 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β β)
β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
330 | 232, 329 | syldan 592 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
331 | 328, 330 | subcld 11446 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
332 | 331 | abscld 15256 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β β) |
333 | 332 | rexrd 11139 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β
β*) |
334 | 325 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ Β¬ π‘ β π·) β 0 β
β*) |
335 | 333, 334 | ifclda 4520 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β
β*) |
336 | 335 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β
β*) |
337 | 330 | abscld 15256 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
338 | | 0red 11092 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ Β¬ π‘ β π·) β 0 β
β) |
339 | 337, 338 | ifclda 4520 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β β) |
340 | | 0red 11092 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ π‘ β π·) β 0 β β) |
341 | 301, 340 | ifclda 4520 |
. . . . . . . . . . . . . . . . 17
β’ (π β if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) β β) |
342 | 311, 340 | ifclda 4520 |
. . . . . . . . . . . . . . . . 17
β’ (π β if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) β β) |
343 | 341, 342 | readdcld 11118 |
. . . . . . . . . . . . . . . 16
β’ (π β (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) β β) |
344 | 343 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (if(π‘ β π·,
(absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) β β) |
345 | 339, 344 | readdcld 11118 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) β β) |
346 | 345 | rexrd 11139 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) β
β*) |
347 | 346 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) β
β*) |
348 | | breq1 5107 |
. . . . . . . . . . . . 13
β’
((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) = if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β€ if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) |
349 | | breq1 5107 |
. . . . . . . . . . . . 13
β’ (0 =
if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β (0 β€ if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) |
350 | 224 | adantllr 718 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β π‘ β π·) |
351 | 332 | leidd 11655 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β€ (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
352 | 351 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β π·) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β€ (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
353 | | iftrue 4491 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β π· β if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) = (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
354 | 353 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β π·) β if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) = (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
355 | 352, 354 | breqtrrd 5132 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β π·) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β€ if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) |
356 | 350, 355 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β€ if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) |
357 | | breq2 5108 |
. . . . . . . . . . . . . . 15
β’
((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) = if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β (0 β€ (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β 0 β€ if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) |
358 | | breq2 5108 |
. . . . . . . . . . . . . . 15
β’ (0 =
if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β (0 β€ 0 β 0 β€
if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) |
359 | 331 | absge0d 15264 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β 0 β€
(absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
360 | 357, 358,
359, 236 | ifbothda 4523 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β 0 β€ if(π‘ β
π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) |
361 | 360 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ Β¬ π‘ β (π’(,)π€)) β 0 β€ if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) |
362 | 348, 349,
356, 361 | ifbothda 4523 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) |
363 | 254 | negcld 11433 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π‘ β π·) β -(πΉβπ‘) β β) |
364 | 363 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β -(πΉβπ‘) β β) |
365 | 330, 364 | addcld 11108 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (((πβπ‘) + (i Β· (πβπ‘))) + -(πΉβπ‘)) β β) |
366 | 365 | abscld 15256 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ(((πβπ‘) + (i Β· (πβπ‘))) + -(πΉβπ‘))) β β) |
367 | 363 | abscld 15256 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π‘ β π·) β (absβ-(πΉβπ‘)) β β) |
368 | 367 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ-(πΉβπ‘)) β β) |
369 | 337, 368 | readdcld 11118 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ-(πΉβπ‘))) β β) |
370 | 301, 311 | readdcld 11118 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π‘ β π·) β ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘)))) β β) |
371 | 370 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β
((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘)))) β β) |
372 | 337, 371 | readdcld 11118 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))) β β) |
373 | 330, 364 | abstrid 15276 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ(((πβπ‘) + (i Β· (πβπ‘))) + -(πΉβπ‘))) β€ ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ-(πΉβπ‘)))) |
374 | | mulcl 11069 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((i
β β β§ (ββ(πΉβπ‘)) β β) β (i Β·
(ββ(πΉβπ‘))) β β) |
375 | 31, 310, 374 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π‘ β π·) β (i Β· (ββ(πΉβπ‘))) β β) |
376 | 300, 375 | abstrid 15276 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π‘ β π·) β (absβ((ββ(πΉβπ‘)) + (i Β· (ββ(πΉβπ‘))))) β€ ((absβ(ββ(πΉβπ‘))) + (absβ(i Β·
(ββ(πΉβπ‘)))))) |
377 | 254 | absnegd 15269 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π‘ β π·) β (absβ-(πΉβπ‘)) = (absβ(πΉβπ‘))) |
378 | 254 | replimd 15016 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π‘ β π·) β (πΉβπ‘) = ((ββ(πΉβπ‘)) + (i Β· (ββ(πΉβπ‘))))) |
379 | 378 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π‘ β π·) β (absβ(πΉβπ‘)) = (absβ((ββ(πΉβπ‘)) + (i Β· (ββ(πΉβπ‘)))))) |
380 | 377, 379 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π‘ β π·) β (absβ-(πΉβπ‘)) = (absβ((ββ(πΉβπ‘)) + (i Β· (ββ(πΉβπ‘)))))) |
381 | | absmul 15114 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((i
β β β§ (ββ(πΉβπ‘)) β β) β (absβ(i
Β· (ββ(πΉβπ‘)))) = ((absβi) Β·
(absβ(ββ(πΉβπ‘))))) |
382 | 31, 310, 381 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π‘ β π·) β (absβ(i Β·
(ββ(πΉβπ‘)))) = ((absβi) Β·
(absβ(ββ(πΉβπ‘))))) |
383 | 182 | oveq1i 7360 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((absβi) Β· (absβ(ββ(πΉβπ‘)))) = (1 Β·
(absβ(ββ(πΉβπ‘)))) |
384 | 382, 383 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π‘ β π·) β (absβ(i Β·
(ββ(πΉβπ‘)))) = (1 Β·
(absβ(ββ(πΉβπ‘))))) |
385 | 311 | recnd 11117 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π‘ β π·) β (absβ(ββ(πΉβπ‘))) β β) |
386 | 385 | mulid2d 11107 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π‘ β π·) β (1 Β·
(absβ(ββ(πΉβπ‘)))) = (absβ(ββ(πΉβπ‘)))) |
387 | 384, 386 | eqtr2d 2779 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π‘ β π·) β (absβ(ββ(πΉβπ‘))) = (absβ(i Β·
(ββ(πΉβπ‘))))) |
388 | 387 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π‘ β π·) β ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘)))) = ((absβ(ββ(πΉβπ‘))) + (absβ(i Β·
(ββ(πΉβπ‘)))))) |
389 | 376, 380,
388 | 3brtr4d 5136 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π‘ β π·) β (absβ-(πΉβπ‘)) β€ ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))) |
390 | 389 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ-(πΉβπ‘)) β€ ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))) |
391 | 368, 371,
337, 390 | leadd2dd 11704 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ-(πΉβπ‘))) β€ ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘)))))) |
392 | 366, 369,
372, 373, 391 | letrd 11246 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ(((πβπ‘) + (i Β· (πβπ‘))) + -(πΉβπ‘))) β€ ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘)))))) |
393 | 328, 330 | abssubd 15273 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) = (absβ(((πβπ‘) + (i Β· (πβπ‘))) β (πΉβπ‘)))) |
394 | 353 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) = (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
395 | 330, 328 | negsubd 11452 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (((πβπ‘) + (i Β· (πβπ‘))) + -(πΉβπ‘)) = (((πβπ‘) + (i Β· (πβπ‘))) β (πΉβπ‘))) |
396 | 395 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ(((πβπ‘) + (i Β· (πβπ‘))) + -(πΉβπ‘))) = (absβ(((πβπ‘) + (i Β· (πβπ‘))) β (πΉβπ‘)))) |
397 | 393, 394,
396 | 3eqtr4d 2788 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) = (absβ(((πβπ‘) + (i Β· (πβπ‘))) + -(πΉβπ‘)))) |
398 | | iftrue 4491 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ β π· β if(π‘ β π·, ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))), 0) = ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘)))))) |
399 | 398 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β if(π‘ β π·, ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))), 0) = ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘)))))) |
400 | 392, 397,
399 | 3brtr4d 5136 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ if(π‘ β π·, ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))), 0)) |
401 | 400 | ex 414 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (π‘ β π· β if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ if(π‘ β π·, ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))), 0))) |
402 | 235 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π‘ β π· β 0 β€ 0) |
403 | | iffalse 4494 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π‘ β π· β if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) = 0) |
404 | | iffalse 4494 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π‘ β π· β if(π‘ β π·, ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))), 0) = 0) |
405 | 402, 403,
404 | 3brtr4d 5136 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π‘ β π· β if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ if(π‘ β π·, ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))), 0)) |
406 | 401, 405 | pm2.61d1 180 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ if(π‘ β π·, ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))), 0)) |
407 | | iftrue 4491 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ β π· β if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) = (absβ(ββ(πΉβπ‘)))) |
408 | | iftrue 4491 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ β π· β if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) = (absβ(ββ(πΉβπ‘)))) |
409 | 407, 408 | oveq12d 7368 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ β π· β (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) = ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))) |
410 | 225, 409 | oveq12d 7368 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β π· β (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) = ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘)))))) |
411 | 410, 398 | eqtr4d 2781 |
. . . . . . . . . . . . . . 15
β’ (π‘ β π· β (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) = if(π‘ β π·, ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))), 0)) |
412 | | 00id 11264 |
. . . . . . . . . . . . . . . . . 18
β’ (0 + 0) =
0 |
413 | 412 | oveq2i 7361 |
. . . . . . . . . . . . . . . . 17
β’ (0 + (0 +
0)) = (0 + 0) |
414 | 413, 412 | eqtri 2766 |
. . . . . . . . . . . . . . . 16
β’ (0 + (0 +
0)) = 0 |
415 | | iffalse 4494 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π‘ β π· β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) = 0) |
416 | | iffalse 4494 |
. . . . . . . . . . . . . . . . . 18
β’ (Β¬
π‘ β π· β if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) = 0) |
417 | | iffalse 4494 |
. . . . . . . . . . . . . . . . . 18
β’ (Β¬
π‘ β π· β if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) = 0) |
418 | 416, 417 | oveq12d 7368 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π‘ β π· β (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) = (0 + 0)) |
419 | 415, 418 | oveq12d 7368 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π‘ β π· β (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) = (0 + (0 + 0))) |
420 | 414, 419,
404 | 3eqtr4a 2804 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π‘ β π· β (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) = if(π‘ β π·, ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))), 0)) |
421 | 411, 420 | pm2.61i 182 |
. . . . . . . . . . . . . 14
β’ (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) = if(π‘ β π·, ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + ((absβ(ββ(πΉβπ‘))) + (absβ(ββ(πΉβπ‘))))), 0) |
422 | 406, 421 | breqtrrdi 5146 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) |
423 | 422 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β π·, (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) |
424 | 327, 336,
347, 362, 423 | xrletrd 13010 |
. . . . . . . . . . 11
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) |
425 | 424 | ralrimivw 3146 |
. . . . . . . . . 10
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) |
426 | | fvex 6851 |
. . . . . . . . . . . . . 14
β’
(absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β V |
427 | 426, 17 | ifex 4535 |
. . . . . . . . . . . . 13
β’ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β V |
428 | 427 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β β) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β V) |
429 | | ovexd 7385 |
. . . . . . . . . . . 12
β’ ((π β§ π‘ β β) β (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) β V) |
430 | | eqidd 2739 |
. . . . . . . . . . . 12
β’ (π β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) = (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) |
431 | | ovexd 7385 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β β) β (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) β V) |
432 | 341 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β β) β if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) β β) |
433 | 342 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β β) β if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) β β) |
434 | | eqidd 2739 |
. . . . . . . . . . . . . 14
β’ (π β (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) = (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) |
435 | | eqidd 2739 |
. . . . . . . . . . . . . 14
β’ (π β (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) = (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) |
436 | 241, 432,
433, 434, 435 | offval2 7628 |
. . . . . . . . . . . . 13
β’ (π β ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) = (π‘ β β β¦ (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) |
437 | 241, 244,
431, 246, 436 | offval2 7628 |
. . . . . . . . . . . 12
β’ (π β ((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) = (π‘ β β β¦ (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))))) |
438 | 241, 428,
429, 430, 437 | ofrfval2 7629 |
. . . . . . . . . . 11
β’ (π β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) βr β€ ((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))))) |
439 | 438 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) βr β€ ((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ (if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + (if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) + if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))))) |
440 | 425, 439 | mpbird 257 |
. . . . . . . . 9
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) βr β€ ((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))))) |
441 | | itg2le 25026 |
. . . . . . . . 9
β’ (((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)):ββΆ(0[,]+β)
β§ ((π‘ β β
β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))):ββΆ(0[,]+β)
β§ (π‘ β β
β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) βr β€ ((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β€
(β«2β((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))))) |
442 | 276, 324,
440, 441 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β€
(β«2β((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))))) |
443 | 6 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β π· β
β) |
444 | 243 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β V) |
445 | | eldifn 4086 |
. . . . . . . . . . . . . 14
β’ (π‘ β (β β π·) β Β¬ π‘ β π·) |
446 | 445 | iffalsed 4496 |
. . . . . . . . . . . . 13
β’ (π‘ β (β β π·) β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) = 0) |
447 | 446 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β (β
β π·)) β if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) = 0) |
448 | | ovexd 7385 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (i Β· (πβπ‘)) β V) |
449 | 41, 42, 448, 45, 52 | offval2 7628 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π β dom
β«1) β (π βf + ((β Γ {i})
βf Β· π)) = (π‘ β β β¦ ((πβπ‘) + (i Β· (πβπ‘))))) |
450 | 39, 449, 56, 57 | fmptco 7070 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β (π βf + ((β Γ {i})
βf Β· π))) = (π‘ β β β¦ (absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
451 | 450 | reseq1d 5933 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β ((abs β (π βf + ((β Γ {i})
βf Β· π))) βΎ π·) = ((π‘ β β β¦ (absβ((πβπ‘) + (i Β· (πβπ‘))))) βΎ π·)) |
452 | 6 | resmptd 5991 |
. . . . . . . . . . . . . . 15
β’ (π β ((π‘ β β β¦ (absβ((πβπ‘) + (i Β· (πβπ‘))))) βΎ π·) = (π‘ β π· β¦ (absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
453 | 451, 452 | sylan9eqr 2800 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β ((abs β (π
βf + ((β Γ {i}) βf Β· π))) βΎ π·) = (π‘ β π· β¦ (absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
454 | 225 | mpteq2ia 5207 |
. . . . . . . . . . . . . 14
β’ (π‘ β π· β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) = (π‘ β π· β¦ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
455 | 453, 454 | eqtr4di 2796 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β ((abs β (π
βf + ((β Γ {i}) βf Β· π))) βΎ π·) = (π‘ β π· β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
456 | | i1fmbf 24961 |
. . . . . . . . . . . . . . 15
β’ ((abs
β (π
βf + ((β Γ {i}) βf Β· π))) β dom β«1
β (abs β (π
βf + ((β Γ {i}) βf Β· π))) β
MblFn) |
457 | 59, 456 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β (π βf + ((β Γ {i})
βf Β· π))) β MblFn) |
458 | 8 | fdmd 6675 |
. . . . . . . . . . . . . . 15
β’ (π β dom πΉ = π·) |
459 | | iblmbf 25054 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β πΏ1
β πΉ β
MblFn) |
460 | | mbfdm 24912 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β MblFn β dom πΉ β dom
vol) |
461 | 7, 459, 460 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β dom πΉ β dom vol) |
462 | 458, 461 | eqeltrrd 2840 |
. . . . . . . . . . . . . 14
β’ (π β π· β dom vol) |
463 | | mbfres 24930 |
. . . . . . . . . . . . . 14
β’ (((abs
β (π
βf + ((β Γ {i}) βf Β· π))) β MblFn β§ π· β dom vol) β ((abs
β (π
βf + ((β Γ {i}) βf Β· π))) βΎ π·) β MblFn) |
464 | 457, 462,
463 | syl2anr 598 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β ((abs β (π
βf + ((β Γ {i}) βf Β· π))) βΎ π·) β MblFn) |
465 | 455, 464 | eqeltrrd 2840 |
. . . . . . . . . . . 12
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (π‘ β π· β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β MblFn) |
466 | 443, 15, 444, 447, 465 | mbfss 24932 |
. . . . . . . . . . 11
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (π‘ β β
β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β MblFn) |
467 | 200 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
468 | | 0cnd 11082 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ π‘ β π·) β 0 β β) |
469 | 300, 468 | ifclda 4520 |
. . . . . . . . . . . . . . . . 17
β’ (π β if(π‘ β π·, (ββ(πΉβπ‘)), 0) β β) |
470 | 469 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π‘ β β) β if(π‘ β π·, (ββ(πΉβπ‘)), 0) β β) |
471 | | eqidd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π β (π‘ β β β¦ if(π‘ β π·, (ββ(πΉβπ‘)), 0)) = (π‘ β β β¦ if(π‘ β π·, (ββ(πΉβπ‘)), 0))) |
472 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β
abs:ββΆβ) |
473 | 472 | feqmptd 6906 |
. . . . . . . . . . . . . . . 16
β’ (π β abs = (π₯ β β β¦ (absβπ₯))) |
474 | | fveq2 6838 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = if(π‘ β π·, (ββ(πΉβπ‘)), 0) β (absβπ₯) = (absβif(π‘ β π·, (ββ(πΉβπ‘)), 0))) |
475 | | fvif 6854 |
. . . . . . . . . . . . . . . . . 18
β’
(absβif(π‘
β π·,
(ββ(πΉβπ‘)), 0)) = if(π‘ β π·, (absβ(ββ(πΉβπ‘))), (absβ0)) |
476 | | abs0 15105 |
. . . . . . . . . . . . . . . . . . 19
β’
(absβ0) = 0 |
477 | | ifeq2 4490 |
. . . . . . . . . . . . . . . . . . 19
β’
((absβ0) = 0 β if(π‘ β π·, (absβ(ββ(πΉβπ‘))), (absβ0)) = if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) |
478 | 476, 477 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), (absβ0)) = if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) |
479 | 475, 478 | eqtri 2766 |
. . . . . . . . . . . . . . . . 17
β’
(absβif(π‘
β π·,
(ββ(πΉβπ‘)), 0)) = if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0) |
480 | 474, 479 | eqtrdi 2794 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = if(π‘ β π·, (ββ(πΉβπ‘)), 0) β (absβπ₯) = if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) |
481 | 470, 471,
473, 480 | fmptco 7070 |
. . . . . . . . . . . . . . 15
β’ (π β (abs β (π‘ β β β¦ if(π‘ β π·, (ββ(πΉβπ‘)), 0))) = (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) |
482 | 299, 340 | ifclda 4520 |
. . . . . . . . . . . . . . . . . 18
β’ (π β if(π‘ β π·, (ββ(πΉβπ‘)), 0) β β) |
483 | 482 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π‘ β β) β if(π‘ β π·, (ββ(πΉβπ‘)), 0) β β) |
484 | 483 | fmpttd 7058 |
. . . . . . . . . . . . . . . 16
β’ (π β (π‘ β β β¦ if(π‘ β π·, (ββ(πΉβπ‘)),
0)):ββΆβ) |
485 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β dom
vol) |
486 | 482 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π‘ β π·) β if(π‘ β π·, (ββ(πΉβπ‘)), 0) β β) |
487 | 445 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π‘ β (β β π·)) β Β¬ π‘ β π·) |
488 | 487 | iffalsed 4496 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π‘ β (β β π·)) β if(π‘ β π·, (ββ(πΉβπ‘)), 0) = 0) |
489 | | iftrue 4491 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ β π· β if(π‘ β π·, (ββ(πΉβπ‘)), 0) = (ββ(πΉβπ‘))) |
490 | 489 | mpteq2ia 5207 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ β π· β¦ if(π‘ β π·, (ββ(πΉβπ‘)), 0)) = (π‘ β π· β¦ (ββ(πΉβπ‘))) |
491 | 8 | feqmptd 6906 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β πΉ = (π‘ β π· β¦ (πΉβπ‘))) |
492 | 7, 459 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β πΉ β MblFn) |
493 | 491, 492 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π‘ β π· β¦ (πΉβπ‘)) β MblFn) |
494 | 254 | ismbfcn2 24924 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π‘ β π· β¦ (πΉβπ‘)) β MblFn β ((π‘ β π· β¦ (ββ(πΉβπ‘))) β MblFn β§ (π‘ β π· β¦ (ββ(πΉβπ‘))) β MblFn))) |
495 | 493, 494 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π‘ β π· β¦ (ββ(πΉβπ‘))) β MblFn β§ (π‘ β π· β¦ (ββ(πΉβπ‘))) β MblFn)) |
496 | 495 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π‘ β π· β¦ (ββ(πΉβπ‘))) β MblFn) |
497 | 490, 496 | eqeltrid 2843 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π‘ β π· β¦ if(π‘ β π·, (ββ(πΉβπ‘)), 0)) β MblFn) |
498 | 6, 485, 486, 488, 497 | mbfss 24932 |
. . . . . . . . . . . . . . . 16
β’ (π β (π‘ β β β¦ if(π‘ β π·, (ββ(πΉβπ‘)), 0)) β MblFn) |
499 | | ftc1anclem1 36037 |
. . . . . . . . . . . . . . . 16
β’ (((π‘ β β β¦ if(π‘ β π·, (ββ(πΉβπ‘)), 0)):ββΆβ β§ (π‘ β β β¦ if(π‘ β π·, (ββ(πΉβπ‘)), 0)) β MblFn) β (abs β
(π‘ β β β¦
if(π‘ β π·, (ββ(πΉβπ‘)), 0))) β MblFn) |
500 | 484, 498,
499 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (abs β (π‘ β β β¦ if(π‘ β π·, (ββ(πΉβπ‘)), 0))) β MblFn) |
501 | 481, 500 | eqeltrrd 2840 |
. . . . . . . . . . . . . 14
β’ (π β (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) β MblFn) |
502 | 501, 308,
282, 317, 288 | itg2addnc 36018 |
. . . . . . . . . . . . 13
β’ (π β
(β«2β((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) = ((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))))) |
503 | 502, 289 | eqeltrd 2839 |
. . . . . . . . . . . 12
β’ (π β
(β«2β((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) β β) |
504 | 503 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (β«2β((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) β β) |
505 | 466, 297,
467, 319, 504 | itg2addnc 36018 |
. . . . . . . . . 10
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (β«2β((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))))) =
((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + (β«2β((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))))) |
506 | 502 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (β«2β((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))) = ((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))))) |
507 | 506 | oveq2d 7366 |
. . . . . . . . . 10
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β ((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + (β«2β((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))))) =
((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + ((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))))) |
508 | 505, 507 | eqtrd 2778 |
. . . . . . . . 9
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (β«2β((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))))) =
((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + ((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))))) |
509 | 508 | adantr 482 |
. . . . . . . 8
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β((π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + ((π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)) βf + (π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))))) =
((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + ((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))))) |
510 | 442, 509 | breqtrd 5130 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β€
((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + ((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))))) |
511 | | itg2lecl 25025 |
. . . . . . 7
β’ (((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)):ββΆ(0[,]+β)
β§ ((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + ((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))))) β β β§
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β€
((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + ((β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(ββ(πΉβπ‘))), 0)))))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β β) |
512 | 276, 291,
510, 511 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β β) |
513 | 69, 78, 253, 269, 512 | itg2addnc 36018 |
. . . . 5
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) =
((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))))) |
514 | 241, 242,
428, 245, 430 | offval2 7628 |
. . . . . . . . 9
β’ (π β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) = (π‘ β β β¦ (if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) |
515 | | eqeq2 2750 |
. . . . . . . . . . 11
β’
(((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) = if(π‘ β (π’(,)π€), ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))), 0) β ((if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) = ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) β (if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) = if(π‘ β (π’(,)π€), ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))), 0))) |
516 | | eqeq2 2750 |
. . . . . . . . . . 11
β’ (0 =
if(π‘ β (π’(,)π€), ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))), 0) β ((if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) = 0 β (if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) = if(π‘ β (π’(,)π€), ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))), 0))) |
517 | | iftrue 4491 |
. . . . . . . . . . . . 13
β’ (π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) = (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
518 | 23, 517 | oveq12d 7368 |
. . . . . . . . . . . 12
β’ (π‘ β (π’(,)π€) β (if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) = ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))))) |
519 | 518 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β (π’(,)π€)) β (if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) = ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))))) |
520 | | iffalse 4494 |
. . . . . . . . . . . . . 14
β’ (Β¬
π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) = 0) |
521 | | iffalse 4494 |
. . . . . . . . . . . . . 14
β’ (Β¬
π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) = 0) |
522 | 520, 521 | oveq12d 7368 |
. . . . . . . . . . . . 13
β’ (Β¬
π‘ β (π’(,)π€) β (if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) = (0 + 0)) |
523 | 522, 412 | eqtrdi 2794 |
. . . . . . . . . . . 12
β’ (Β¬
π‘ β (π’(,)π€) β (if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) = 0) |
524 | 523 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ π‘ β (π’(,)π€)) β (if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) = 0) |
525 | 515, 516,
519, 524 | ifbothda 4523 |
. . . . . . . . . 10
β’ (π β (if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) = if(π‘ β (π’(,)π€), ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))), 0)) |
526 | 525 | mpteq2dv 5206 |
. . . . . . . . 9
β’ (π β (π‘ β β β¦ (if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) + if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) = (π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))), 0))) |
527 | 514, 526 | eqtrd 2778 |
. . . . . . . 8
β’ (π β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) = (π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))), 0))) |
528 | 527 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) = (π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))), 0))) |
529 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π β dom β«1 β§ π β dom
β«1)) |
530 | 258 | abscld 15256 |
. . . . . . . . . . . 12
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β (π’(,)π€)) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
531 | 530 | recnd 11117 |
. . . . . . . . . . 11
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β (π’(,)π€)) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
532 | 529, 531 | sylan 581 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
533 | 262 | recnd 11117 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β β) |
534 | 532, 533 | addcomd 11291 |
. . . . . . . . 9
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) = ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
535 | 534 | ifeq1da 4516 |
. . . . . . . 8
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β (π’(,)π€), ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))), 0) = if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)) |
536 | 535 | mpteq2dv 5206 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πβπ‘) + (i Β· (πβπ‘)))) + (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))), 0)) = (π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) |
537 | 528, 536 | eqtrd 2778 |
. . . . . 6
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) = (π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) |
538 | 537 | fveq2d 6842 |
. . . . 5
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βf + (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) =
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) |
539 | 513, 538 | eqtr3d 2780 |
. . . 4
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) =
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) |
540 | 10, 11, 539 | syl2an 597 |
. . 3
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β ((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) =
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) |
541 | 540 | adantr 482 |
. 2
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) =
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) |
542 | | rpcn 12854 |
. . . 4
β’ (π¦ β β+
β π¦ β
β) |
543 | 542 | 2halvesd 12333 |
. . 3
β’ (π¦ β β+
β ((π¦ / 2) + (π¦ / 2)) = π¦) |
544 | 543 | ad3antlr 730 |
. 2
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
((π¦ / 2) + (π¦ / 2)) = π¦) |
545 | 9, 541, 544 | 3brtr3d 5135 |
1
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) < π¦) |