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 | ftc1lem2 25322 |
. 2
β’ (π β πΊ:(π΄[,]π΅)βΆβ) |
10 | | rphalfcl 12871 |
. . . . . 6
β’ (π¦ β β+
β (π¦ / 2) β
β+) |
11 | 1, 2, 3, 4, 5, 6, 7, 8 | ftc1anclem6 36042 |
. . . . . 6
β’ ((π β§ (π¦ / 2) β β+) β
βπ β dom
β«1βπ
β dom β«1(β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) |
12 | 10, 11 | sylan2 594 |
. . . . 5
β’ ((π β§ π¦ β β+) β
βπ β dom
β«1βπ
β dom β«1(β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) |
13 | 12 | adantrl 715 |
. . . 4
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β
βπ β dom
β«1βπ
β dom β«1(β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) |
14 | 10 | ad2antll 728 |
. . . . . . . . . . 11
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β (π¦ / 2) β
β+) |
15 | | 2rp 12849 |
. . . . . . . . . . . 12
β’ 2 β
β+ |
16 | | i1ff 24962 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β dom β«1
β π:ββΆβ) |
17 | 16 | frnd 6672 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β dom β«1
β ran π β
β) |
18 | 17 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β dom β«1
β§ π β dom
β«1) β ran π β β) |
19 | | i1ff 24962 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β dom β«1
β π:ββΆβ) |
20 | 19 | frnd 6672 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β dom β«1
β ran π β
β) |
21 | 20 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β dom β«1
β§ π β dom
β«1) β ran π β β) |
22 | 18, 21 | unssd 4145 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β dom β«1
β§ π β dom
β«1) β (ran π βͺ ran π) β β) |
23 | | ax-resscn 11042 |
. . . . . . . . . . . . . . . . . 18
β’ β
β β |
24 | 22, 23 | sstrdi 3955 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π β dom
β«1) β (ran π βͺ ran π) β β) |
25 | | i1f0rn 24968 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β dom β«1
β 0 β ran π) |
26 | | elun1 4135 |
. . . . . . . . . . . . . . . . . . 19
β’ (0 β
ran π β 0 β (ran
π βͺ ran π)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom β«1
β 0 β (ran π
βͺ ran π)) |
28 | 27 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π β dom
β«1) β 0 β (ran π βͺ ran π)) |
29 | | absf 15157 |
. . . . . . . . . . . . . . . . . . 19
β’
abs:ββΆβ |
30 | | ffn 6664 |
. . . . . . . . . . . . . . . . . . 19
β’
(abs:ββΆβ β abs Fn β) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’ abs Fn
β |
32 | | fnfvima 7178 |
. . . . . . . . . . . . . . . . . 18
β’ ((abs Fn
β β§ (ran π βͺ
ran π) β β
β§ 0 β (ran π βͺ
ran π)) β
(absβ0) β (abs β (ran π βͺ ran π))) |
33 | 31, 32 | mp3an1 1449 |
. . . . . . . . . . . . . . . . 17
β’ (((ran
π βͺ ran π) β β β§ 0 β
(ran π βͺ ran π)) β (absβ0) β
(abs β (ran π βͺ
ran π))) |
34 | 24, 28, 33 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π β dom
β«1) β (absβ0) β (abs β (ran π βͺ ran π))) |
35 | 34 | ne0d 4294 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β (ran π βͺ ran π)) β β
) |
36 | | imassrn 6021 |
. . . . . . . . . . . . . . . . 17
β’ (abs
β (ran π βͺ ran
π)) β ran
abs |
37 | | frn 6671 |
. . . . . . . . . . . . . . . . . 18
β’
(abs:ββΆβ β ran abs β
β) |
38 | 29, 37 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ ran abs
β β |
39 | 36, 38 | sstri 3952 |
. . . . . . . . . . . . . . . 16
β’ (abs
β (ran π βͺ ran
π)) β
β |
40 | | ffun 6667 |
. . . . . . . . . . . . . . . . . 18
β’
(abs:ββΆβ β Fun abs) |
41 | 29, 40 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ Fun
abs |
42 | | i1frn 24963 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom β«1
β ran π β
Fin) |
43 | | i1frn 24963 |
. . . . . . . . . . . . . . . . . 18
β’ (π β dom β«1
β ran π β
Fin) |
44 | | unfi 9050 |
. . . . . . . . . . . . . . . . . 18
β’ ((ran
π β Fin β§ ran
π β Fin) β (ran
π βͺ ran π) β Fin) |
45 | 42, 43, 44 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’ ((π β dom β«1
β§ π β dom
β«1) β (ran π βͺ ran π) β Fin) |
46 | | imafi 9053 |
. . . . . . . . . . . . . . . . 17
β’ ((Fun abs
β§ (ran π βͺ ran
π) β Fin) β (abs
β (ran π βͺ ran
π)) β
Fin) |
47 | 41, 45, 46 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β (ran π βͺ ran π)) β Fin) |
48 | | fimaxre2 12034 |
. . . . . . . . . . . . . . . 16
β’ (((abs
β (ran π βͺ ran
π)) β β β§
(abs β (ran π βͺ
ran π)) β Fin) β
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯) |
49 | 39, 47, 48 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β βπ₯ β β βπ¦ β (abs β (ran π βͺ ran π))π¦ β€ π₯) |
50 | | suprcl 12049 |
. . . . . . . . . . . . . . . 16
β’ (((abs
β (ran π βͺ ran
π)) β β β§
(abs β (ran π βͺ
ran π)) β β
β§
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯) β sup((abs β (ran π βͺ ran π)), β, < ) β
β) |
51 | 39, 50 | mp3an1 1449 |
. . . . . . . . . . . . . . 15
β’ (((abs
β (ran π βͺ ran
π)) β β
β§
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯) β sup((abs β (ran π βͺ ran π)), β, < ) β
β) |
52 | 35, 49, 51 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π β dom
β«1) β sup((abs β (ran π βͺ ran π)), β, < ) β
β) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β dom β«1
β§ π β dom
β«1) β§ βπ β (ran π βͺ ran π)π β 0) β sup((abs β (ran π βͺ ran π)), β, < ) β
β) |
54 | | 0red 11092 |
. . . . . . . . . . . . . . . 16
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π
β (ran π βͺ ran
π) β§ π β 0)) β 0 β
β) |
55 | 24 | sselda 3943 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β π β
β) |
56 | 55 | abscld 15256 |
. . . . . . . . . . . . . . . . 17
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β (absβπ) β
β) |
57 | 56 | adantrr 716 |
. . . . . . . . . . . . . . . 16
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π
β (ran π βͺ ran
π) β§ π β 0)) β (absβπ) β
β) |
58 | 52 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π
β (ran π βͺ ran
π) β§ π β 0)) β sup((abs β (ran π βͺ ran π)), β, < ) β
β) |
59 | | absgt0 15144 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β (π β 0 β 0 <
(absβπ))) |
60 | 55, 59 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β (π β 0 β 0 <
(absβπ))) |
61 | 60 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β (π β 0 β 0 <
(absβπ))) |
62 | 61 | impr 456 |
. . . . . . . . . . . . . . . 16
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π
β (ran π βͺ ran
π) β§ π β 0)) β 0 < (absβπ)) |
63 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β dom β«1
β§ π β dom
β«1) β (abs β (ran π βͺ ran π)) β β) |
64 | 63, 35, 49 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β dom β«1
β§ π β dom
β«1) β ((abs β (ran π βͺ ran π)) β β β§ (abs β (ran
π βͺ ran π)) β β
β§
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯)) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β ((abs β
(ran π βͺ ran π)) β β β§ (abs
β (ran π βͺ ran
π)) β β
β§
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯)) |
66 | | fnfvima 7178 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((abs Fn
β β§ (ran π βͺ
ran π) β β
β§ π β (ran π βͺ ran π)) β (absβπ) β (abs β (ran π βͺ ran π))) |
67 | 31, 66 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . . 19
β’ (((ran
π βͺ ran π) β β β§ π β (ran π βͺ ran π)) β (absβπ) β (abs β (ran π βͺ ran π))) |
68 | 24, 67 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β (absβπ) β (abs β (ran π βͺ ran π))) |
69 | | suprub 12050 |
. . . . . . . . . . . . . . . . . 18
β’ ((((abs
β (ran π βͺ ran
π)) β β β§
(abs β (ran π βͺ
ran π)) β β
β§
βπ₯ β β
βπ¦ β (abs
β (ran π βͺ ran
π))π¦ β€ π₯) β§ (absβπ) β (abs β (ran π βͺ ran π))) β (absβπ) β€ sup((abs β (ran π βͺ ran π)), β, < )) |
70 | 65, 68, 69 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π
β (ran π βͺ ran
π)) β (absβπ) β€ sup((abs β (ran
π βͺ ran π)), β, <
)) |
71 | 70 | adantrr 716 |
. . . . . . . . . . . . . . . 16
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π
β (ran π βͺ ran
π) β§ π β 0)) β (absβπ) β€ sup((abs β (ran
π βͺ ran π)), β, <
)) |
72 | 54, 57, 58, 62, 71 | ltletrd 11249 |
. . . . . . . . . . . . . . 15
β’ (((π β dom β«1
β§ π β dom
β«1) β§ (π
β (ran π βͺ ran
π) β§ π β 0)) β 0 < sup((abs β (ran
π βͺ ran π)), β, <
)) |
73 | 72 | rexlimdvaa 3152 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π β dom
β«1) β (βπ β (ran π βͺ ran π)π β 0 β 0 < sup((abs β (ran
π βͺ ran π)), β, <
))) |
74 | 73 | imp 408 |
. . . . . . . . . . . . 13
β’ (((π β dom β«1
β§ π β dom
β«1) β§ βπ β (ran π βͺ ran π)π β 0) β 0 < sup((abs β (ran
π βͺ ran π)), β, <
)) |
75 | 53, 74 | elrpd 12883 |
. . . . . . . . . . . 12
β’ (((π β dom β«1
β§ π β dom
β«1) β§ βπ β (ran π βͺ ran π)π β 0) β sup((abs β (ran π βͺ ran π)), β, < ) β
β+) |
76 | | rpmulcl 12867 |
. . . . . . . . . . . 12
β’ ((2
β β+ β§ sup((abs β (ran π βͺ ran π)), β, < ) β
β+) β (2 Β· sup((abs β (ran π βͺ ran π)), β, < )) β
β+) |
77 | 15, 75, 76 | sylancr 588 |
. . . . . . . . . . 11
β’ (((π β dom β«1
β§ π β dom
β«1) β§ βπ β (ran π βͺ ran π)π β 0) β (2 Β· sup((abs β
(ran π βͺ ran π)), β, < )) β
β+) |
78 | | rpdivcl 12869 |
. . . . . . . . . . 11
β’ (((π¦ / 2) β β+
β§ (2 Β· sup((abs β (ran π βͺ ran π)), β, < )) β
β+) β ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
β+) |
79 | 14, 77, 78 | syl2an 597 |
. . . . . . . . . 10
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ ((π β dom β«1
β§ π β dom
β«1) β§ βπ β (ran π βͺ ran π)π β 0)) β ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
β+) |
80 | 79 | anassrs 469 |
. . . . . . . . 9
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ βπ β (ran π βͺ ran π)π β 0) β ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
β+) |
81 | 80 | adantlr 714 |
. . . . . . . 8
β’
(((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
β+) |
82 | | ancom 462 |
. . . . . . . . . . . 12
β’ ((π’ β (π΄[,]π΅) β§ π¦ β β+) β (π¦ β β+
β§ π’ β (π΄[,]π΅))) |
83 | 82 | anbi2i 624 |
. . . . . . . . . . 11
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β
((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ (π¦ β β+ β§ π’ β (π΄[,]π΅)))) |
84 | | an32 645 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β ((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π¦ β
β+))) |
85 | 84 | anbi1i 625 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2))) |
86 | | an32 645 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ (π’ β (π΄[,]π΅) β§ π¦ β
β+))) |
87 | 85, 86 | bitri 275 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ (π’ β (π΄[,]π΅) β§ π¦ β
β+))) |
88 | 87 | anbi1i 625 |
. . . . . . . . . . . 12
β’
(((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
βπ β (ran π βͺ ran π)π β 0)) |
89 | | an32 645 |
. . . . . . . . . . . 12
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
βπ β (ran π βͺ ran π)π β 0) β ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ (π’ β (π΄[,]π΅) β§ π¦ β
β+))) |
90 | 88, 89 | bitri 275 |
. . . . . . . . . . 11
β’
(((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ (π’ β (π΄[,]π΅) β§ π¦ β
β+))) |
91 | | anass 470 |
. . . . . . . . . . 11
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ π’ β (π΄[,]π΅)) β ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ (π¦ β β+ β§ π’ β (π΄[,]π΅)))) |
92 | 83, 90, 91 | 3bitr4i 303 |
. . . . . . . . . 10
β’
(((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β (((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ π’ β (π΄[,]π΅))) |
93 | | oveq12 7359 |
. . . . . . . . . . . . . . . 16
β’ ((π = π€ β§ π = π’) β (π β π) = (π€ β π’)) |
94 | 93 | ancoms 460 |
. . . . . . . . . . . . . . 15
β’ ((π = π’ β§ π = π€) β (π β π) = (π€ β π’)) |
95 | 94 | fveq2d 6842 |
. . . . . . . . . . . . . 14
β’ ((π = π’ β§ π = π€) β (absβ(π β π)) = (absβ(π€ β π’))) |
96 | 95 | breq1d 5114 |
. . . . . . . . . . . . 13
β’ ((π = π’ β§ π = π€) β ((absβ(π β π)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, <
))))) |
97 | | fveq2 6838 |
. . . . . . . . . . . . . . . 16
β’ (π = π€ β (πΊβπ) = (πΊβπ€)) |
98 | | fveq2 6838 |
. . . . . . . . . . . . . . . 16
β’ (π = π’ β (πΊβπ) = (πΊβπ’)) |
99 | 97, 98 | oveqan12rd 7370 |
. . . . . . . . . . . . . . 15
β’ ((π = π’ β§ π = π€) β ((πΊβπ) β (πΊβπ)) = ((πΊβπ€) β (πΊβπ’))) |
100 | 99 | fveq2d 6842 |
. . . . . . . . . . . . . 14
β’ ((π = π’ β§ π = π€) β (absβ((πΊβπ) β (πΊβπ))) = (absβ((πΊβπ€) β (πΊβπ’)))) |
101 | 100 | breq1d 5114 |
. . . . . . . . . . . . 13
β’ ((π = π’ β§ π = π€) β ((absβ((πΊβπ) β (πΊβπ))) < π¦ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
102 | 96, 101 | imbi12d 345 |
. . . . . . . . . . . 12
β’ ((π = π’ β§ π = π€) β (((absβ(π β π)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ) β (πΊβπ))) < π¦) β ((absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ€) β (πΊβπ’))) < π¦))) |
103 | | oveq12 7359 |
. . . . . . . . . . . . . . . 16
β’ ((π = π’ β§ π = π€) β (π β π) = (π’ β π€)) |
104 | 103 | ancoms 460 |
. . . . . . . . . . . . . . 15
β’ ((π = π€ β§ π = π’) β (π β π) = (π’ β π€)) |
105 | 104 | fveq2d 6842 |
. . . . . . . . . . . . . 14
β’ ((π = π€ β§ π = π’) β (absβ(π β π)) = (absβ(π’ β π€))) |
106 | 105 | breq1d 5114 |
. . . . . . . . . . . . 13
β’ ((π = π€ β§ π = π’) β ((absβ(π β π)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ(π’ β π€)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, <
))))) |
107 | | fveq2 6838 |
. . . . . . . . . . . . . . . 16
β’ (π = π’ β (πΊβπ) = (πΊβπ’)) |
108 | | fveq2 6838 |
. . . . . . . . . . . . . . . 16
β’ (π = π€ β (πΊβπ) = (πΊβπ€)) |
109 | 107, 108 | oveqan12rd 7370 |
. . . . . . . . . . . . . . 15
β’ ((π = π€ β§ π = π’) β ((πΊβπ) β (πΊβπ)) = ((πΊβπ’) β (πΊβπ€))) |
110 | 109 | fveq2d 6842 |
. . . . . . . . . . . . . 14
β’ ((π = π€ β§ π = π’) β (absβ((πΊβπ) β (πΊβπ))) = (absβ((πΊβπ’) β (πΊβπ€)))) |
111 | 110 | breq1d 5114 |
. . . . . . . . . . . . 13
β’ ((π = π€ β§ π = π’) β ((absβ((πΊβπ) β (πΊβπ))) < π¦ β (absβ((πΊβπ’) β (πΊβπ€))) < π¦)) |
112 | 106, 111 | imbi12d 345 |
. . . . . . . . . . . 12
β’ ((π = π€ β§ π = π’) β (((absβ(π β π)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ) β (πΊβπ))) < π¦) β ((absβ(π’ β π€)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ’) β (πΊβπ€))) < π¦))) |
113 | | iccssre 13275 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
114 | 2, 3, 113 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (π΄[,]π΅) β β) |
115 | 114 | ad4antr 731 |
. . . . . . . . . . . 12
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β (π΄[,]π΅) β β) |
116 | | simp-4l 782 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β π) |
117 | 114, 23 | sstrdi 3955 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄[,]π΅) β β) |
118 | 117 | sselda 3943 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β (π΄[,]π΅)) β π€ β β) |
119 | 117 | sselda 3943 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π΄[,]π΅)) β π’ β β) |
120 | | abssub 15146 |
. . . . . . . . . . . . . . . . 17
β’ ((π€ β β β§ π’ β β) β
(absβ(π€ β π’)) = (absβ(π’ β π€))) |
121 | 118, 119,
120 | syl2anr 598 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π’ β (π΄[,]π΅)) β§ (π β§ π€ β (π΄[,]π΅))) β (absβ(π€ β π’)) = (absβ(π’ β π€))) |
122 | 121 | anandis 677 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (absβ(π€ β π’)) = (absβ(π’ β π€))) |
123 | 122 | breq1d 5114 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ(π’ β π€)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, <
))))) |
124 | 9 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π€ β (π΄[,]π΅)) β (πΊβπ€) β β) |
125 | 9 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π’ β (π΄[,]π΅)) β (πΊβπ’) β β) |
126 | | abssub 15146 |
. . . . . . . . . . . . . . . . 17
β’ (((πΊβπ€) β β β§ (πΊβπ’) β β) β (absβ((πΊβπ€) β (πΊβπ’))) = (absβ((πΊβπ’) β (πΊβπ€)))) |
127 | 124, 125,
126 | syl2anr 598 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π’ β (π΄[,]π΅)) β§ (π β§ π€ β (π΄[,]π΅))) β (absβ((πΊβπ€) β (πΊβπ’))) = (absβ((πΊβπ’) β (πΊβπ€)))) |
128 | 127 | anandis 677 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (absβ((πΊβπ€) β (πΊβπ’))) = (absβ((πΊβπ’) β (πΊβπ€)))) |
129 | 128 | breq1d 5114 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((absβ((πΊβπ€) β (πΊβπ’))) < π¦ β (absβ((πΊβπ’) β (πΊβπ€))) < π¦)) |
130 | 123, 129 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (((absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ€) β (πΊβπ’))) < π¦) β ((absβ(π’ β π€)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ’) β (πΊβπ€))) < π¦))) |
131 | 116, 130 | sylan 581 |
. . . . . . . . . . . 12
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (((absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ€) β (πΊβπ’))) < π¦) β ((absβ(π’ β π€)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ’) β (πΊβπ€))) < π¦))) |
132 | 2 | rexrd 11139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π΄ β
β*) |
133 | 3 | rexrd 11139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π΅ β
β*) |
134 | 132, 133 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (π΄ β β* β§ π΅ β
β*)) |
135 | | df-icc 13200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ [,] =
(π₯ β
β*, π¦
β β* β¦ {π‘ β β* β£ (π₯ β€ π‘ β§ π‘ β€ π¦)}) |
136 | 135 | elixx3g 13206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π’ β (π΄[,]π΅) β ((π΄ β β* β§ π΅ β β*
β§ π’ β
β*) β§ (π΄ β€ π’ β§ π’ β€ π΅))) |
137 | 136 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π’ β (π΄[,]π΅) β (π΄ β€ π’ β§ π’ β€ π΅)) |
138 | 137 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π’ β (π΄[,]π΅) β π΄ β€ π’) |
139 | 135 | elixx3g 13206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π€ β (π΄[,]π΅) β ((π΄ β β* β§ π΅ β β*
β§ π€ β
β*) β§ (π΄ β€ π€ β§ π€ β€ π΅))) |
140 | 139 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π€ β (π΄[,]π΅) β (π΄ β€ π€ β§ π€ β€ π΅)) |
141 | 140 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ β (π΄[,]π΅) β π€ β€ π΅) |
142 | 138, 141 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅)) β (π΄ β€ π’ β§ π€ β€ π΅)) |
143 | | ioossioo 13287 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π΄ β β*
β§ π΅ β
β*) β§ (π΄ β€ π’ β§ π€ β€ π΅)) β (π’(,)π€) β (π΄(,)π΅)) |
144 | 134, 142,
143 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π’(,)π€) β (π΄(,)π΅)) |
145 | 5 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π΄(,)π΅) β π·) |
146 | 144, 145 | sstrd 3953 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π’(,)π€) β π·) |
147 | 146 | sselda 3943 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β π‘ β π·) |
148 | 8 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π‘ β π·) β (πΉβπ‘) β β) |
149 | 148 | abscld 15256 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π‘ β π·) β (absβ(πΉβπ‘)) β β) |
150 | 149 | rexrd 11139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π‘ β π·) β (absβ(πΉβπ‘)) β
β*) |
151 | 148 | absge0d 15264 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π‘ β π·) β 0 β€ (absβ(πΉβπ‘))) |
152 | | elxrge0 13303 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((absβ(πΉβπ‘)) β (0[,]+β) β
((absβ(πΉβπ‘)) β β*
β§ 0 β€ (absβ(πΉβπ‘)))) |
153 | 150, 151,
152 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π‘ β π·) β (absβ(πΉβπ‘)) β (0[,]+β)) |
154 | 153 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β π·) β (absβ(πΉβπ‘)) β (0[,]+β)) |
155 | 147, 154 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ(πΉβπ‘)) β (0[,]+β)) |
156 | | 0e0iccpnf 13305 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 0 β
(0[,]+β) |
157 | 156 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ Β¬ π‘ β (π’(,)π€)) β 0 β
(0[,]+β)) |
158 | 155, 157 | ifclda 4520 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β
(0[,]+β)) |
159 | 158 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β β) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β
(0[,]+β)) |
160 | 159 | fmpttd 7058 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)),
0)):ββΆ(0[,]+β)) |
161 | | itg2cl 25019 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)):ββΆ(0[,]+β) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β
β*) |
162 | 160, 161 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β
β*) |
163 | 162 | 3adantr3 1172 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β
β*) |
164 | 116, 163 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β
β*) |
165 | 164 | adantr 482 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β
β*) |
166 | | simplll 774 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β (π β§ (π β dom β«1 β§ π β dom
β«1))) |
167 | 148 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β π·) β (πΉβπ‘) β β) |
168 | 147, 167 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (πΉβπ‘) β β) |
169 | 168 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (πΉβπ‘) β β) |
170 | | elioore 13223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π‘ β (π’(,)π€) β π‘ β β) |
171 | 16 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β
β) |
172 | 171 | recnd 11117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β
β) |
173 | | ax-icn 11044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ i β
β |
174 | 19 | ffvelcdmda 7030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β
β) |
175 | 174 | recnd 11117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β
β) |
176 | | mulcl 11069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((i
β β β§ (πβπ‘) β β) β (i Β· (πβπ‘)) β β) |
177 | 173, 175,
176 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β dom β«1
β§ π‘ β β)
β (i Β· (πβπ‘)) β β) |
178 | | addcl 11067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((πβπ‘) β β β§ (i Β· (πβπ‘)) β β) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
179 | 172, 177,
178 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β dom β«1
β§ π‘ β β)
β§ (π β dom
β«1 β§ π‘
β β)) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
180 | 179 | anandirs 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
181 | 170, 180 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β (π’(,)π€)) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
182 | 181 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β (π’(,)π€)) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
183 | 182 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β ((πβπ‘) + (i Β· (πβπ‘))) β β) |
184 | 169, 183 | subcld 11446 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
185 | 184 | abscld 15256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) β β) |
186 | 181 | abscld 15256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β (π’(,)π€)) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
187 | 186 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β (π’(,)π€)) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
188 | 187 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ((πβπ‘) + (i Β· (πβπ‘)))) β β) |
189 | 185, 188 | readdcld 11118 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))) β β) |
190 | 189 | rexrd 11139 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))) β
β*) |
191 | 184 | absge0d 15264 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β 0 β€ (absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))))) |
192 | 180 | absge0d 15264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β 0 β€ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
193 | 170, 192 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β dom β«1
β§ π β dom
β«1) β§ π‘
β (π’(,)π€)) β 0 β€
(absβ((πβπ‘) + (i Β· (πβπ‘))))) |
194 | 193 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ π‘ β (π’(,)π€)) β 0 β€ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
195 | 194 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β 0 β€ (absβ((πβπ‘) + (i Β· (πβπ‘))))) |
196 | 185, 188,
191, 195 | addge0d 11665 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β 0 β€ ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
197 | | elxrge0 13303 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))) β (0[,]+β) β
(((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))) β β* β§ 0 β€
((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))))) |
198 | 190, 196,
197 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))) β (0[,]+β)) |
199 | 156 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ Β¬ π‘ β (π’(,)π€)) β 0 β
(0[,]+β)) |
200 | 198, 199 | ifclda 4520 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0) β
(0[,]+β)) |
201 | 200 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β β) β if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0) β
(0[,]+β)) |
202 | 201 | fmpttd 7058 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))),
0)):ββΆ(0[,]+β)) |
203 | | itg2cl 25019 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)):ββΆ(0[,]+β)
β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β
β*) |
204 | 202, 203 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β
β*) |
205 | 204 | 3adantr3 1172 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β
β*) |
206 | 166, 205 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β
β*) |
207 | 206 | adantr 482 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ (π β 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))) β
β*) |
208 | | rpxr 12853 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β+
β π¦ β
β*) |
209 | 208 | ad3antlr 730 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
π¦ β
β*) |
210 | 158 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β
(0[,]+β)) |
211 | 210 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β β) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β
(0[,]+β)) |
212 | 211 | fmpttd 7058 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)),
0)):ββΆ(0[,]+β)) |
213 | 169, 183 | npcand 11450 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))) + ((πβπ‘) + (i Β· (πβπ‘)))) = (πΉβπ‘)) |
214 | 213 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ(((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))) + ((πβπ‘) + (i Β· (πβπ‘))))) = (absβ(πΉβπ‘))) |
215 | 184, 183 | abstrid 15276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ(((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘)))) + ((πβπ‘) + (i Β· (πβπ‘))))) β€ ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
216 | 214, 215 | eqbrtrrd 5128 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (absβ(πΉβπ‘)) β€ ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
217 | | iftrue 4491 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) = (absβ(πΉβπ‘))) |
218 | 217 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) = (absβ(πΉβπ‘))) |
219 | | iftrue 4491 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0) = ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
220 | 219 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0) = ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘)))))) |
221 | 216, 218,
220 | 3brtr4d 5136 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)) |
222 | 221 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) |
223 | | 0le0 12188 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 0 β€
0 |
224 | 223 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Β¬
π‘ β (π’(,)π€) β 0 β€ 0) |
225 | | iffalse 4494 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Β¬
π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) = 0) |
226 | | iffalse 4494 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Β¬
π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0) = 0) |
227 | 224, 225,
226 | 3brtr4d 5136 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (Β¬
π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)) |
228 | 222, 227 | pm2.61d1 180 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)) |
229 | 228 | ralrimivw 3146 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)) |
230 | | reex 11076 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ β
β V |
231 | 230 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β
V) |
232 | | fvex 6851 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(absβ(πΉβπ‘)) β V |
233 | | c0ex 11083 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 0 β
V |
234 | 232, 233 | ifex 4535 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β V |
235 | 234 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π‘ β β) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β V) |
236 | | ovex 7383 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))) β V |
237 | 236, 233 | ifex 4535 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0) β V |
238 | 237 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π‘ β β) β if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0) β V) |
239 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)) = (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) |
240 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)) = (π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) |
241 | 231, 235,
238, 239, 240 | ofrfval2 7629 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)) βr β€ (π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) |
242 | 241 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)) βr β€ (π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) |
243 | 229, 242 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)) βr β€ (π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) |
244 | | itg2le 25026 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)):ββΆ(0[,]+β) β§
(π‘ β β β¦
if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)):ββΆ(0[,]+β)
β§ (π‘ β β
β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)) βr β€ (π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β€ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) |
245 | 212, 202,
243, 244 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β€ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) |
246 | 245 | 3adantr3 1172 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β€ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) |
247 | 166, 246 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β€ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) |
248 | 247 | adantr 482 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β€ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), ((absβ((πΉβπ‘) β ((πβπ‘) + (i Β· (πβπ‘))))) + (absβ((πβπ‘) + (i Β· (πβπ‘))))), 0)))) |
249 | 1, 2, 3, 4, 5, 6, 7, 8 | ftc1anclem8 36044 |
. . . . . . . . . . . . . . 15
β’
(((((((π β§ (π β 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))) < π¦) |
250 | 165, 207,
209, 248, 249 | xrlelttrd 13008 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ(πΉβπ‘)), 0))) < π¦) |
251 | | simplll 774 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β π) |
252 | | simpr2 1196 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β π€ β (π΄[,]π΅)) |
253 | | oveq2 7358 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ = π€ β (π΄(,)π₯) = (π΄(,)π€)) |
254 | | itgeq1 25059 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π΄(,)π₯) = (π΄(,)π€) β β«(π΄(,)π₯)(πΉβπ‘) dπ‘ = β«(π΄(,)π€)(πΉβπ‘) dπ‘) |
255 | 253, 254 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = π€ β β«(π΄(,)π₯)(πΉβπ‘) dπ‘ = β«(π΄(,)π€)(πΉβπ‘) dπ‘) |
256 | | itgex 25057 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β«(π΄(,)π€)(πΉβπ‘) dπ‘ β V |
257 | 255, 1, 256 | fvmpt 6944 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π€ β (π΄[,]π΅) β (πΊβπ€) = β«(π΄(,)π€)(πΉβπ‘) dπ‘) |
258 | 252, 257 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (πΊβπ€) = β«(π΄(,)π€)(πΉβπ‘) dπ‘) |
259 | 2 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β π΄ β β) |
260 | 114 | sselda 3943 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π€ β (π΄[,]π΅)) β π€ β β) |
261 | 260 | 3ad2antr2 1190 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β π€ β β) |
262 | 114 | sselda 3943 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π’ β (π΄[,]π΅)) β π’ β β) |
263 | 262 | rexrd 11139 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π’ β (π΄[,]π΅)) β π’ β β*) |
264 | 263 | 3ad2antr1 1189 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β π’ β β*) |
265 | | elicc1 13237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π΄ β β*
β§ π΅ β
β*) β (π’ β (π΄[,]π΅) β (π’ β β* β§ π΄ β€ π’ β§ π’ β€ π΅))) |
266 | 132, 133,
265 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π’ β (π΄[,]π΅) β (π’ β β* β§ π΄ β€ π’ β§ π’ β€ π΅))) |
267 | 266 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π’ β (π΄[,]π΅)) β (π’ β β* β§ π΄ β€ π’ β§ π’ β€ π΅)) |
268 | 267 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π’ β (π΄[,]π΅)) β π΄ β€ π’) |
269 | 268 | 3ad2antr1 1189 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β π΄ β€ π’) |
270 | | simpr3 1197 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β π’ β€ π€) |
271 | 132 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π€ β (π΄[,]π΅)) β π΄ β
β*) |
272 | 260 | rexrd 11139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π€ β (π΄[,]π΅)) β π€ β β*) |
273 | | elicc1 13237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π΄ β β*
β§ π€ β
β*) β (π’ β (π΄[,]π€) β (π’ β β* β§ π΄ β€ π’ β§ π’ β€ π€))) |
274 | 271, 272,
273 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π€ β (π΄[,]π΅)) β (π’ β (π΄[,]π€) β (π’ β β* β§ π΄ β€ π’ β§ π’ β€ π€))) |
275 | 274 | 3ad2antr2 1190 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (π’ β (π΄[,]π€) β (π’ β β* β§ π΄ β€ π’ β§ π’ β€ π€))) |
276 | 264, 269,
270, 275 | mpbir3and 1343 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β π’ β (π΄[,]π€)) |
277 | | iooss2 13229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π΅ β β*
β§ π€ β€ π΅) β (π΄(,)π€) β (π΄(,)π΅)) |
278 | 133, 141,
277 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π€ β (π΄[,]π΅)) β (π΄(,)π€) β (π΄(,)π΅)) |
279 | 5 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π€ β (π΄[,]π΅)) β (π΄(,)π΅) β π·) |
280 | 278, 279 | sstrd 3953 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π€ β (π΄[,]π΅)) β (π΄(,)π€) β π·) |
281 | 280 | 3ad2antr2 1190 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (π΄(,)π€) β π·) |
282 | 281 | sselda 3943 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β (π΄(,)π€)) β π‘ β π·) |
283 | 148 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β π·) β (πΉβπ‘) β β) |
284 | 282, 283 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ π‘ β (π΄(,)π€)) β (πΉβπ‘) β β) |
285 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π€ = π’ β (π€ β (π΄[,]π΅) β π’ β (π΄[,]π΅))) |
286 | 285 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ = π’ β ((π β§ π€ β (π΄[,]π΅)) β (π β§ π’ β (π΄[,]π΅)))) |
287 | | oveq2 7358 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π€ = π’ β (π΄(,)π€) = (π΄(,)π’)) |
288 | 287 | mpteq1d 5199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π€ = π’ β (π‘ β (π΄(,)π€) β¦ (πΉβπ‘)) = (π‘ β (π΄(,)π’) β¦ (πΉβπ‘))) |
289 | 288 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ = π’ β ((π‘ β (π΄(,)π€) β¦ (πΉβπ‘)) β πΏ1 β (π‘ β (π΄(,)π’) β¦ (πΉβπ‘)) β
πΏ1)) |
290 | 286, 289 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π€ = π’ β (((π β§ π€ β (π΄[,]π΅)) β (π‘ β (π΄(,)π€) β¦ (πΉβπ‘)) β πΏ1) β
((π β§ π’ β (π΄[,]π΅)) β (π‘ β (π΄(,)π’) β¦ (πΉβπ‘)) β
πΏ1))) |
291 | | ioombl 24851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π΄(,)π€) β dom vol |
292 | 291 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π€ β (π΄[,]π΅)) β (π΄(,)π€) β dom vol) |
293 | 148 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π€ β (π΄[,]π΅)) β§ π‘ β π·) β (πΉβπ‘) β β) |
294 | 8 | feqmptd 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β πΉ = (π‘ β π· β¦ (πΉβπ‘))) |
295 | 294, 7 | eqeltrrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π‘ β π· β¦ (πΉβπ‘)) β
πΏ1) |
296 | 295 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π€ β (π΄[,]π΅)) β (π‘ β π· β¦ (πΉβπ‘)) β
πΏ1) |
297 | 280, 292,
293, 296 | iblss 25091 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π€ β (π΄[,]π΅)) β (π‘ β (π΄(,)π€) β¦ (πΉβπ‘)) β
πΏ1) |
298 | 290, 297 | chvarvv 2003 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π’ β (π΄[,]π΅)) β (π‘ β (π΄(,)π’) β¦ (πΉβπ‘)) β
πΏ1) |
299 | 298 | 3ad2antr1 1189 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (π‘ β (π΄(,)π’) β¦ (πΉβπ‘)) β
πΏ1) |
300 | | ioombl 24851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π’(,)π€) β dom vol |
301 | 300 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π’(,)π€) β dom vol) |
302 | | fvexd 6853 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β π·) β (πΉβπ‘) β V) |
303 | 295 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β π· β¦ (πΉβπ‘)) β
πΏ1) |
304 | 146, 301,
302, 303 | iblss 25091 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β (π’(,)π€) β¦ (πΉβπ‘)) β
πΏ1) |
305 | 304 | 3adantr3 1172 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (π‘ β (π’(,)π€) β¦ (πΉβπ‘)) β
πΏ1) |
306 | 259, 261,
276, 284, 299, 305 | itgsplitioo 25124 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β β«(π΄(,)π€)(πΉβπ‘) dπ‘ = (β«(π΄(,)π’)(πΉβπ‘) dπ‘ + β«(π’(,)π€)(πΉβπ‘) dπ‘)) |
307 | 258, 306 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (πΊβπ€) = (β«(π΄(,)π’)(πΉβπ‘) dπ‘ + β«(π’(,)π€)(πΉβπ‘) dπ‘)) |
308 | | simpr1 1195 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β π’ β (π΄[,]π΅)) |
309 | | oveq2 7358 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = π’ β (π΄(,)π₯) = (π΄(,)π’)) |
310 | | itgeq1 25059 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π΄(,)π₯) = (π΄(,)π’) β β«(π΄(,)π₯)(πΉβπ‘) dπ‘ = β«(π΄(,)π’)(πΉβπ‘) dπ‘) |
311 | 309, 310 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = π’ β β«(π΄(,)π₯)(πΉβπ‘) dπ‘ = β«(π΄(,)π’)(πΉβπ‘) dπ‘) |
312 | | itgex 25057 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β«(π΄(,)π’)(πΉβπ‘) dπ‘ β V |
313 | 311, 1, 312 | fvmpt 6944 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π’ β (π΄[,]π΅) β (πΊβπ’) = β«(π΄(,)π’)(πΉβπ‘) dπ‘) |
314 | 308, 313 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (πΊβπ’) = β«(π΄(,)π’)(πΉβπ‘) dπ‘) |
315 | 307, 314 | oveq12d 7368 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β ((πΊβπ€) β (πΊβπ’)) = ((β«(π΄(,)π’)(πΉβπ‘) dπ‘ + β«(π’(,)π€)(πΉβπ‘) dπ‘) β β«(π΄(,)π’)(πΉβπ‘) dπ‘)) |
316 | | fvexd 6853 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π’ β (π΄[,]π΅)) β§ π‘ β (π΄(,)π’)) β (πΉβπ‘) β V) |
317 | 316, 298 | itgcl 25070 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π’ β (π΄[,]π΅)) β β«(π΄(,)π’)(πΉβπ‘) dπ‘ β β) |
318 | 317 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β β«(π΄(,)π’)(πΉβπ‘) dπ‘ β β) |
319 | | fvexd 6853 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β (π’(,)π€)) β (πΉβπ‘) β V) |
320 | 319, 304 | itgcl 25070 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β β«(π’(,)π€)(πΉβπ‘) dπ‘ β β) |
321 | 318, 320 | pncan2d 11448 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((β«(π΄(,)π’)(πΉβπ‘) dπ‘ + β«(π’(,)π€)(πΉβπ‘) dπ‘) β β«(π΄(,)π’)(πΉβπ‘) dπ‘) = β«(π’(,)π€)(πΉβπ‘) dπ‘) |
322 | 321 | 3adantr3 1172 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β ((β«(π΄(,)π’)(πΉβπ‘) dπ‘ + β«(π’(,)π€)(πΉβπ‘) dπ‘) β β«(π΄(,)π’)(πΉβπ‘) dπ‘) = β«(π’(,)π€)(πΉβπ‘) dπ‘) |
323 | 315, 322 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β ((πΊβπ€) β (πΊβπ’)) = β«(π’(,)π€)(πΉβπ‘) dπ‘) |
324 | 323 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (absβ((πΊβπ€) β (πΊβπ’))) = (absββ«(π’(,)π€)(πΉβπ‘) dπ‘)) |
325 | | ftc1anc.t |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β βπ β ((,) β ((π΄[,]π΅) Γ (π΄[,]π΅)))(absββ«π (πΉβπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π , (absβ(πΉβπ‘)), 0)))) |
326 | | df-ov 7353 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π’(,)π€) = ((,)ββ¨π’, π€β©) |
327 | | opelxpi 5668 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅)) β β¨π’, π€β© β ((π΄[,]π΅) Γ (π΄[,]π΅))) |
328 | | ioof 13293 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(,):(β* Γ β*)βΆπ«
β |
329 | | ffn 6664 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
330 | 328, 329 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (,) Fn
(β* Γ β*) |
331 | | iccssxr 13276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π΄[,]π΅) β
β* |
332 | | xpss12 5646 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π΄[,]π΅) β β* β§ (π΄[,]π΅) β β*) β
((π΄[,]π΅) Γ (π΄[,]π΅)) β (β* Γ
β*)) |
333 | 331, 331,
332 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π΄[,]π΅) Γ (π΄[,]π΅)) β (β* Γ
β*) |
334 | | fnfvima 7178 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((,) Fn
(β* Γ β*) β§ ((π΄[,]π΅) Γ (π΄[,]π΅)) β (β* Γ
β*) β§ β¨π’, π€β© β ((π΄[,]π΅) Γ (π΄[,]π΅))) β ((,)ββ¨π’, π€β©) β ((,) β ((π΄[,]π΅) Γ (π΄[,]π΅)))) |
335 | 330, 333,
334 | mp3an12 1452 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(β¨π’, π€β© β ((π΄[,]π΅) Γ (π΄[,]π΅)) β ((,)ββ¨π’, π€β©) β ((,) β ((π΄[,]π΅) Γ (π΄[,]π΅)))) |
336 | 327, 335 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅)) β ((,)ββ¨π’, π€β©) β ((,) β ((π΄[,]π΅) Γ (π΄[,]π΅)))) |
337 | 326, 336 | eqeltrid 2843 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅)) β (π’(,)π€) β ((,) β ((π΄[,]π΅) Γ (π΄[,]π΅)))) |
338 | | itgeq1 25059 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π’(,)π€) β β«π (πΉβπ‘) dπ‘ = β«(π’(,)π€)(πΉβπ‘) dπ‘) |
339 | 338 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π’(,)π€) β (absββ«π (πΉβπ‘) dπ‘) = (absββ«(π’(,)π€)(πΉβπ‘) dπ‘)) |
340 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (π’(,)π€) β (π‘ β π β π‘ β (π’(,)π€))) |
341 | 340 | ifbid 4508 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (π’(,)π€) β if(π‘ β π , (absβ(πΉβπ‘)), 0) = if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)) |
342 | 341 | mpteq2dv 5206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π’(,)π€) β (π‘ β β β¦ if(π‘ β π , (absβ(πΉβπ‘)), 0)) = (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) |
343 | 342 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π’(,)π€) β (β«2β(π‘ β β β¦ if(π‘ β π , (absβ(πΉβπ‘)), 0))) = (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)))) |
344 | 339, 343 | breq12d 5117 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π’(,)π€) β ((absββ«π (πΉβπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π , (absβ(πΉβπ‘)), 0))) β (absββ«(π’(,)π€)(πΉβπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))))) |
345 | 344 | rspccva 3579 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((βπ β
((,) β ((π΄[,]π΅) Γ (π΄[,]π΅)))(absββ«π (πΉβπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π , (absβ(πΉβπ‘)), 0))) β§ (π’(,)π€) β ((,) β ((π΄[,]π΅) Γ (π΄[,]π΅)))) β (absββ«(π’(,)π€)(πΉβπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)))) |
346 | 325, 337,
345 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (absββ«(π’(,)π€)(πΉβπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)))) |
347 | 346 | 3adantr3 1172 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (absββ«(π’(,)π€)(πΉβπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)))) |
348 | 324, 347 | eqbrtrd 5126 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (absβ((πΊβπ€) β (πΊβπ’))) β€ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)))) |
349 | 348 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (absβ((πΊβπ€) β (πΊβπ’))) β€ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)))) |
350 | | subcl 11334 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πΊβπ€) β β β§ (πΊβπ’) β β) β ((πΊβπ€) β (πΊβπ’)) β β) |
351 | 124, 125,
350 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π’ β (π΄[,]π΅)) β§ (π β§ π€ β (π΄[,]π΅))) β ((πΊβπ€) β (πΊβπ’)) β β) |
352 | 351 | anandis 677 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((πΊβπ€) β (πΊβπ’)) β β) |
353 | 352 | abscld 15256 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (absβ((πΊβπ€) β (πΊβπ’))) β β) |
354 | 353 | rexrd 11139 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (absβ((πΊβπ€) β (πΊβπ’))) β
β*) |
355 | 354 | 3adantr3 1172 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (absβ((πΊβπ€) β (πΊβπ’))) β
β*) |
356 | 355 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (absβ((πΊβπ€) β (πΊβπ’))) β
β*) |
357 | 163 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β
β*) |
358 | 208 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β π¦ β β*) |
359 | | xrlelttr 13004 |
. . . . . . . . . . . . . . . . . 18
β’
(((absβ((πΊβπ€) β (πΊβπ’))) β β* β§
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β β* β§
π¦ β
β*) β (((absβ((πΊβπ€) β (πΊβπ’))) β€ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β§
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ(πΉβπ‘)), 0))) < π¦) β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
360 | 356, 357,
358, 359 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (((absβ((πΊβπ€) β (πΊβπ’))) β€ (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β§
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ(πΉβπ‘)), 0))) < π¦) β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
361 | 349, 360 | mpand 694 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β ((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) < π¦ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
362 | 251, 361 | sylanl1 679 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β ((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) < π¦ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
363 | 362 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
((β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) < π¦ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
364 | 250, 363 | mpd 15 |
. . . . . . . . . . . . 13
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β§ (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < )))) β
(absβ((πΊβπ€) β (πΊβπ’))) < π¦) |
365 | 364 | ex 414 |
. . . . . . . . . . . 12
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β ((absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
366 | 102, 112,
115, 131, 365 | wlogle 11622 |
. . . . . . . . . . 11
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
367 | 366 | anassrs 469 |
. . . . . . . . . 10
β’
(((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π¦ β β+) β§ π’ β (π΄[,]π΅)) β§ π€ β (π΄[,]π΅)) β ((absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
368 | 92, 367 | sylanb 582 |
. . . . . . . . 9
β’
((((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β§ π€ β (π΄[,]π΅)) β ((absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
369 | 368 | ralrimiva 3142 |
. . . . . . . 8
β’
(((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
370 | | breq2 5108 |
. . . . . . . . 9
β’ (π§ = ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
((absβ(π€ β
π’)) < π§ β (absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, <
))))) |
371 | 370 | rspceaimv 3584 |
. . . . . . . 8
β’ ((((π¦ / 2) / (2 Β· sup((abs
β (ran π βͺ ran
π)), β, < )))
β β+ β§ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < ((π¦ / 2) / (2 Β· sup((abs β (ran
π βͺ ran π)), β, < ))) β
(absβ((πΊβπ€) β (πΊβπ’))) < π¦)) β βπ§ β β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
372 | 81, 369, 371 | syl2anc 585 |
. . . . . . 7
β’
(((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π β 0) β βπ§ β β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
373 | | ralnex 3074 |
. . . . . . . . 9
β’
(βπ β
(ran π βͺ ran π) Β¬ π β 0 β Β¬ βπ β (ran π βͺ ran π)π β 0) |
374 | | nne 2946 |
. . . . . . . . . 10
β’ (Β¬
π β 0 β π = 0) |
375 | 374 | ralbii 3095 |
. . . . . . . . 9
β’
(βπ β
(ran π βͺ ran π) Β¬ π β 0 β βπ β (ran π βͺ ran π)π = 0) |
376 | 373, 375 | bitr3i 277 |
. . . . . . . 8
β’ (Β¬
βπ β (ran π βͺ ran π)π β 0 β βπ β (ran π βͺ ran π)π = 0) |
377 | 16 | ffnd 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β dom β«1
β π Fn
β) |
378 | | fnfvelrn 7027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π Fn β β§ π‘ β β) β (πβπ‘) β ran π) |
379 | 377, 378 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β ran π) |
380 | | elun1 4135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((πβπ‘) β ran π β (πβπ‘) β (ran π βͺ ran π)) |
381 | 379, 380 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β (ran π βͺ ran π)) |
382 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = (πβπ‘) β (π = 0 β (πβπ‘) = 0)) |
383 | 382 | rspcva 3578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((πβπ‘) β (ran π βͺ ran π) β§ βπ β (ran π βͺ ran π)π = 0) β (πβπ‘) = 0) |
384 | 381, 383 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β dom β«1
β§ π‘ β β)
β§ βπ β (ran
π βͺ ran π)π = 0) β (πβπ‘) = 0) |
385 | 384 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β§ βπ β (ran π βͺ ran π)π = 0) β (πβπ‘) = 0) |
386 | 19 | ffnd 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β dom β«1
β π Fn
β) |
387 | | fnfvelrn 7027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π Fn β β§ π‘ β β) β (πβπ‘) β ran π) |
388 | 386, 387 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β ran π) |
389 | | elun2 4136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((πβπ‘) β ran π β (πβπ‘) β (ran π βͺ ran π)) |
390 | 388, 389 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β dom β«1
β§ π‘ β β)
β (πβπ‘) β (ran π βͺ ran π)) |
391 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π = (πβπ‘) β (π = 0 β (πβπ‘) = 0)) |
392 | 391 | rspcva 3578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((πβπ‘) β (ran π βͺ ran π) β§ βπ β (ran π βͺ ran π)π = 0) β (πβπ‘) = 0) |
393 | 392 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((πβπ‘) β (ran π βͺ ran π) β§ βπ β (ran π βͺ ran π)π = 0) β (i Β· (πβπ‘)) = (i Β· 0)) |
394 | | it0e0 12309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (i
Β· 0) = 0 |
395 | 393, 394 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((πβπ‘) β (ran π βͺ ran π) β§ βπ β (ran π βͺ ran π)π = 0) β (i Β· (πβπ‘)) = 0) |
396 | 390, 395 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β dom β«1
β§ π‘ β β)
β§ βπ β (ran
π βͺ ran π)π = 0) β (i Β· (πβπ‘)) = 0) |
397 | 396 | adantlll 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β§ βπ β (ran π βͺ ran π)π = 0) β (i Β· (πβπ‘)) = 0) |
398 | 385, 397 | oveq12d 7368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β dom β«1
β§ π β dom
β«1) β§ π‘
β β) β§ βπ β (ran π βͺ ran π)π = 0) β ((πβπ‘) + (i Β· (πβπ‘))) = (0 + 0)) |
399 | 398 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β dom β«1
β§ π β dom
β«1) β§ βπ β (ran π βͺ ran π)π = 0) β§ π‘ β β) β ((πβπ‘) + (i Β· (πβπ‘))) = (0 + 0)) |
400 | | 00id 11264 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (0 + 0) =
0 |
401 | 399, 400 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β dom β«1
β§ π β dom
β«1) β§ βπ β (ran π βͺ ran π)π = 0) β§ π‘ β β) β ((πβπ‘) + (i Β· (πβπ‘))) = 0) |
402 | 401 | adantlll 717 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π = 0) β§ π‘ β β) β ((πβπ‘) + (i Β· (πβπ‘))) = 0) |
403 | 402 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π = 0) β§ π‘ β β) β (if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))) = (if(π‘ β π·, (πΉβπ‘), 0) β 0)) |
404 | | 0cnd 11082 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ Β¬ π‘ β π·) β 0 β β) |
405 | 148, 404 | ifclda 4520 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β if(π‘ β π·, (πΉβπ‘), 0) β β) |
406 | 405 | subid1d 11435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (if(π‘ β π·, (πΉβπ‘), 0) β 0) = if(π‘ β π·, (πΉβπ‘), 0)) |
407 | 406 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π = 0) β§ π‘ β β) β (if(π‘ β π·, (πΉβπ‘), 0) β 0) = if(π‘ β π·, (πΉβπ‘), 0)) |
408 | 403, 407 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π = 0) β§ π‘ β β) β (if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))) = if(π‘ β π·, (πΉβπ‘), 0)) |
409 | 408 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π = 0) β§ π‘ β β) β (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))) = (absβif(π‘ β π·, (πΉβπ‘), 0))) |
410 | | fvif 6854 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(absβif(π‘
β π·, (πΉβπ‘), 0)) = if(π‘ β π·, (absβ(πΉβπ‘)), (absβ0)) |
411 | | abs0 15105 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(absβ0) = 0 |
412 | | ifeq2 4490 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((absβ0) = 0 β if(π‘ β π·, (absβ(πΉβπ‘)), (absβ0)) = if(π‘ β π·, (absβ(πΉβπ‘)), 0)) |
413 | 411, 412 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ if(π‘ β π·, (absβ(πΉβπ‘)), (absβ0)) = if(π‘ β π·, (absβ(πΉβπ‘)), 0) |
414 | 410, 413 | eqtri 2766 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(absβif(π‘
β π·, (πΉβπ‘), 0)) = if(π‘ β π·, (absβ(πΉβπ‘)), 0) |
415 | 409, 414 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π = 0) β§ π‘ β β) β (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))) = if(π‘ β π·, (absβ(πΉβπ‘)), 0)) |
416 | 415 | mpteq2dva 5204 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π = 0) β (π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘)))))) = (π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) |
417 | 416 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π = 0) β (β«2β(π‘ β β β¦
(absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) = (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)))) |
418 | 417 | breq1d 5114 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π = 0) β ((β«2β(π‘ β β β¦
(absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2))) |
419 | 418 | biimpd 228 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ βπ β (ran
π βͺ ran π)π = 0) β ((β«2β(π‘ β β β¦
(absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2))) |
420 | 419 | ex 414 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (βπ β
(ran π βͺ ran π)π = 0 β ((β«2β(π‘ β β β¦
(absβ(if(π‘ β
π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)))) |
421 | 420 | com23 86 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β ((β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2) β (βπ β (ran π βͺ ran π)π = 0 β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)))) |
422 | 421 | imp32 420 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ ((β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2) β§ βπ β (ran π βͺ ran π)π = 0)) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) |
423 | 422 | anasss 468 |
. . . . . . . . . . . 12
β’ ((π β§ ((π β dom β«1 β§ π β dom β«1)
β§ ((β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2) β§ βπ β (ran π βͺ ran π)π = 0))) β
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) |
424 | 423 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ ((π β dom β«1
β§ π β dom
β«1) β§ ((β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2) β§ βπ β (ran π βͺ ran π)π = 0))) β
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) |
425 | | 1rp 12848 |
. . . . . . . . . . . . 13
β’ 1 β
β+ |
426 | 425 | ne0ii 4296 |
. . . . . . . . . . . 12
β’
β+ β β
|
427 | 352 | anassrs 469 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π’ β (π΄[,]π΅)) β§ π€ β (π΄[,]π΅)) β ((πΊβπ€) β (πΊβπ’)) β β) |
428 | 427 | abscld 15256 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π’ β (π΄[,]π΅)) β§ π€ β (π΄[,]π΅)) β (absβ((πΊβπ€) β (πΊβπ’))) β β) |
429 | 428 | adantlrr 720 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ π€ β (π΄[,]π΅)) β (absβ((πΊβπ€) β (πΊβπ’))) β β) |
430 | 429 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β§ π€ β (π΄[,]π΅)) β (absβ((πΊβπ€) β (πΊβπ’))) β β) |
431 | | rpre 12852 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β β+
β π¦ β
β) |
432 | 431 | rehalfcld 12334 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β β+
β (π¦ / 2) β
β) |
433 | 432 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β (π΄[,]π΅) β§ π¦ β β+) β (π¦ / 2) β
β) |
434 | 433 | ad3antlr 730 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β§ π€ β (π΄[,]π΅)) β (π¦ / 2) β β) |
435 | 431 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β (π΄[,]π΅) β§ π¦ β β+) β π¦ β
β) |
436 | 435 | ad3antlr 730 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β§ π€ β (π΄[,]π΅)) β π¦ β β) |
437 | 430 | rexrd 11139 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β§ π€ β (π΄[,]π΅)) β (absβ((πΊβπ€) β (πΊβπ’))) β
β*) |
438 | 156 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ Β¬ π‘ β π·) β 0 β
(0[,]+β)) |
439 | 153, 438 | ifclda 4520 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β if(π‘ β π·, (absβ(πΉβπ‘)), 0) β
(0[,]+β)) |
440 | 439 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π‘ β β) β if(π‘ β π·, (absβ(πΉβπ‘)), 0) β
(0[,]+β)) |
441 | 440 | fmpttd 7058 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)),
0)):ββΆ(0[,]+β)) |
442 | | itg2cl 25019 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)):ββΆ(0[,]+β) β
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) β
β*) |
443 | 441, 442 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) β
β*) |
444 | 443 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β§ π€ β (π΄[,]π΅)) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) β
β*) |
445 | 434 | rexrd 11139 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β§ π€ β (π΄[,]π΅)) β (π¦ / 2) β
β*) |
446 | 108, 107 | oveqan12rd 7370 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π = π’ β§ π = π€) β ((πΊβπ) β (πΊβπ)) = ((πΊβπ€) β (πΊβπ’))) |
447 | 446 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π = π’ β§ π = π€) β (absβ((πΊβπ) β (πΊβπ))) = (absβ((πΊβπ€) β (πΊβπ’)))) |
448 | 447 | breq1d 5114 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π = π’ β§ π = π€) β ((absβ((πΊβπ) β (πΊβπ))) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) β (absβ((πΊβπ€) β (πΊβπ’))) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))))) |
449 | 98, 97 | oveqan12rd 7370 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π = π€ β§ π = π’) β ((πΊβπ) β (πΊβπ)) = ((πΊβπ’) β (πΊβπ€))) |
450 | 449 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π = π€ β§ π = π’) β (absβ((πΊβπ) β (πΊβπ))) = (absβ((πΊβπ’) β (πΊβπ€)))) |
451 | 450 | breq1d 5114 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π = π€ β§ π = π’) β ((absβ((πΊβπ) β (πΊβπ))) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) β (absβ((πΊβπ’) β (πΊβπ€))) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))))) |
452 | 128 | breq1d 5114 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((absβ((πΊβπ€) β (πΊβπ’))) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) β (absβ((πΊβπ’) β (πΊβπ€))) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))))) |
453 | 320 | abscld 15256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (absββ«(π’(,)π€)(πΉβπ‘) dπ‘) β β) |
454 | 453 | rexrd 11139 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (absββ«(π’(,)π€)(πΉβπ‘) dπ‘) β
β*) |
455 | 443 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) β
β*) |
456 | 441 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)),
0)):ββΆ(0[,]+β)) |
457 | | breq2 5108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((absβ(πΉβπ‘)) = if(π‘ β π·, (absβ(πΉβπ‘)), 0) β (if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ (absβ(πΉβπ‘)) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) |
458 | | breq2 5108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (0 =
if(π‘ β π·, (absβ(πΉβπ‘)), 0) β (if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ 0 β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) |
459 | 149 | leidd 11655 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π‘ β π·) β (absβ(πΉβπ‘)) β€ (absβ(πΉβπ‘))) |
460 | | breq1 5107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((absβ(πΉβπ‘)) = if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β ((absβ(πΉβπ‘)) β€ (absβ(πΉβπ‘)) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ (absβ(πΉβπ‘)))) |
461 | | breq1 5107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (0 =
if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β (0 β€ (absβ(πΉβπ‘)) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ (absβ(πΉβπ‘)))) |
462 | 460, 461 | ifboth 4524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((absβ(πΉβπ‘)) β€ (absβ(πΉβπ‘)) β§ 0 β€ (absβ(πΉβπ‘))) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ (absβ(πΉβπ‘))) |
463 | 459, 151,
462 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π‘ β π·) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ (absβ(πΉβπ‘))) |
464 | 463 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ π‘ β π·) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ (absβ(πΉβπ‘))) |
465 | 146 | ssneld 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (Β¬ π‘ β π· β Β¬ π‘ β (π’(,)π€))) |
466 | 465 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ Β¬ π‘ β π·) β Β¬ π‘ β (π’(,)π€)) |
467 | 225, 223 | eqbrtrdi 5143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (Β¬
π‘ β (π’(,)π€) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ 0) |
468 | 466, 467 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β§ Β¬ π‘ β π·) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ 0) |
469 | 457, 458,
464, 468 | ifbothda 4523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ if(π‘ β π·, (absβ(πΉβπ‘)), 0)) |
470 | 469 | ralrimivw 3146 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ if(π‘ β π·, (absβ(πΉβπ‘)), 0)) |
471 | 232, 233 | ifex 4535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ if(π‘ β π·, (absβ(πΉβπ‘)), 0) β V |
472 | 471 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π‘ β β) β if(π‘ β π·, (absβ(πΉβπ‘)), 0) β V) |
473 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)) = (π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) |
474 | 231, 235,
472, 239, 473 | ofrfval2 7629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)) βr β€ (π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) |
475 | 474 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β ((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)) βr β€ (π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)) β βπ‘ β β if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0) β€ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) |
476 | 470, 475 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)) βr β€ (π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) |
477 | | itg2le 25026 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)):ββΆ(0[,]+β) β§
(π‘ β β β¦
if(π‘ β π·, (absβ(πΉβπ‘)), 0)):ββΆ(0[,]+β) β§
(π‘ β β β¦
if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0)) βr β€ (π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) β
(β«2β(π‘
β β β¦ if(π‘
β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)))) |
478 | 160, 456,
476, 477 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (β«2β(π‘ β β β¦ if(π‘ β (π’(,)π€), (absβ(πΉβπ‘)), 0))) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)))) |
479 | 454, 162,
455, 346, 478 | xrletrd 13010 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (absββ«(π’(,)π€)(πΉβπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)))) |
480 | 479 | 3adantr3 1172 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (absββ«(π’(,)π€)(πΉβπ‘) dπ‘) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)))) |
481 | 324, 480 | eqbrtrd 5126 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅) β§ π’ β€ π€)) β (absβ((πΊβπ€) β (πΊβπ’))) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)))) |
482 | 448, 451,
114, 452, 481 | wlogle 11622 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π€ β (π΄[,]π΅))) β (absβ((πΊβπ€) β (πΊβπ’))) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)))) |
483 | 482 | anassrs 469 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π’ β (π΄[,]π΅)) β§ π€ β (π΄[,]π΅)) β (absβ((πΊβπ€) β (πΊβπ’))) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)))) |
484 | 483 | adantlrr 720 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ π€ β (π΄[,]π΅)) β (absβ((πΊβπ€) β (πΊβπ’))) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)))) |
485 | 484 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β§ π€ β (π΄[,]π΅)) β (absβ((πΊβπ€) β (πΊβπ’))) β€ (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0)))) |
486 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β§ π€ β (π΄[,]π΅)) β (β«2β(π‘ β β β¦ if(π‘ β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) |
487 | 437, 444,
445, 485, 486 | xrlelttrd 13008 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β§ π€ β (π΄[,]π΅)) β (absβ((πΊβπ€) β (πΊβπ’))) < (π¦ / 2)) |
488 | | rphalflt 12873 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β β+
β (π¦ / 2) < π¦) |
489 | 488 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β (π΄[,]π΅) β§ π¦ β β+) β (π¦ / 2) < π¦) |
490 | 489 | ad3antlr 730 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β§ π€ β (π΄[,]π΅)) β (π¦ / 2) < π¦) |
491 | 430, 434,
436, 487, 490 | lttrd 11250 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β§ π€ β (π΄[,]π΅)) β (absβ((πΊβπ€) β (πΊβπ’))) < π¦) |
492 | 491 | a1d 25 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β§ π€ β (π΄[,]π΅)) β ((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
493 | 492 | ralrimiva 3142 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
494 | 493 | ralrimivw 3146 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β βπ§ β β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
495 | | r19.2z 4451 |
. . . . . . . . . . . 12
β’
((β+ β β
β§ βπ§ β β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) β βπ§ β β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
496 | 426, 494,
495 | sylancr 588 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§
(β«2β(π‘
β β β¦ if(π‘
β π·, (absβ(πΉβπ‘)), 0))) < (π¦ / 2)) β βπ§ β β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
497 | 424, 496 | syldan 592 |
. . . . . . . . . 10
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ ((π β dom β«1
β§ π β dom
β«1) β§ ((β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2) β§ βπ β (ran π βͺ ran π)π = 0))) β βπ§ β β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
498 | 497 | anassrs 469 |
. . . . . . . . 9
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ ((β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2) β§ βπ β (ran π βͺ ran π)π = 0)) β βπ§ β β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
499 | 498 | anassrs 469 |
. . . . . . . 8
β’
(((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ βπ β (ran π βͺ ran π)π = 0) β βπ§ β β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
500 | 376, 499 | sylan2b 595 |
. . . . . . 7
β’
(((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β§ Β¬ βπ β (ran π βͺ ran π)π β 0) β βπ§ β β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
501 | 372, 500 | pm2.61dan 812 |
. . . . . 6
β’ ((((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β§ (β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2)) β βπ§ β β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
502 | 501 | ex 414 |
. . . . 5
β’ (((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β§ (π β dom β«1
β§ π β dom
β«1)) β ((β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2) β βπ§ β β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦))) |
503 | 502 | rexlimdvva 3204 |
. . . 4
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β
(βπ β dom
β«1βπ
β dom β«1(β«2β(π‘ β β β¦ (absβ(if(π‘ β π·, (πΉβπ‘), 0) β ((πβπ‘) + (i Β· (πβπ‘))))))) < (π¦ / 2) β βπ§ β β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦))) |
504 | 13, 503 | mpd 15 |
. . 3
β’ ((π β§ (π’ β (π΄[,]π΅) β§ π¦ β β+)) β
βπ§ β
β+ βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
505 | 504 | ralrimivva 3196 |
. 2
β’ (π β βπ’ β (π΄[,]π΅)βπ¦ β β+ βπ§ β β+
βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)) |
506 | | ssid 3965 |
. . 3
β’ β
β β |
507 | | elcncf2 24175 |
. . 3
β’ (((π΄[,]π΅) β β β§ β β
β) β (πΊ β
((π΄[,]π΅)βcnββ) β (πΊ:(π΄[,]π΅)βΆβ β§ βπ’ β (π΄[,]π΅)βπ¦ β β+ βπ§ β β+
βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)))) |
508 | 117, 506,
507 | sylancl 587 |
. 2
β’ (π β (πΊ β ((π΄[,]π΅)βcnββ) β (πΊ:(π΄[,]π΅)βΆβ β§ βπ’ β (π΄[,]π΅)βπ¦ β β+ βπ§ β β+
βπ€ β (π΄[,]π΅)((absβ(π€ β π’)) < π§ β (absβ((πΊβπ€) β (πΊβπ’))) < π¦)))) |
509 | 9, 505, 508 | mpbir2and 712 |
1
β’ (π β πΊ β ((π΄[,]π΅)βcnββ)) |