Step | Hyp | Ref
| Expression |
1 | | i1ff 24962 |
. . . . . . . . . . 11
β’ (π β dom β«1
β π:ββΆβ) |
2 | 1 | ffvelcdmda 7030 |
. . . . . . . . . 10
β’ ((π β dom β«1
β§ π₯ β β)
β (πβπ₯) β
β) |
3 | 2 | recnd 11117 |
. . . . . . . . 9
β’ ((π β dom β«1
β§ π₯ β β)
β (πβπ₯) β
β) |
4 | | ax-icn 11044 |
. . . . . . . . . 10
β’ i β
β |
5 | | i1ff 24962 |
. . . . . . . . . . . 12
β’ (π β dom β«1
β π:ββΆβ) |
6 | 5 | ffvelcdmda 7030 |
. . . . . . . . . . 11
β’ ((π β dom β«1
β§ π₯ β β)
β (πβπ₯) β
β) |
7 | 6 | recnd 11117 |
. . . . . . . . . 10
β’ ((π β dom β«1
β§ π₯ β β)
β (πβπ₯) β
β) |
8 | | mulcl 11069 |
. . . . . . . . . 10
β’ ((i
β β β§ (πβπ₯) β β) β (i Β· (πβπ₯)) β β) |
9 | 4, 7, 8 | sylancr 588 |
. . . . . . . . 9
β’ ((π β dom β«1
β§ π₯ β β)
β (i Β· (πβπ₯)) β β) |
10 | | addcl 11067 |
. . . . . . . . 9
β’ (((πβπ₯) β β β§ (i Β· (πβπ₯)) β β) β ((πβπ₯) + (i Β· (πβπ₯))) β β) |
11 | 3, 9, 10 | syl2an 597 |
. . . . . . . 8
β’ (((π β dom β«1
β§ π₯ β β)
β§ (π β dom
β«1 β§ π₯
β β)) β ((πβπ₯) + (i Β· (πβπ₯))) β β) |
12 | 11 | anandirs 678 |
. . . . . . 7
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π₯
β β) β ((πβπ₯) + (i Β· (πβπ₯))) β β) |
13 | | reex 11076 |
. . . . . . . . 9
β’ β
β V |
14 | 13 | a1i 11 |
. . . . . . . 8
β’ ((π β dom β«1
β§ π β dom
β«1) β β β V) |
15 | 2 | adantlr 714 |
. . . . . . . 8
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π₯
β β) β (πβπ₯) β β) |
16 | | ovexd 7385 |
. . . . . . . 8
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π₯
β β) β (i Β· (πβπ₯)) β V) |
17 | 1 | feqmptd 6906 |
. . . . . . . . 9
β’ (π β dom β«1
β π = (π₯ β β β¦ (πβπ₯))) |
18 | 17 | adantr 482 |
. . . . . . . 8
β’ ((π β dom β«1
β§ π β dom
β«1) β π
= (π₯ β β β¦
(πβπ₯))) |
19 | 13 | a1i 11 |
. . . . . . . . . 10
β’ (π β dom β«1
β β β V) |
20 | 4 | a1i 11 |
. . . . . . . . . 10
β’ ((π β dom β«1
β§ π₯ β β)
β i β β) |
21 | | fconstmpt 5691 |
. . . . . . . . . . 11
β’ (β
Γ {i}) = (π₯ β
β β¦ i) |
22 | 21 | a1i 11 |
. . . . . . . . . 10
β’ (π β dom β«1
β (β Γ {i}) = (π₯ β β β¦ i)) |
23 | 5 | feqmptd 6906 |
. . . . . . . . . 10
β’ (π β dom β«1
β π = (π₯ β β β¦ (πβπ₯))) |
24 | 19, 20, 6, 22, 23 | offval2 7628 |
. . . . . . . . 9
β’ (π β dom β«1
β ((β Γ {i}) βf Β· π) = (π₯ β β β¦ (i Β· (πβπ₯)))) |
25 | 24 | adantl 483 |
. . . . . . . 8
β’ ((π β dom β«1
β§ π β dom
β«1) β ((β Γ {i}) βf Β·
π) = (π₯ β β β¦ (i Β· (πβπ₯)))) |
26 | 14, 15, 16, 18, 25 | offval2 7628 |
. . . . . . 7
β’ ((π β dom β«1
β§ π β dom
β«1) β (π βf + ((β Γ {i})
βf Β· π)) = (π₯ β β β¦ ((πβπ₯) + (i Β· (πβπ₯))))) |
27 | | absf 15157 |
. . . . . . . . 9
β’
abs:ββΆβ |
28 | 27 | a1i 11 |
. . . . . . . 8
β’ ((π β dom β«1
β§ π β dom
β«1) β abs:ββΆβ) |
29 | 28 | feqmptd 6906 |
. . . . . . 7
β’ ((π β dom β«1
β§ π β dom
β«1) β abs = (π‘ β β β¦ (absβπ‘))) |
30 | | fveq2 6838 |
. . . . . . 7
β’ (π‘ = ((πβπ₯) + (i Β· (πβπ₯))) β (absβπ‘) = (absβ((πβπ₯) + (i Β· (πβπ₯))))) |
31 | 12, 26, 29, 30 | fmptco 7070 |
. . . . . 6
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β (π βf + ((β Γ {i})
βf Β· π))) = (π₯ β β β¦ (absβ((πβπ₯) + (i Β· (πβπ₯)))))) |
32 | | ftc1anclem3 36039 |
. . . . . 6
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β (π βf + ((β Γ {i})
βf Β· π))) β dom
β«1) |
33 | 31, 32 | eqeltrrd 2840 |
. . . . 5
β’ ((π β dom β«1
β§ π β dom
β«1) β (π₯ β β β¦ (absβ((πβπ₯) + (i Β· (πβπ₯))))) β dom
β«1) |
34 | | ioombl 24851 |
. . . . 5
β’ (π’(,)π€) β dom vol |
35 | | fveq2 6838 |
. . . . . . . . . . . 12
β’ (π₯ = π‘ β (πβπ₯) = (πβπ‘)) |
36 | | fveq2 6838 |
. . . . . . . . . . . . 13
β’ (π₯ = π‘ β (πβπ₯) = (πβπ‘)) |
37 | 36 | oveq2d 7366 |
. . . . . . . . . . . 12
β’ (π₯ = π‘ β (i Β· (πβπ₯)) = (i Β· (πβπ‘))) |
38 | 35, 37 | oveq12d 7368 |
. . . . . . . . . . 11
β’ (π₯ = π‘ β ((πβπ₯) + (i Β· (πβπ₯))) = ((πβπ‘) + (i Β· (πβπ‘)))) |
39 | 38 | fveq2d 6842 |
. . . . . . . . . 10
β’ (π₯ = π‘ β (absβ((πβπ₯) + (i Β· (πβπ₯)))) = (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
40 | | eqid 2738 |
. . . . . . . . . 10
β’ (π₯ β β β¦
(absβ((πβπ₯) + (i Β· (πβπ₯))))) = (π₯ β β β¦ (absβ((πβπ₯) + (i Β· (πβπ₯))))) |
41 | | fvex 6851 |
. . . . . . . . . 10
β’
(absβ((πβπ‘) + (i Β· (πβπ‘)))) β V |
42 | 39, 40, 41 | fvmpt 6944 |
. . . . . . . . 9
β’ (π‘ β β β ((π₯ β β β¦
(absβ((πβπ₯) + (i Β· (πβπ₯)))))βπ‘) = (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
43 | 42 | eqcomd 2744 |
. . . . . . . 8
β’ (π‘ β β β
(absβ((πβπ‘) + (i Β· (πβπ‘)))) = ((π₯ β β β¦ (absβ((πβπ₯) + (i Β· (πβπ₯)))))βπ‘)) |
44 | 43 | ifeq1d 4504 |
. . . . . . 7
β’ (π‘ β β β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) = if(π‘ β (π’(,)π€), ((π₯ β β β¦ (absβ((πβπ₯) + (i Β· (πβπ₯)))))βπ‘), 0)) |
45 | 44 | mpteq2ia 5207 |
. . . . . 6
β’ (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) = (π‘ β β β¦ if(π‘ β (π’(,)π€), ((π₯ β β β¦ (absβ((πβπ₯) + (i Β· (πβπ₯)))))βπ‘), 0)) |
46 | 45 | i1fres 24992 |
. . . . 5
β’ (((π₯ β β β¦
(absβ((πβπ₯) + (i Β· (πβπ₯))))) β dom β«1 β§
(π’(,)π€) β dom vol) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β dom
β«1) |
47 | 33, 34, 46 | sylancl 587 |
. . . 4
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β dom
β«1) |
48 | | breq2 5108 |
. . . . . . 7
β’
((absβ((πβπ‘) + (i Β· (πβπ‘)))) = if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β (0 β€ (absβ((πβπ‘) + (i Β· (πβπ‘)))) β 0 β€ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
49 | | breq2 5108 |
. . . . . . 7
β’ (0 =
if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β (0 β€ 0 β 0 β€
if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
50 | | elioore 13223 |
. . . . . . . 8
β’ (π‘ β (π’(,)π€) β π‘ β β) |
51 | | eleq1w 2821 |
. . . . . . . . . . . 12
β’ (π₯ = π‘ β (π₯ β β β π‘ β β)) |
52 | 51 | anbi2d 630 |
. . . . . . . . . . 11
β’ (π₯ = π‘ β (((π β dom β«1 β§ π β dom β«1)
β§ π₯ β β)
β ((π β dom
β«1 β§ π
β dom β«1) β§ π‘ β β))) |
53 | 38 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (π₯ = π‘ β (((πβπ₯) + (i Β· (πβπ₯))) β β β ((πβπ‘) + (i Β· (πβπ‘))) β β)) |
54 | 52, 53 | imbi12d 345 |
. . . . . . . . . 10
β’ (π₯ = π‘ β ((((π β dom β«1 β§ π β dom β«1)
β§ π₯ β β)
β ((πβπ₯) + (i Β· (πβπ₯))) β β) β (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β ((πβπ‘) + (i Β· (πβπ‘))) β β))) |
55 | 54, 12 | chvarvv 2003 |
. . . . . . . . 9
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
56 | 55 | absge0d 15264 |
. . . . . . . 8
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β 0 β€ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
57 | 50, 56 | sylan2 594 |
. . . . . . 7
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β (π’(,)π€)) β 0 β€
(absβ((πβπ‘) + (i Β· (πβπ‘))))) |
58 | | 0le0 12188 |
. . . . . . . 8
β’ 0 β€
0 |
59 | 58 | a1i 11 |
. . . . . . 7
β’ (((π β dom β«1
β§ π β dom
β«1) β§ Β¬ π‘ β (π’(,)π€)) β 0 β€ 0) |
60 | 48, 49, 57, 59 | ifbothda 4523 |
. . . . . 6
β’ ((π β dom β«1
β§ π β dom
β«1) β 0 β€ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) |
61 | 60 | ralrimivw 3146 |
. . . . 5
β’ ((π β dom β«1
β§ π β dom
β«1) β βπ‘ β β 0 β€ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) |
62 | | ax-resscn 11042 |
. . . . . . . 8
β’ β
β β |
63 | 62 | a1i 11 |
. . . . . . 7
β’ ((π β dom β«1
β§ π β dom
β«1) β β β β) |
64 | | c0ex 11083 |
. . . . . . . . . 10
β’ 0 β
V |
65 | 41, 64 | ifex 4535 |
. . . . . . . . 9
β’ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β V |
66 | | eqid 2738 |
. . . . . . . . 9
β’ (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) = (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) |
67 | 65, 66 | fnmpti 6640 |
. . . . . . . 8
β’ (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) Fn β |
68 | 67 | a1i 11 |
. . . . . . 7
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) Fn β) |
69 | 63, 68 | 0pledm 24959 |
. . . . . 6
β’ ((π β dom β«1
β§ π β dom
β«1) β (0π βr β€
(π‘ β β β¦
if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β (β Γ {0})
βr β€ (π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)))) |
70 | 64 | a1i 11 |
. . . . . . 7
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β 0 β V) |
71 | 65 | a1i 11 |
. . . . . . 7
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β V) |
72 | | fconstmpt 5691 |
. . . . . . . 8
β’ (β
Γ {0}) = (π‘ β
β β¦ 0) |
73 | 72 | a1i 11 |
. . . . . . 7
β’ ((π β dom β«1
β§ π β dom
β«1) β (β Γ {0}) = (π‘ β β β¦ 0)) |
74 | | eqidd 2739 |
. . . . . . 7
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) = (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
75 | 14, 70, 71, 73, 74 | ofrfval2 7629 |
. . . . . 6
β’ ((π β dom β«1
β§ π β dom
β«1) β ((β Γ {0}) βr β€
(π‘ β β β¦
if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β βπ‘ β β 0 β€ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
76 | 69, 75 | bitrd 279 |
. . . . 5
β’ ((π β dom β«1
β§ π β dom
β«1) β (0π βr β€
(π‘ β β β¦
if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β βπ‘ β β 0 β€ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
77 | 61, 76 | mpbird 257 |
. . . 4
β’ ((π β dom β«1
β§ π β dom
β«1) β 0π βr β€ (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) |
78 | | itg2itg1 25023 |
. . . . 5
β’ (((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β dom β«1 β§
0π βr β€ (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) = (β«1β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)))) |
79 | | itg1cl 24971 |
. . . . . 6
β’ ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β dom β«1 β
(β«1β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
80 | 79 | adantr 482 |
. . . . 5
β’ (((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β dom β«1 β§
0π βr β€ (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β
(β«1β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
81 | 78, 80 | eqeltrd 2839 |
. . . 4
β’ (((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) β dom β«1 β§
0π βr β€ (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
82 | 47, 77, 81 | syl2anc 585 |
. . 3
β’ ((π β dom β«1
β§ π β dom
β«1) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
83 | 82 | ad6antlr 736 |
. 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))) β β) |
84 | | simplll 774 |
. . . . 5
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β (π β§ (π β dom β«1 β§ π β dom
β«1))) |
85 | | ftc1anc.a |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΄ β β) |
86 | 85 | rexrd 11139 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΄ β
β*) |
87 | | ftc1anc.b |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΅ β β) |
88 | 87 | rexrd 11139 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΅ β
β*) |
89 | 86, 88 | jca 513 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄ β β* β§ π΅ β
β*)) |
90 | | df-icc 13200 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ [,] =
(π₯ β
β*, π¦
β β* β¦ {π‘ β β* β£ (π₯ β€ π‘ β§ π‘ β€ π¦)}) |
91 | 90 | elixx3g 13206 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π’ β (π΄[,]π΅) β ((π΄ β β* β§ π΅ β β*
β§ π’ β
β*) β§ (π΄ β€ π’ β§ π’ β€ π΅))) |
92 | 91 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π’ β (π΄[,]π΅) β (π΄ β€ π’ β§ π’ β€ π΅)) |
93 | 92 | simpld 496 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ β (π΄[,]π΅) β π΄ β€ π’) |
94 | 90 | elixx3g 13206 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β (π΄[,]π΅) β ((π΄ β β* β§ π΅ β β*
β§ π€ β
β*) β§ (π΄ β€ π€ β§ π€ β€ π΅))) |
95 | 94 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ β (π΄[,]π΅) β (π΄ β€ π€ β§ π€ β€ π΅)) |
96 | 95 | simprd 497 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ β (π΄[,]π΅) β π€ β€ π΅) |
97 | 93, 96 | anim12i 614 |
. . . . . . . . . . . . . . . . . 18
β’ ((π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅)) β (π΄ β€ π’ β§ π€ β€ π΅)) |
98 | | ioossioo 13287 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β β*
β§ π΅ β
β*) β§ (π΄ β€ π’ β§ π€ β€ π΅)) β (π’(,)π€) β (π΄(,)π΅)) |
99 | 89, 97, 98 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π’(,)π€) β (π΄(,)π΅)) |
100 | | ftc1anc.s |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄(,)π΅) β π·) |
101 | 100 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π΄(,)π΅) β π·) |
102 | 99, 101 | sstrd 3953 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π’(,)π€) β π·) |
103 | 102 | 3adantr3 1172 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (π’(,)π€) β π·) |
104 | 103 | sselda 3943 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β (π’(,)π€)) β π‘ β π·) |
105 | | ftc1anc.f |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:π·βΆβ) |
106 | 105 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π‘ β π·) β (πΉβπ‘) β β) |
107 | 106 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β π·) β (πΉβπ‘) β β) |
108 | 104, 107 | syldan 592 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β (π’(,)π€)) β (πΉβπ‘) β β) |
109 | 108 | adantllr 718 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β (π’(,)π€)) β (πΉβπ‘) β β) |
110 | 55 | adantll 713 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β β)
β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
111 | 50, 110 | sylan2 594 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β (π’(,)π€)) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
112 | 111 | adantlr 714 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β (π’(,)π€)) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
113 | 109, 112 | subcld 11446 |
. . . . . . . . . . 11
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β (π’(,)π€)) β ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
114 | 113 | abscld 15256 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β β) |
115 | 114 | rexrd 11139 |
. . . . . . . . 9
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β
β*) |
116 | 113 | absge0d 15264 |
. . . . . . . . 9
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β (π’(,)π€)) β 0 β€ (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
117 | | elxrge0 13303 |
. . . . . . . . 9
β’
((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β (0[,]+β) β
((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β β* β§ 0 β€
(absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))))) |
118 | 115, 116,
117 | sylanbrc 584 |
. . . . . . . 8
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β (0[,]+β)) |
119 | | 0e0iccpnf 13305 |
. . . . . . . . 9
β’ 0 β
(0[,]+β) |
120 | 119 | a1i 11 |
. . . . . . . 8
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ Β¬ π‘ β (π’(,)π€)) β 0 β
(0[,]+β)) |
121 | 118, 120 | ifclda 4520 |
. . . . . . 7
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β
(0[,]+β)) |
122 | 121 | adantr 482 |
. . . . . 6
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β β) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β
(0[,]+β)) |
123 | 122 | fmpttd 7058 |
. . . . 5
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))),
0)):ββΆ(0[,]+β)) |
124 | 84, 123 | sylan 581 |
. . . 4
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))),
0)):ββΆ(0[,]+β)) |
125 | | rpre 12852 |
. . . . . 6
β’ (π¦ β β+
β π¦ β
β) |
126 | 125 | rehalfcld 12334 |
. . . . 5
β’ (π¦ β β+
β (π¦ / 2) β
β) |
127 | 126 | ad2antlr 726 |
. . . 4
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (π¦ / 2) β β) |
128 | | simpll 766 |
. . . . . . . 8
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ π¦ β β+) β (π β§ (π β dom β«1 β§ π β dom
β«1))) |
129 | 102 | sselda 3943 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β π‘ β π·) |
130 | 129 | adantllr 718 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β π‘ β π·) |
131 | 106 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (πΉβπ‘) β β) |
132 | | ftc1anc.d |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π· β β) |
133 | 132 | sselda 3943 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π‘ β π·) β π‘ β β) |
134 | 133 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β π‘ β β) |
135 | 134, 110 | syldan 592 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
136 | 131, 135 | subcld 11446 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
137 | 136 | abscld 15256 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β β) |
138 | 137 | rexrd 11139 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β
β*) |
139 | 138 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β π·) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β
β*) |
140 | 130, 139 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β
β*) |
141 | 136 | absge0d 15264 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β 0 β€
(absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
142 | 141 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β π·) β 0 β€ (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
143 | 130, 142 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β 0 β€ (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
144 | 140, 143,
117 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β (0[,]+β)) |
145 | 119 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ Β¬ π‘ β (π’(,)π€)) β 0 β
(0[,]+β)) |
146 | 144, 145 | ifclda 4520 |
. . . . . . . . . . 11
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β
(0[,]+β)) |
147 | 146 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β β) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β
(0[,]+β)) |
148 | 147 | fmpttd 7058 |
. . . . . . . . 9
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))),
0)):ββΆ(0[,]+β)) |
149 | | itg2cl 25019 |
. . . . . . . . 9
β’ ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)):ββΆ(0[,]+β)
β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β
β*) |
150 | 148, 149 | syl 17 |
. . . . . . . 8
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β
β*) |
151 | 128, 150 | sylan 581 |
. . . . . . 7
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β
β*) |
152 | | rphalfcl 12871 |
. . . . . . . . 9
β’ (π¦ β β+
β (π¦ / 2) β
β+) |
153 | 152 | rpxrd 12887 |
. . . . . . . 8
β’ (π¦ β β+
β (π¦ / 2) β
β*) |
154 | 153 | ad2antlr 726 |
. . . . . . 7
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π¦ / 2) β
β*) |
155 | | 0cnd 11082 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ π‘ β π·) β 0 β β) |
156 | 106, 155 | ifclda 4520 |
. . . . . . . . . . . . . . . 16
β’ (π β if(π‘ β π·, (πΉβπ‘), 0) β β) |
157 | | subcl 11334 |
. . . . . . . . . . . . . . . 16
β’
((if(π‘ β π·, (πΉβπ‘), 0) β β β§ ((πβπ‘) + (i Β· (πβπ‘))) β β) β (if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
158 | 156, 55, 157 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π β dom β«1 β§ π β dom β«1)
β§ π‘ β β))
β (if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
159 | 158 | anassrs 469 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β β)
β (if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
160 | 159 | abscld 15256 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β β)
β (absβ(if(π‘
β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))) β β) |
161 | 160 | rexrd 11139 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β β)
β (absβ(if(π‘
β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))) β
β*) |
162 | 159 | absge0d 15264 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β β)
β 0 β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
163 | | elxrge0 13303 |
. . . . . . . . . . . 12
β’
((absβ(if(π‘
β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))) β (0[,]+β) β
((absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))) β β* β§ 0 β€
(absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) |
164 | 161, 162,
163 | sylanbrc 584 |
. . . . . . . . . . 11
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β β)
β (absβ(if(π‘
β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))) β (0[,]+β)) |
165 | 164 | fmpttd 7058 |
. . . . . . . . . 10
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (π‘ β β
β¦ (absβ(if(π‘
β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))):ββΆ(0[,]+β)) |
166 | | itg2cl 25019 |
. . . . . . . . . 10
β’ ((π‘ β β β¦
(absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))):ββΆ(0[,]+β) β
(β«2β(π‘
β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) β
β*) |
167 | 165, 166 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) β
β*) |
168 | 167 | ad3antrrr 729 |
. . . . . . . 8
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦
(absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) β
β*) |
169 | 165 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))):ββΆ(0[,]+β)) |
170 | | breq1 5107 |
. . . . . . . . . . . . 13
β’
((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) = if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) |
171 | | breq1 5107 |
. . . . . . . . . . . . 13
β’ (0 =
if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β (0 β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) |
172 | 137 | leidd 11655 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β€ (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
173 | | iftrue 4491 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ β π· β if(π‘ β π·, (πΉβπ‘), 0) = (πΉβπ‘)) |
174 | 173 | fvoveq1d 7372 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ β π· β (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))) = (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
175 | 174 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))) = (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
176 | 172, 175 | breqtrrd 5132 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β π·) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
177 | 176 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β π·) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
178 | 130, 177 | syldan 592 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
179 | 178 | adantlr 714 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β β) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
180 | 162 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β β) β 0 β€
(absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
181 | 180 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β β) β§ Β¬ π‘ β (π’(,)π€)) β 0 β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
182 | 170, 171,
179, 181 | ifbothda 4523 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β β) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
183 | 182 | ralrimiva 3142 |
. . . . . . . . . . 11
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
184 | 13 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β β β
V) |
185 | | fvex 6851 |
. . . . . . . . . . . . . . 15
β’
(absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β V |
186 | 185, 64 | ifex 4535 |
. . . . . . . . . . . . . 14
β’ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β V |
187 | 186 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β β) β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β V) |
188 | | fvexd 6853 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β β) β (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))) β V) |
189 | | eqidd 2739 |
. . . . . . . . . . . . 13
β’ (π β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) = (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) |
190 | | eqidd 2739 |
. . . . . . . . . . . . 13
β’ (π β (π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))) = (π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) |
191 | 184, 187,
188, 189, 190 | ofrfval2 7629 |
. . . . . . . . . . . 12
β’ (π β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) βr β€ (π‘ β β β¦
(absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) |
192 | 191 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) βr β€ (π‘ β β β¦
(absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0) β€ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) |
193 | 183, 192 | mpbird 257 |
. . . . . . . . . 10
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) βr β€ (π‘ β β β¦
(absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) |
194 | | itg2le 25026 |
. . . . . . . . . 10
β’ (((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)):ββΆ(0[,]+β)
β§ (π‘ β β
β¦ (absβ(if(π‘
β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))):ββΆ(0[,]+β) β§
(π‘ β β β¦
if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)) βr β€ (π‘ β β β¦
(absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β€
(β«2β(π‘
β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))))) |
195 | 148, 169,
193, 194 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β€
(β«2β(π‘
β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))))) |
196 | 128, 195 | sylan 581 |
. . . . . . . 8
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β€
(β«2β(π‘
β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))))) |
197 | | simpllr 775 |
. . . . . . . 8
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦
(absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) |
198 | 151, 168,
154, 196, 197 | xrlelttrd 13008 |
. . . . . . 7
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) < (π¦ / 2)) |
199 | 151, 154,
198 | xrltled 12998 |
. . . . . 6
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β€ (π¦ / 2)) |
200 | 199 | adantllr 718 |
. . . . 5
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β€ (π¦ / 2)) |
201 | 200 | 3adantr3 1172 |
. . . 4
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β€ (π¦ / 2)) |
202 | | itg2lecl 25025 |
. . . 4
β’ (((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)):ββΆ(0[,]+β)
β§ (π¦ / 2) β
β β§ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β€ (π¦ / 2)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β β) |
203 | 124, 127,
201, 202 | syl3anc 1372 |
. . 3
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β β) |
204 | 203 | 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))) β β) |
205 | 126 | ad3antlr 730 |
. 2
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
(π¦ / 2) β
β) |
206 | 82 | adantr 482 |
. . . . . . . 8
β’ (((π β dom β«1
β§ π β dom
β«1) β§ βπ β (ran π βͺ ran π)π β 0) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
207 | | 2rp 12849 |
. . . . . . . . 9
β’ 2 β
β+ |
208 | | imassrn 6021 |
. . . . . . . . . . . . . . . 16
β’ (abs
β (ran π βͺ ran
π)) β ran
abs |
209 | | frn 6671 |
. . . . . . . . . . . . . . . . 17
β’
(abs:ββΆβ β ran abs β
β) |
210 | 27, 209 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ ran abs
β β |
211 | 208, 210 | sstri 3952 |
. . . . . . . . . . . . . . 15
β’ (abs
β (ran π βͺ ran
π)) β
β |
212 | 211 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β (ran π βͺ ran π)) β β) |
213 | 1 | frnd 6672 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β dom β«1
β ran π β
β) |
214 | 213 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β dom β«1
β§ π β dom
β«1) β ran π β β) |
215 | 5 | frnd 6672 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β dom β«1
β ran π β
β) |
216 | 215 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β dom β«1
β§ π β dom
β«1) β ran π β β) |
217 | 214, 216 | unssd 4145 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π β dom
β«1) β (ran π βͺ ran π) β β) |
218 | 217, 62 | sstrdi 3955 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π β dom
β«1) β (ran π βͺ ran π) β β) |
219 | | i1f0rn 24968 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom β«1
β 0 β ran π) |
220 | | elun1 4135 |
. . . . . . . . . . . . . . . . . 18
β’ (0 β
ran π β 0 β (ran
π βͺ ran π)) |
221 | 219, 220 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom β«1
β 0 β (ran π
βͺ ran π)) |
222 | 221 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π β dom
β«1) β 0 β (ran π βͺ ran π)) |
223 | | ffn 6664 |
. . . . . . . . . . . . . . . . . 18
β’
(abs:ββΆβ β abs Fn β) |
224 | 27, 223 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ abs Fn
β |
225 | | fnfvima 7178 |
. . . . . . . . . . . . . . . . 17
β’ ((abs Fn
β β§ (ran π βͺ
ran π) β β
β§ 0 β (ran π βͺ
ran π)) β
(absβ0) β (abs β (ran π βͺ ran π))) |
226 | 224, 225 | mp3an1 1449 |
. . . . . . . . . . . . . . . 16
β’ (((ran
π βͺ ran π) β β β§ 0 β
(ran π βͺ ran π)) β (absβ0) β
(abs β (ran π βͺ
ran π))) |
227 | 218, 222,
226 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β (absβ0) β (abs β (ran π βͺ ran π))) |
228 | 227 | ne0d 4294 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β (ran π βͺ ran π)) β β
) |
229 | | ffun 6667 |
. . . . . . . . . . . . . . . . 17
β’
(abs:ββΆβ β Fun abs) |
230 | 27, 229 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ Fun
abs |
231 | | i1frn 24963 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom β«1
β ran π β
Fin) |
232 | | i1frn 24963 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom β«1
β ran π β
Fin) |
233 | | unfi 9050 |
. . . . . . . . . . . . . . . . 17
β’ ((ran
π β Fin β§ ran
π β Fin) β (ran
π βͺ ran π) β Fin) |
234 | 231, 232,
233 | syl2an 597 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π β dom
β«1) β (ran π βͺ ran π) β Fin) |
235 | | imafi 9053 |
. . . . . . . . . . . . . . . 16
β’ ((Fun abs
β§ (ran π βͺ ran
π) β Fin) β (abs
β (ran π βͺ ran
π)) β
Fin) |
236 | 230, 234,
235 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β (ran π βͺ ran π)) β Fin) |
237 | | fimaxre2 12034 |
. . . . . . . . . . . . . . 15
β’ (((abs
β (ran π βͺ ran
π)) β β β§
(abs β (ran π βͺ
ran π)) β Fin) β
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯) |
238 | 211, 236,
237 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π β dom
β«1) β βπ₯ β β βπ¦ β (abs β (ran π βͺ ran π))π¦ β€ π₯) |
239 | | suprcl 12049 |
. . . . . . . . . . . . . 14
β’ (((abs
β (ran π βͺ ran
π)) β β β§
(abs β (ran π βͺ
ran π)) β β
β§
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯) β sup((abs β (ran π βͺ ran π)), β, < ) β
β) |
240 | 212, 228,
238, 239 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β dom β«1
β§ π β dom
β«1) β sup((abs β (ran π βͺ ran π)), β, < ) β
β) |
241 | 240 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π
β (ran π βͺ ran
π) β§ π β 0)) β sup((abs β (ran π βͺ ran π)), β, < ) β
β) |
242 | | 0red 11092 |
. . . . . . . . . . . . 13
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π
β (ran π βͺ ran
π) β§ π β 0)) β 0 β
β) |
243 | 218 | sselda 3943 |
. . . . . . . . . . . . . . 15
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β π β
β) |
244 | 243 | abscld 15256 |
. . . . . . . . . . . . . 14
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β (absβπ) β
β) |
245 | 244 | adantrr 716 |
. . . . . . . . . . . . 13
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π
β (ran π βͺ ran
π) β§ π β 0)) β (absβπ) β
β) |
246 | | absgt0 15144 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π β 0 β 0 <
(absβπ))) |
247 | 243, 246 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β (π β 0 β 0 <
(absβπ))) |
248 | 247 | biimpa 478 |
. . . . . . . . . . . . . 14
β’ ((((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β§ π β 0) β 0 <
(absβπ)) |
249 | 248 | anasss 468 |
. . . . . . . . . . . . 13
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π
β (ran π βͺ ran
π) β§ π β 0)) β 0 < (absβπ)) |
250 | 212, 228,
238 | 3jca 1129 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π β dom
β«1) β ((abs β (ran π βͺ ran π)) β β β§ (abs β (ran
π βͺ ran π)) β β
β§
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯)) |
251 | 250 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β ((abs β
(ran π βͺ ran π)) β β β§ (abs
β (ran π βͺ ran
π)) β β
β§
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯)) |
252 | | fnfvima 7178 |
. . . . . . . . . . . . . . . . 17
β’ ((abs Fn
β β§ (ran π βͺ
ran π) β β
β§ π β (ran π βͺ ran π)) β (absβπ) β (abs β (ran π βͺ ran π))) |
253 | 224, 252 | mp3an1 1449 |
. . . . . . . . . . . . . . . 16
β’ (((ran
π βͺ ran π) β β β§ π β (ran π βͺ ran π)) β (absβπ) β (abs β (ran π βͺ ran π))) |
254 | 218, 253 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β (absβπ) β (abs β (ran π βͺ ran π))) |
255 | | suprub 12050 |
. . . . . . . . . . . . . . 15
β’ ((((abs
β (ran π βͺ ran
π)) β β β§
(abs β (ran π βͺ
ran π)) β β
β§
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯) β§ (absβπ) β (abs β (ran π βͺ ran π))) β (absβπ) β€ sup((abs β (ran π βͺ ran π)), β, < )) |
256 | 251, 254,
255 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β (absβπ) β€ sup((abs β (ran
π βͺ ran π)), β, <
)) |
257 | 256 | adantrr 716 |
. . . . . . . . . . . . 13
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π
β (ran π βͺ ran
π) β§ π β 0)) β (absβπ) β€ sup((abs β (ran
π βͺ ran π)), β, <
)) |
258 | 242, 245,
241, 249, 257 | ltletrd 11249 |
. . . . . . . . . . . 12
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π
β (ran π βͺ ran
π) β§ π β 0)) β 0 < sup((abs β (ran
π βͺ ran π)), β, <
)) |
259 | 241, 258 | elrpd 12883 |
. . . . . . . . . . 11
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π
β (ran π βͺ ran
π) β§ π β 0)) β sup((abs β (ran π βͺ ran π)), β, < ) β
β+) |
260 | 259 | rexlimdvaa 3152 |
. . . . . . . . . 10
β’ ((π β dom β«1
β§ π β dom
β«1) β (βπ β (ran π βͺ ran π)π β 0 β sup((abs β (ran π βͺ ran π)), β, < ) β
β+)) |
261 | 260 | imp 408 |
. . . . . . . . 9
β’ (((π β dom β«1
β§ π β dom
β«1) β§ βπ β (ran π βͺ ran π)π β 0) β sup((abs β (ran π βͺ ran π)), β, < ) β
β+) |
262 | | rpmulcl 12867 |
. . . . . . . . 9
β’ ((2
β β+ β§ sup((abs β (ran π βͺ ran π)), β, < ) β
β+) β (2 Β· sup((abs β (ran π βͺ ran π)), β, < )) β
β+) |
263 | 207, 261,
262 | sylancr 588 |
. . . . . . . 8
β’ (((π β dom β«1
β§ π β dom
β«1) β§ βπ β (ran π βͺ ran π)π β 0) β (2 Β· sup((abs β
(ran π βͺ ran π)), β, < )) β
β+) |
264 | 206, 263 | rerpdivcld 12917 |
. . . . . . 7
β’ (((π β dom β«1
β§ π β dom
β«1) β§ βπ β (ran π βͺ ran π)π β 0) β
((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) / (2 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) β
β) |
265 | 264 | adantll 713 |
. . . . . 6
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β
((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) / (2 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) β
β) |
266 | 265 | adantlr 714 |
. . . . 5
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β
((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) / (2 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) β
β) |
267 | 266 | ad3antrrr 729 |
. . . 4
β’
(((((((π β§ (π β 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 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) β
β) |
268 | | simp-4l 782 |
. . . . . 6
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β π) |
269 | | iccssre 13275 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
270 | 85, 87, 269 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (π΄[,]π΅) β β) |
271 | 270, 62 | sstrdi 3955 |
. . . . . . . . . . 11
β’ (π β (π΄[,]π΅) β β) |
272 | 271 | sselda 3943 |
. . . . . . . . . 10
β’ ((π β§ π€ β (π΄[,]π΅)) β π€ β β) |
273 | 271 | sselda 3943 |
. . . . . . . . . 10
β’ ((π β§ π’ β (π΄[,]π΅)) β π’ β β) |
274 | | subcl 11334 |
. . . . . . . . . 10
β’ ((π€ β β β§ π’ β β) β (π€ β π’) β β) |
275 | 272, 273,
274 | syl2anr 598 |
. . . . . . . . 9
β’ (((π β§ π’ β (π΄[,]π΅)) β§ (π β§ π€ β (π΄[,]π΅))) β (π€ β π’) β β) |
276 | 275 | anandis 677 |
. . . . . . . 8
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π€ β π’) β β) |
277 | 276 | abscld 15256 |
. . . . . . 7
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (absβ(π€ β π’)) β β) |
278 | 277 | 3adantr3 1172 |
. . . . . 6
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (absβ(π€ β π’)) β β) |
279 | 268, 278 | sylan 581 |
. . . . 5
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (absβ(π€ β π’)) β β) |
280 | 279 | adantr 482 |
. . . 4
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
(absβ(π€ β π’)) β
β) |
281 | | rpdivcl 12869 |
. . . . . . . . 9
β’ (((π¦ / 2) β β+
β§ (2 Β· sup((abs β (ran π βͺ ran π)), β, < )) β
β+) β ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
β+) |
282 | 152, 263,
281 | syl2anr 598 |
. . . . . . . 8
β’ ((((π β dom β«1
β§ π β dom
β«1) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β ((π¦ / 2) / (2 Β· sup((abs
β (ran π βͺ ran
π)), β, < )))
β β+) |
283 | 282 | rpred 12886 |
. . . . . . 7
β’ ((((π β dom β«1
β§ π β dom
β«1) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β ((π¦ / 2) / (2 Β· sup((abs
β (ran π βͺ ran
π)), β, < )))
β β) |
284 | 283 | adantlll 717 |
. . . . . 6
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β§ π¦ β β+) β ((π¦ / 2) / (2 Β· sup((abs
β (ran π βͺ ran
π)), β, < )))
β β) |
285 | 284 | adantllr 718 |
. . . . 5
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β ((π¦ / 2) / (2 Β· sup((abs
β (ran π βͺ ran
π)), β, < )))
β β) |
286 | 285 | ad2antrr 725 |
. . . 4
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
((π¦ / 2) / (2 Β·
sup((abs β (ran π
βͺ ran π)), β,
< ))) β β) |
287 | 270 | sseld 3942 |
. . . . . . . . . . 11
β’ (π β (π’ β (π΄[,]π΅) β π’ β β)) |
288 | 270 | sseld 3942 |
. . . . . . . . . . 11
β’ (π β (π€ β (π΄[,]π΅) β π€ β β)) |
289 | | idd 24 |
. . . . . . . . . . 11
β’ (π β (π’ β€ π€ β π’ β€ π€)) |
290 | 287, 288,
289 | 3anim123d 1444 |
. . . . . . . . . 10
β’ (π β ((π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€) β (π’ β β β§ π€ β β β§ π’ β€ π€))) |
291 | 290 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β ((π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€) β (π’ β β β§ π€ β β β§ π’ β€ π€))) |
292 | 291 | imp 408 |
. . . . . . . 8
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (π’ β β β§ π€ β β β§ π’ β€ π€)) |
293 | 55 | abscld 15256 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
294 | 293 | rexrd 11139 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β
β*) |
295 | | elxrge0 13303 |
. . . . . . . . . . . . . . . . . 18
β’
((absβ((πβπ‘) + (i Β· (πβπ‘)))) β (0[,]+β) β
((absβ((πβπ‘) + (i Β· (πβπ‘)))) β β* β§ 0 β€
(absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
296 | 294, 56, 295 | sylanbrc 584 |
. . . . . . . . . . . . . . . . 17
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β (0[,]+β)) |
297 | | ifcl 4530 |
. . . . . . . . . . . . . . . . 17
β’
(((absβ((πβπ‘) + (i Β· (πβπ‘)))) β (0[,]+β) β§ 0 β
(0[,]+β)) β if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β
(0[,]+β)) |
298 | 296, 119,
297 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β
(0[,]+β)) |
299 | 298 | fmpttd 7058 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))),
0)):ββΆ(0[,]+β)) |
300 | 240 | recnd 11117 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β dom β«1
β§ π β dom
β«1) β sup((abs β (ran π βͺ ran π)), β, < ) β
β) |
301 | 300 | 2timesd 12330 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β dom β«1
β§ π β dom
β«1) β (2 Β· sup((abs β (ran π βͺ ran π)), β, < )) = (sup((abs β (ran
π βͺ ran π)), β, < ) + sup((abs
β (ran π βͺ ran
π)), β, <
))) |
302 | 240, 240 | readdcld 11118 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β dom β«1
β§ π β dom
β«1) β (sup((abs β (ran π βͺ ran π)), β, < ) + sup((abs β (ran
π βͺ ran π)), β, < )) β
β) |
303 | 302 | rexrd 11139 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β dom β«1
β§ π β dom
β«1) β (sup((abs β (ran π βͺ ran π)), β, < ) + sup((abs β (ran
π βͺ ran π)), β, < )) β
β*) |
304 | | abs0 15105 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(absβ0) = 0 |
305 | 304, 227 | eqeltrrid 2844 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β dom β«1
β§ π β dom
β«1) β 0 β (abs β (ran π βͺ ran π))) |
306 | | suprub 12050 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((abs
β (ran π βͺ ran
π)) β β β§
(abs β (ran π βͺ
ran π)) β β
β§
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯) β§ 0 β (abs β (ran π βͺ ran π))) β 0 β€ sup((abs β (ran π βͺ ran π)), β, < )) |
307 | 250, 305,
306 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β dom β«1
β§ π β dom
β«1) β 0 β€ sup((abs β (ran π βͺ ran π)), β, < )) |
308 | 240, 240,
307, 307 | addge0d 11665 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β dom β«1
β§ π β dom
β«1) β 0 β€ (sup((abs β (ran π βͺ ran π)), β, < ) + sup((abs β (ran
π βͺ ran π)), β, <
))) |
309 | | elxrge0 13303 |
. . . . . . . . . . . . . . . . . . . 20
β’
((sup((abs β (ran π βͺ ran π)), β, < ) + sup((abs β (ran
π βͺ ran π)), β, < )) β
(0[,]+β) β ((sup((abs β (ran π βͺ ran π)), β, < ) + sup((abs β (ran
π βͺ ran π)), β, < )) β
β* β§ 0 β€ (sup((abs β (ran π βͺ ran π)), β, < ) + sup((abs β (ran
π βͺ ran π)), β, <
)))) |
310 | 303, 308,
309 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β dom β«1
β§ π β dom
β«1) β (sup((abs β (ran π βͺ ran π)), β, < ) + sup((abs β (ran
π βͺ ran π)), β, < )) β
(0[,]+β)) |
311 | 301, 310 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β dom β«1
β§ π β dom
β«1) β (2 Β· sup((abs β (ran π βͺ ran π)), β, < )) β
(0[,]+β)) |
312 | | ifcl 4530 |
. . . . . . . . . . . . . . . . . 18
β’ (((2
Β· sup((abs β (ran π βͺ ran π)), β, < )) β (0[,]+β)
β§ 0 β (0[,]+β)) β if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0) β
(0[,]+β)) |
313 | 311, 119,
312 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π β dom
β«1) β if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0) β
(0[,]+β)) |
314 | 313 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β if(π‘
β (π’(,)π€), (2 Β· sup((abs β
(ran π βͺ ran π)), β, < )), 0) β
(0[,]+β)) |
315 | 314 | fmpttd 7058 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )),
0)):ββΆ(0[,]+β)) |
316 | 1 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β
β) |
317 | 316 | recnd 11117 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β
β) |
318 | 317 | abscld 15256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(πβπ‘)) β β) |
319 | 5 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β
β) |
320 | 319 | recnd 11117 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β
β) |
321 | 320 | abscld 15256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(πβπ‘)) β β) |
322 | | readdcl 11068 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((absβ(πβπ‘)) β β β§ (absβ(πβπ‘)) β β) β ((absβ(πβπ‘)) + (absβ(πβπ‘))) β β) |
323 | 318, 321,
322 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β dom β«1
β§ π‘ β β)
β§ (π β dom
β«1 β§ π‘
β β)) β ((absβ(πβπ‘)) + (absβ(πβπ‘))) β β) |
324 | 323 | anandirs 678 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β ((absβ(πβπ‘)) + (absβ(πβπ‘))) β β) |
325 | 302 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (sup((abs β (ran π βͺ ran π)), β, < ) + sup((abs β (ran
π βͺ ran π)), β, < )) β
β) |
326 | | mulcl 11069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((i
β β β§ (πβπ‘) β β) β (i Β· (πβπ‘)) β β) |
327 | 4, 320, 326 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β dom β«1
β§ π‘ β β)
β (i Β· (πβπ‘)) β β) |
328 | | abstri 15150 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((πβπ‘) β β β§ (i Β· (πβπ‘)) β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ ((absβ(πβπ‘)) + (absβ(i Β· (πβπ‘))))) |
329 | 317, 327,
328 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β dom β«1
β§ π‘ β β)
β§ (π β dom
β«1 β§ π‘
β β)) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ ((absβ(πβπ‘)) + (absβ(i Β· (πβπ‘))))) |
330 | 329 | anandirs 678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ ((absβ(πβπ‘)) + (absβ(i Β· (πβπ‘))))) |
331 | | absmul 15114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((i
β β β§ (πβπ‘) β β) β (absβ(i
Β· (πβπ‘))) = ((absβi) Β·
(absβ(πβπ‘)))) |
332 | 4, 320, 331 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(i Β· (πβπ‘))) = ((absβi) Β·
(absβ(πβπ‘)))) |
333 | | absi 15106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(absβi) = 1 |
334 | 333 | oveq1i 7360 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((absβi) Β· (absβ(πβπ‘))) = (1 Β· (absβ(πβπ‘))) |
335 | 332, 334 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(i Β· (πβπ‘))) = (1 Β· (absβ(πβπ‘)))) |
336 | 321 | recnd 11117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(πβπ‘)) β β) |
337 | 336 | mulid2d 11107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β dom β«1
β§ π‘ β β)
β (1 Β· (absβ(πβπ‘))) = (absβ(πβπ‘))) |
338 | 335, 337 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β dom β«1
β§ π‘ β β)
β (absβ(i Β· (πβπ‘))) = (absβ(πβπ‘))) |
339 | 338 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ(i Β· (πβπ‘))) = (absβ(πβπ‘))) |
340 | 339 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β ((absβ(πβπ‘)) + (absβ(i Β· (πβπ‘)))) = ((absβ(πβπ‘)) + (absβ(πβπ‘)))) |
341 | 330, 340 | breqtrd 5130 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ ((absβ(πβπ‘)) + (absβ(πβπ‘)))) |
342 | 318 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ(πβπ‘)) β β) |
343 | 321 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ(πβπ‘)) β β) |
344 | 240 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β sup((abs β (ran π βͺ ran π)), β, < ) β
β) |
345 | 250 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β ((abs β (ran π βͺ ran π)) β β β§ (abs β (ran
π βͺ ran π)) β β
β§
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯)) |
346 | 218 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (ran π βͺ ran π) β β) |
347 | 1 | ffnd 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β dom β«1
β π Fn
β) |
348 | | fnfvelrn 7027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π Fn β β§ π‘ β β) β (πβπ‘) β ran π) |
349 | 347, 348 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β ran π) |
350 | | elun1 4135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πβπ‘) β ran π β (πβπ‘) β (ran π βͺ ran π)) |
351 | 349, 350 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β (ran π βͺ ran π)) |
352 | 351 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (πβπ‘) β (ran π βͺ ran π)) |
353 | | fnfvima 7178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((abs Fn
β β§ (ran π βͺ
ran π) β β
β§ (πβπ‘) β (ran π βͺ ran π)) β (absβ(πβπ‘)) β (abs β (ran π βͺ ran π))) |
354 | 224, 353 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((ran
π βͺ ran π) β β β§ (πβπ‘) β (ran π βͺ ran π)) β (absβ(πβπ‘)) β (abs β (ran π βͺ ran π))) |
355 | 346, 352,
354 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ(πβπ‘)) β (abs β (ran π βͺ ran π))) |
356 | | suprub 12050 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((abs
β (ran π βͺ ran
π)) β β β§
(abs β (ran π βͺ
ran π)) β β
β§
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯) β§ (absβ(πβπ‘)) β (abs β (ran π βͺ ran π))) β (absβ(πβπ‘)) β€ sup((abs β (ran π βͺ ran π)), β, < )) |
357 | 345, 355,
356 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ(πβπ‘)) β€ sup((abs β (ran π βͺ ran π)), β, < )) |
358 | 5 | ffnd 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β dom β«1
β π Fn
β) |
359 | | fnfvelrn 7027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π Fn β β§ π‘ β β) β (πβπ‘) β ran π) |
360 | 358, 359 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β ran π) |
361 | | elun2 4136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πβπ‘) β ran π β (πβπ‘) β (ran π βͺ ran π)) |
362 | 360, 361 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β (ran π βͺ ran π)) |
363 | 362 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (πβπ‘) β (ran π βͺ ran π)) |
364 | | fnfvima 7178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((abs Fn
β β§ (ran π βͺ
ran π) β β
β§ (πβπ‘) β (ran π βͺ ran π)) β (absβ(πβπ‘)) β (abs β (ran π βͺ ran π))) |
365 | 224, 364 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((ran
π βͺ ran π) β β β§ (πβπ‘) β (ran π βͺ ran π)) β (absβ(πβπ‘)) β (abs β (ran π βͺ ran π))) |
366 | 346, 363,
365 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ(πβπ‘)) β (abs β (ran π βͺ ran π))) |
367 | | suprub 12050 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((abs
β (ran π βͺ ran
π)) β β β§
(abs β (ran π βͺ
ran π)) β β
β§
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯) β§ (absβ(πβπ‘)) β (abs β (ran π βͺ ran π))) β (absβ(πβπ‘)) β€ sup((abs β (ran π βͺ ran π)), β, < )) |
368 | 345, 366,
367 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ(πβπ‘)) β€ sup((abs β (ran π βͺ ran π)), β, < )) |
369 | 342, 343,
344, 344, 357, 368 | le2addd 11708 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β ((absβ(πβπ‘)) + (absβ(πβπ‘))) β€ (sup((abs β (ran π βͺ ran π)), β, < ) + sup((abs β (ran
π βͺ ran π)), β, <
))) |
370 | 293, 324,
325, 341, 369 | letrd 11246 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ (sup((abs β (ran π βͺ ran π)), β, < ) + sup((abs β (ran
π βͺ ran π)), β, <
))) |
371 | 301 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (2 Β· sup((abs β (ran π βͺ ran π)), β, < )) = (sup((abs β (ran
π βͺ ran π)), β, < ) + sup((abs
β (ran π βͺ ran
π)), β, <
))) |
372 | 370, 371 | breqtrrd 5132 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ (2 Β· sup((abs β (ran
π βͺ ran π)), β, <
))) |
373 | 50, 372 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β (π’(,)π€)) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β€ (2 Β· sup((abs β (ran
π βͺ ran π)), β, <
))) |
374 | | iftrue 4491 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) = (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
375 | 374 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β (π’(,)π€)) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) = (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
376 | | iftrue 4491 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0) = (2 Β·
sup((abs β (ran π
βͺ ran π)), β,
< ))) |
377 | 376 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β (π’(,)π€)) β if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0) = (2 Β·
sup((abs β (ran π
βͺ ran π)), β,
< ))) |
378 | 373, 375,
377 | 3brtr4d 5136 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β (π’(,)π€)) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0)) |
379 | 378 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0))) |
380 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
π‘ β (π’(,)π€) β 0 β€ 0) |
381 | | iffalse 4494 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) = 0) |
382 | | iffalse 4494 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0) =
0) |
383 | 380, 381,
382 | 3brtr4d 5136 |
. . . . . . . . . . . . . . . . . 18
β’ (Β¬
π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0)) |
384 | 379, 383 | pm2.61d1 180 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π β dom
β«1) β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0)) |
385 | 384 | ralrimivw 3146 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π β dom
β«1) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0)) |
386 | | ovex 7383 |
. . . . . . . . . . . . . . . . . . 19
β’ (2
Β· sup((abs β (ran π βͺ ran π)), β, < )) β
V |
387 | 386, 64 | ifex 4535 |
. . . . . . . . . . . . . . . . . 18
β’ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0) β
V |
388 | 387 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β if(π‘
β (π’(,)π€), (2 Β· sup((abs β
(ran π βͺ ran π)), β, < )), 0) β
V) |
389 | | eqidd 2739 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0)) = (π‘ β β β¦ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0))) |
390 | 14, 71, 388, 74, 389 | ofrfval2 7629 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π β dom
β«1) β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βr β€ (π‘ β β β¦ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0)) β
βπ‘ β β
if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0) β€ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0))) |
391 | 385, 390 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βr β€ (π‘ β β β¦ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0))) |
392 | | itg2le 25026 |
. . . . . . . . . . . . . . 15
β’ (((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)):ββΆ(0[,]+β) β§
(π‘ β β β¦
if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )),
0)):ββΆ(0[,]+β) β§ (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0)) βr β€ (π‘ β β β¦ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β€
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (2 Β· sup((abs β
(ran π βͺ ran π)), β, < )),
0)))) |
393 | 299, 315,
391, 392 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π β dom
β«1) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β€
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (2 Β· sup((abs β
(ran π βͺ ran π)), β, < )),
0)))) |
394 | 393 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π’
β β β§ π€
β β β§ π’ β€
π€)) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β€
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (2 Β· sup((abs β
(ran π βͺ ran π)), β, < )),
0)))) |
395 | | mblvol 24816 |
. . . . . . . . . . . . . . . . 17
β’ ((π’(,)π€) β dom vol β (volβ(π’(,)π€)) = (vol*β(π’(,)π€))) |
396 | 34, 395 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
(volβ(π’(,)π€)) = (vol*β(π’(,)π€)) |
397 | | ovolioo 24854 |
. . . . . . . . . . . . . . . 16
β’ ((π’ β β β§ π€ β β β§ π’ β€ π€) β (vol*β(π’(,)π€)) = (π€ β π’)) |
398 | 396, 397 | eqtrid 2790 |
. . . . . . . . . . . . . . 15
β’ ((π’ β β β§ π€ β β β§ π’ β€ π€) β (volβ(π’(,)π€)) = (π€ β π’)) |
399 | | resubcl 11399 |
. . . . . . . . . . . . . . . . 17
β’ ((π€ β β β§ π’ β β) β (π€ β π’) β β) |
400 | 399 | ancoms 460 |
. . . . . . . . . . . . . . . 16
β’ ((π’ β β β§ π€ β β) β (π€ β π’) β β) |
401 | 400 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
β’ ((π’ β β β§ π€ β β β§ π’ β€ π€) β (π€ β π’) β β) |
402 | 398, 401 | eqeltrd 2839 |
. . . . . . . . . . . . . 14
β’ ((π’ β β β§ π€ β β β§ π’ β€ π€) β (volβ(π’(,)π€)) β β) |
403 | | elrege0 13300 |
. . . . . . . . . . . . . . . . 17
β’ (sup((abs
β (ran π βͺ ran
π)), β, < ) β
(0[,)+β) β (sup((abs β (ran π βͺ ran π)), β, < ) β β β§ 0
β€ sup((abs β (ran π βͺ ran π)), β, < ))) |
404 | 240, 307,
403 | sylanbrc 584 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π β dom
β«1) β sup((abs β (ran π βͺ ran π)), β, < ) β
(0[,)+β)) |
405 | | ge0addcl 13306 |
. . . . . . . . . . . . . . . 16
β’
((sup((abs β (ran π βͺ ran π)), β, < ) β (0[,)+β)
β§ sup((abs β (ran π βͺ ran π)), β, < ) β (0[,)+β))
β (sup((abs β (ran π βͺ ran π)), β, < ) + sup((abs β (ran
π βͺ ran π)), β, < )) β
(0[,)+β)) |
406 | 404, 404,
405 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β (sup((abs β (ran π βͺ ran π)), β, < ) + sup((abs β (ran
π βͺ ran π)), β, < )) β
(0[,)+β)) |
407 | 301, 406 | eqeltrd 2839 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π β dom
β«1) β (2 Β· sup((abs β (ran π βͺ ran π)), β, < )) β
(0[,)+β)) |
408 | | itg2const 25027 |
. . . . . . . . . . . . . . 15
β’ (((π’(,)π€) β dom vol β§ (volβ(π’(,)π€)) β β β§ (2 Β· sup((abs
β (ran π βͺ ran
π)), β, < ))
β (0[,)+β)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0))) = ((2 Β·
sup((abs β (ran π
βͺ ran π)), β,
< )) Β· (volβ(π’(,)π€)))) |
409 | 34, 408 | mp3an1 1449 |
. . . . . . . . . . . . . 14
β’
(((volβ(π’(,)π€)) β β β§ (2 Β· sup((abs
β (ran π βͺ ran
π)), β, < ))
β (0[,)+β)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (2 Β· sup((abs β (ran π βͺ ran π)), β, < )), 0))) = ((2 Β·
sup((abs β (ran π
βͺ ran π)), β,
< )) Β· (volβ(π’(,)π€)))) |
410 | 402, 407,
409 | syl2anr 598 |
. . . . . . . . . . . . 13
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π’
β β β§ π€
β β β§ π’ β€
π€)) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (2 Β· sup((abs β
(ran π βͺ ran π)), β, < )), 0))) = ((2
Β· sup((abs β (ran π βͺ ran π)), β, < )) Β·
(volβ(π’(,)π€)))) |
411 | 394, 410 | breqtrd 5130 |
. . . . . . . . . . . 12
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π’
β β β§ π€
β β β§ π’ β€
π€)) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β€ ((2 Β· sup((abs β
(ran π βͺ ran π)), β, < )) Β·
(volβ(π’(,)π€)))) |
412 | 411 | adantll 713 |
. . . . . . . . . . 11
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β β
β§ π€ β β
β§ π’ β€ π€)) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β€ ((2 Β· sup((abs β
(ran π βͺ ran π)), β, < )) Β·
(volβ(π’(,)π€)))) |
413 | 412 | adantlr 714 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β§ (π’ β β β§ π€ β β β§ π’ β€ π€)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β€ ((2 Β· sup((abs β
(ran π βͺ ran π)), β, < )) Β·
(volβ(π’(,)π€)))) |
414 | 82 | ad3antlr 730 |
. . . . . . . . . . 11
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β§ (π’ β β β§ π€ β β β§ π’ β€ π€)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
415 | 402 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β§ (π’ β β β§ π€ β β β§ π’ β€ π€)) β (volβ(π’(,)π€)) β β) |
416 | 263 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β (2 Β· sup((abs β
(ran π βͺ ran π)), β, < )) β
β+) |
417 | 416 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β§ (π’ β β β§ π€ β β β§ π’ β€ π€)) β (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )) β
β+) |
418 | 414, 415,
417 | ledivmuld 12939 |
. . . . . . . . . 10
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β§ (π’ β β β§ π€ β β β§ π’ β€ π€)) β (((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) / (2 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) β€
(volβ(π’(,)π€)) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β€ ((2 Β· sup((abs β
(ran π βͺ ran π)), β, < )) Β·
(volβ(π’(,)π€))))) |
419 | 413, 418 | mpbird 257 |
. . . . . . . . 9
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β§ (π’ β β β§ π€ β β β§ π’ β€ π€)) β ((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) / (2 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) β€
(volβ(π’(,)π€))) |
420 | | abssubge0 15147 |
. . . . . . . . . . . 12
β’ ((π’ β β β§ π€ β β β§ π’ β€ π€) β (absβ(π€ β π’)) = (π€ β π’)) |
421 | 397, 420 | eqtr4d 2781 |
. . . . . . . . . . 11
β’ ((π’ β β β§ π€ β β β§ π’ β€ π€) β (vol*β(π’(,)π€)) = (absβ(π€ β π’))) |
422 | 396, 421 | eqtrid 2790 |
. . . . . . . . . 10
β’ ((π’ β β β§ π€ β β β§ π’ β€ π€) β (volβ(π’(,)π€)) = (absβ(π€ β π’))) |
423 | 422 | adantl 483 |
. . . . . . . . 9
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β§ (π’ β β β§ π€ β β β§ π’ β€ π€)) β (volβ(π’(,)π€)) = (absβ(π€ β π’))) |
424 | 419, 423 | breqtrd 5130 |
. . . . . . . 8
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β§ (π’ β β β§ π€ β β β§ π’ β€ π€)) β ((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) / (2 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) β€
(absβ(π€ β π’))) |
425 | 292, 424 | syldan 592 |
. . . . . . 7
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π β 0) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β ((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) / (2 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) β€
(absβ(π€ β π’))) |
426 | 425 | adantllr 718 |
. . . . . 6
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β ((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) / (2 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) β€
(absβ(π€ β π’))) |
427 | 426 | adantlr 714 |
. . . . 5
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β ((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) / (2 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) β€
(absβ(π€ β π’))) |
428 | 427 | adantr 482 |
. . . 4
β’
(((((((π β§ (π β 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 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) β€
(absβ(π€ β π’))) |
429 | | simpr 486 |
. . . 4
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
(absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, <
)))) |
430 | 267, 280,
286, 428, 429 | lelttrd 11247 |
. . 3
β’
(((((((π β§ (π β 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 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) <
((π¦ / 2) / (2 Β·
sup((abs β (ran π
βͺ ran π)), β,
< )))) |
431 | 82 | adantl 483 |
. . . . . 6
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
432 | 431 | ad3antrrr 729 |
. . . . 5
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) β β) |
433 | 126 | adantl 483 |
. . . . 5
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β (π¦ / 2) β
β) |
434 | 416 | adantlr 714 |
. . . . . 6
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β (2 Β· sup((abs β
(ran π βͺ ran π)), β, < )) β
β+) |
435 | 434 | adantr 482 |
. . . . 5
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β (2
Β· sup((abs β (ran π βͺ ran π)), β, < )) β
β+) |
436 | 432, 433,
435 | ltdiv1d 12931 |
. . . 4
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β
((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) < (π¦ / 2) β ((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) / (2 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) <
((π¦ / 2) / (2 Β·
sup((abs β (ran π
βͺ ran π)), β,
< ))))) |
437 | 436 | ad2antrr 725 |
. . 3
β’
(((((((π β§ (π β 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) β ((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πβπ‘) + (i Β· (πβπ‘)))), 0))) / (2 Β· sup((abs β
(ran π βͺ ran π)), β, < ))) <
((π¦ / 2) / (2 Β·
sup((abs β (ran π
βͺ ran π)), β,
< ))))) |
438 | 430, 437 | mpbird 257 |
. 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)) |
439 | 198 | adantllr 718 |
. . . 4
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) < (π¦ / 2)) |
440 | 439 | 3adantr3 1172 |
. . 3
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0))) < (π¦ / 2)) |
441 | 440 | 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)) |
442 | 83, 204, 205, 205, 438, 441 | lt2addd 11712 |
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 Β· (πβπ‘)))), 0))) + (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) < ((π¦ / 2) + (π¦ / 2))) |