Step | Hyp | Ref
| Expression |
1 | | c1liplem1.k |
. . 3
β’ πΎ = sup((abs β ((β D
πΉ) β (π΄[,]π΅))), β, < ) |
2 | | imassrn 6029 |
. . . . . 6
β’ (abs
β ((β D πΉ)
β (π΄[,]π΅))) β ran
abs |
3 | | absf 15229 |
. . . . . . 7
β’
abs:ββΆβ |
4 | | frn 6680 |
. . . . . . 7
β’
(abs:ββΆβ β ran abs β
β) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
β’ ran abs
β β |
6 | 2, 5 | sstri 3958 |
. . . . 5
β’ (abs
β ((β D πΉ)
β (π΄[,]π΅))) β
β |
7 | 6 | a1i 11 |
. . . 4
β’ (π β (abs β ((β D
πΉ) β (π΄[,]π΅))) β β) |
8 | | dvf 25287 |
. . . . . . . 8
β’ (β
D πΉ):dom (β D πΉ)βΆβ |
9 | | ffun 6676 |
. . . . . . . 8
β’ ((β
D πΉ):dom (β D πΉ)βΆβ β Fun
(β D πΉ)) |
10 | 8, 9 | ax-mp 5 |
. . . . . . 7
β’ Fun
(β D πΉ) |
11 | 10 | a1i 11 |
. . . . . 6
β’ (π β Fun (β D πΉ)) |
12 | | c1liplem1.dv |
. . . . . . . 8
β’ (π β ((β D πΉ) βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) |
13 | | cncff 24272 |
. . . . . . . 8
β’
(((β D πΉ)
βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ) β ((β D πΉ) βΎ (π΄[,]π΅)):(π΄[,]π΅)βΆβ) |
14 | | fdm 6682 |
. . . . . . . 8
β’
(((β D πΉ)
βΎ (π΄[,]π΅)):(π΄[,]π΅)βΆβ β dom ((β D
πΉ) βΎ (π΄[,]π΅)) = (π΄[,]π΅)) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . 7
β’ (π β dom ((β D πΉ) βΎ (π΄[,]π΅)) = (π΄[,]π΅)) |
16 | | ssdmres 5965 |
. . . . . . 7
β’ ((π΄[,]π΅) β dom (β D πΉ) β dom ((β D πΉ) βΎ (π΄[,]π΅)) = (π΄[,]π΅)) |
17 | 15, 16 | sylibr 233 |
. . . . . 6
β’ (π β (π΄[,]π΅) β dom (β D πΉ)) |
18 | | c1liplem1.a |
. . . . . . . 8
β’ (π β π΄ β β) |
19 | 18 | rexrd 11212 |
. . . . . . 7
β’ (π β π΄ β
β*) |
20 | | c1liplem1.b |
. . . . . . . 8
β’ (π β π΅ β β) |
21 | 20 | rexrd 11212 |
. . . . . . 7
β’ (π β π΅ β
β*) |
22 | | c1liplem1.le |
. . . . . . 7
β’ (π β π΄ β€ π΅) |
23 | | lbicc2 13388 |
. . . . . . 7
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΄ β (π΄[,]π΅)) |
24 | 19, 21, 22, 23 | syl3anc 1372 |
. . . . . 6
β’ (π β π΄ β (π΄[,]π΅)) |
25 | | funfvima2 7186 |
. . . . . . 7
β’ ((Fun
(β D πΉ) β§ (π΄[,]π΅) β dom (β D πΉ)) β (π΄ β (π΄[,]π΅) β ((β D πΉ)βπ΄) β ((β D πΉ) β (π΄[,]π΅)))) |
26 | 25 | imp 408 |
. . . . . 6
β’ (((Fun
(β D πΉ) β§ (π΄[,]π΅) β dom (β D πΉ)) β§ π΄ β (π΄[,]π΅)) β ((β D πΉ)βπ΄) β ((β D πΉ) β (π΄[,]π΅))) |
27 | 11, 17, 24, 26 | syl21anc 837 |
. . . . 5
β’ (π β ((β D πΉ)βπ΄) β ((β D πΉ) β (π΄[,]π΅))) |
28 | | ffun 6676 |
. . . . . . 7
β’
(abs:ββΆβ β Fun abs) |
29 | 3, 28 | ax-mp 5 |
. . . . . 6
β’ Fun
abs |
30 | | imassrn 6029 |
. . . . . . . 8
β’ ((β
D πΉ) β (π΄[,]π΅)) β ran (β D πΉ) |
31 | | frn 6680 |
. . . . . . . . 9
β’ ((β
D πΉ):dom (β D πΉ)βΆβ β ran
(β D πΉ) β
β) |
32 | 8, 31 | ax-mp 5 |
. . . . . . . 8
β’ ran
(β D πΉ) β
β |
33 | 30, 32 | sstri 3958 |
. . . . . . 7
β’ ((β
D πΉ) β (π΄[,]π΅)) β β |
34 | 3 | fdmi 6685 |
. . . . . . 7
β’ dom abs =
β |
35 | 33, 34 | sseqtrri 3986 |
. . . . . 6
β’ ((β
D πΉ) β (π΄[,]π΅)) β dom abs |
36 | | funfvima2 7186 |
. . . . . 6
β’ ((Fun abs
β§ ((β D πΉ)
β (π΄[,]π΅)) β dom abs) β
(((β D πΉ)βπ΄) β ((β D πΉ) β (π΄[,]π΅)) β (absβ((β D πΉ)βπ΄)) β (abs β ((β D πΉ) β (π΄[,]π΅))))) |
37 | 29, 35, 36 | mp2an 691 |
. . . . 5
β’
(((β D πΉ)βπ΄) β ((β D πΉ) β (π΄[,]π΅)) β (absβ((β D πΉ)βπ΄)) β (abs β ((β D πΉ) β (π΄[,]π΅)))) |
38 | | ne0i 4299 |
. . . . 5
β’
((absβ((β D πΉ)βπ΄)) β (abs β ((β D πΉ) β (π΄[,]π΅))) β (abs β ((β D πΉ) β (π΄[,]π΅))) β β
) |
39 | 27, 37, 38 | 3syl 18 |
. . . 4
β’ (π β (abs β ((β D
πΉ) β (π΄[,]π΅))) β β
) |
40 | | ax-resscn 11115 |
. . . . . . . 8
β’ β
β β |
41 | | ssid 3971 |
. . . . . . . 8
β’ β
β β |
42 | | cncfss 24278 |
. . . . . . . 8
β’ ((β
β β β§ β β β) β ((π΄[,]π΅)βcnββ) β ((π΄[,]π΅)βcnββ)) |
43 | 40, 41, 42 | mp2an 691 |
. . . . . . 7
β’ ((π΄[,]π΅)βcnββ) β ((π΄[,]π΅)βcnββ) |
44 | 43, 12 | sselid 3947 |
. . . . . 6
β’ (π β ((β D πΉ) βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) |
45 | | cniccbdd 24841 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β β§ ((β
D πΉ) βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) β βπ β β βπ₯ β (π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π) |
46 | 18, 20, 44, 45 | syl3anc 1372 |
. . . . 5
β’ (π β βπ β β βπ₯ β (π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π) |
47 | | fvelima 6913 |
. . . . . . . . . 10
β’ ((Fun abs
β§ π β (abs β
((β D πΉ) β
(π΄[,]π΅)))) β βπ¦ β ((β D πΉ) β (π΄[,]π΅))(absβπ¦) = π) |
48 | 29, 47 | mpan 689 |
. . . . . . . . 9
β’ (π β (abs β ((β D
πΉ) β (π΄[,]π΅))) β βπ¦ β ((β D πΉ) β (π΄[,]π΅))(absβπ¦) = π) |
49 | | fvres 6866 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄[,]π΅) β (((β D πΉ) βΎ (π΄[,]π΅))βπ) = ((β D πΉ)βπ)) |
50 | 49 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’
((βπ₯ β
(π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π β§ π β (π΄[,]π΅)) β (((β D πΉ) βΎ (π΄[,]π΅))βπ) = ((β D πΉ)βπ)) |
51 | 50 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’
((βπ₯ β
(π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π β§ π β (π΄[,]π΅)) β (absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ)) = (absβ((β D πΉ)βπ))) |
52 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β (absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) = (absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ))) |
53 | 52 | breq1d 5120 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β ((absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π β (absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ)) β€ π)) |
54 | 53 | rspccva 3583 |
. . . . . . . . . . . . . . . 16
β’
((βπ₯ β
(π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π β§ π β (π΄[,]π΅)) β (absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ)) β€ π) |
55 | 51, 54 | eqbrtrrd 5134 |
. . . . . . . . . . . . . . 15
β’
((βπ₯ β
(π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π β§ π β (π΄[,]π΅)) β (absβ((β D πΉ)βπ)) β€ π) |
56 | 55 | adantll 713 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ βπ₯ β (π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π) β§ π β (π΄[,]π΅)) β (absβ((β D πΉ)βπ)) β€ π) |
57 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’
(((β D πΉ)βπ) = π¦ β (absβ((β D πΉ)βπ)) = (absβπ¦)) |
58 | 57 | breq1d 5120 |
. . . . . . . . . . . . . 14
β’
(((β D πΉ)βπ) = π¦ β ((absβ((β D πΉ)βπ)) β€ π β (absβπ¦) β€ π)) |
59 | 56, 58 | syl5ibcom 244 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ βπ₯ β (π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π) β§ π β (π΄[,]π΅)) β (((β D πΉ)βπ) = π¦ β (absβπ¦) β€ π)) |
60 | 59 | rexlimdva 3153 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ βπ₯ β (π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π) β (βπ β (π΄[,]π΅)((β D πΉ)βπ) = π¦ β (absβπ¦) β€ π)) |
61 | | fvelima 6913 |
. . . . . . . . . . . . 13
β’ ((Fun
(β D πΉ) β§ π¦ β ((β D πΉ) β (π΄[,]π΅))) β βπ β (π΄[,]π΅)((β D πΉ)βπ) = π¦) |
62 | 10, 61 | mpan 689 |
. . . . . . . . . . . 12
β’ (π¦ β ((β D πΉ) β (π΄[,]π΅)) β βπ β (π΄[,]π΅)((β D πΉ)βπ) = π¦) |
63 | 60, 62 | impel 507 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ βπ₯ β (π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π) β§ π¦ β ((β D πΉ) β (π΄[,]π΅))) β (absβπ¦) β€ π) |
64 | | breq1 5113 |
. . . . . . . . . . 11
β’
((absβπ¦) =
π β ((absβπ¦) β€ π β π β€ π)) |
65 | 63, 64 | syl5ibcom 244 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ βπ₯ β (π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π) β§ π¦ β ((β D πΉ) β (π΄[,]π΅))) β ((absβπ¦) = π β π β€ π)) |
66 | 65 | rexlimdva 3153 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ βπ₯ β (π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π) β (βπ¦ β ((β D πΉ) β (π΄[,]π΅))(absβπ¦) = π β π β€ π)) |
67 | 48, 66 | syl5 34 |
. . . . . . . 8
β’ (((π β§ π β β) β§ βπ₯ β (π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π) β (π β (abs β ((β D πΉ) β (π΄[,]π΅))) β π β€ π)) |
68 | 67 | ralrimiv 3143 |
. . . . . . 7
β’ (((π β§ π β β) β§ βπ₯ β (π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π) β βπ β (abs β ((β D πΉ) β (π΄[,]π΅)))π β€ π) |
69 | 68 | ex 414 |
. . . . . 6
β’ ((π β§ π β β) β (βπ₯ β (π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π β βπ β (abs β ((β D πΉ) β (π΄[,]π΅)))π β€ π)) |
70 | 69 | reximdva 3166 |
. . . . 5
β’ (π β (βπ β β βπ₯ β (π΄[,]π΅)(absβ(((β D πΉ) βΎ (π΄[,]π΅))βπ₯)) β€ π β βπ β β βπ β (abs β ((β D πΉ) β (π΄[,]π΅)))π β€ π)) |
71 | 46, 70 | mpd 15 |
. . . 4
β’ (π β βπ β β βπ β (abs β ((β D πΉ) β (π΄[,]π΅)))π β€ π) |
72 | 7, 39, 71 | suprcld 12125 |
. . 3
β’ (π β sup((abs β ((β
D πΉ) β (π΄[,]π΅))), β, < ) β
β) |
73 | 1, 72 | eqeltrid 2842 |
. 2
β’ (π β πΎ β β) |
74 | | simplrr 777 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β π¦ β (π΄[,]π΅)) |
75 | 74 | fvresd 6867 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((πΉ βΎ (π΄[,]π΅))βπ¦) = (πΉβπ¦)) |
76 | | c1liplem1.cn |
. . . . . . . . . . . . . 14
β’ (π β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) |
77 | | cncff 24272 |
. . . . . . . . . . . . . 14
β’ ((πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ) β (πΉ βΎ (π΄[,]π΅)):(π΄[,]π΅)βΆβ) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (πΉ βΎ (π΄[,]π΅)):(π΄[,]π΅)βΆβ) |
79 | 78 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (πΉ βΎ (π΄[,]π΅)):(π΄[,]π΅)βΆβ) |
80 | 79, 74 | ffvelcdmd 7041 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((πΉ βΎ (π΄[,]π΅))βπ¦) β β) |
81 | 80 | recnd 11190 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((πΉ βΎ (π΄[,]π΅))βπ¦) β β) |
82 | 75, 81 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (πΉβπ¦) β β) |
83 | | simplrl 776 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β π₯ β (π΄[,]π΅)) |
84 | 83 | fvresd 6867 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((πΉ βΎ (π΄[,]π΅))βπ₯) = (πΉβπ₯)) |
85 | 79, 83 | ffvelcdmd 7041 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((πΉ βΎ (π΄[,]π΅))βπ₯) β β) |
86 | 85 | recnd 11190 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((πΉ βΎ (π΄[,]π΅))βπ₯) β β) |
87 | 84, 86 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (πΉβπ₯) β β) |
88 | 82, 87 | subcld 11519 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((πΉβπ¦) β (πΉβπ₯)) β β) |
89 | | iccssre 13353 |
. . . . . . . . . . . . 13
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
90 | 18, 20, 89 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (π΄[,]π΅) β β) |
91 | 90 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (π΄[,]π΅) β β) |
92 | 91, 74 | sseldd 3950 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β π¦ β β) |
93 | 91, 83 | sseldd 3950 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β π₯ β β) |
94 | 92, 93 | resubcld 11590 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (π¦ β π₯) β β) |
95 | 94 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (π¦ β π₯) β β) |
96 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β π₯ < π¦) |
97 | | difrp 12960 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β β) β (π₯ < π¦ β (π¦ β π₯) β
β+)) |
98 | 93, 92, 97 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (π₯ < π¦ β (π¦ β π₯) β
β+)) |
99 | 96, 98 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (π¦ β π₯) β
β+) |
100 | 99 | rpne0d 12969 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (π¦ β π₯) β 0) |
101 | 88, 95, 100 | absdivd 15347 |
. . . . . . 7
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (absβ(((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) = ((absβ((πΉβπ¦) β (πΉβπ₯))) / (absβ(π¦ β π₯)))) |
102 | 6 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (abs β ((β D πΉ) β (π΄[,]π΅))) β β) |
103 | 39 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (abs β ((β D πΉ) β (π΄[,]π΅))) β β
) |
104 | 71 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β βπ β β βπ β (abs β ((β D πΉ) β (π΄[,]π΅)))π β€ π) |
105 | 29 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β Fun abs) |
106 | 88, 95, 100 | divcld 11938 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) β β) |
107 | 106, 34 | eleqtrrdi 2849 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) β dom abs) |
108 | 93 | rexrd 11212 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β π₯ β β*) |
109 | 92 | rexrd 11212 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β π¦ β β*) |
110 | 93, 92, 96 | ltled 11310 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β π₯ β€ π¦) |
111 | | ubicc2 13389 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β*
β§ π¦ β
β* β§ π₯
β€ π¦) β π¦ β (π₯[,]π¦)) |
112 | 108, 109,
110, 111 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β π¦ β (π₯[,]π¦)) |
113 | 112 | fvresd 6867 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((πΉ βΎ (π₯[,]π¦))βπ¦) = (πΉβπ¦)) |
114 | | lbicc2 13388 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β*
β§ π¦ β
β* β§ π₯
β€ π¦) β π₯ β (π₯[,]π¦)) |
115 | 108, 109,
110, 114 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β π₯ β (π₯[,]π¦)) |
116 | 115 | fvresd 6867 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((πΉ βΎ (π₯[,]π¦))βπ₯) = (πΉβπ₯)) |
117 | 113, 116 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (((πΉ βΎ (π₯[,]π¦))βπ¦) β ((πΉ βΎ (π₯[,]π¦))βπ₯)) = ((πΉβπ¦) β (πΉβπ₯))) |
118 | 117 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((((πΉ βΎ (π₯[,]π¦))βπ¦) β ((πΉ βΎ (π₯[,]π¦))βπ₯)) / (π¦ β π₯)) = (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) |
119 | | iccss2 13342 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅)) β (π₯[,]π¦) β (π΄[,]π΅)) |
120 | 119 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (π₯[,]π¦) β (π΄[,]π΅)) |
121 | 120 | resabs1d 5973 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((πΉ βΎ (π΄[,]π΅)) βΎ (π₯[,]π¦)) = (πΉ βΎ (π₯[,]π¦))) |
122 | 76 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ)) |
123 | | rescncf 24276 |
. . . . . . . . . . . . . . 15
β’ ((π₯[,]π¦) β (π΄[,]π΅) β ((πΉ βΎ (π΄[,]π΅)) β ((π΄[,]π΅)βcnββ) β ((πΉ βΎ (π΄[,]π΅)) βΎ (π₯[,]π¦)) β ((π₯[,]π¦)βcnββ))) |
124 | 120, 122,
123 | sylc 65 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((πΉ βΎ (π΄[,]π΅)) βΎ (π₯[,]π¦)) β ((π₯[,]π¦)βcnββ)) |
125 | 121, 124 | eqeltrrd 2839 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (πΉ βΎ (π₯[,]π¦)) β ((π₯[,]π¦)βcnββ)) |
126 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β β β
β) |
127 | | c1liplem1.f |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ β (β βpm
β)) |
128 | 127 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β πΉ β (β βpm
β)) |
129 | | cnex 11139 |
. . . . . . . . . . . . . . . . . . . 20
β’ β
β V |
130 | | reex 11149 |
. . . . . . . . . . . . . . . . . . . 20
β’ β
β V |
131 | 129, 130 | elpm2 8819 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΉ β (β
βpm β) β (πΉ:dom πΉβΆβ β§ dom πΉ β β)) |
132 | 131 | simplbi 499 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β (β
βpm β) β πΉ:dom πΉβΆβ) |
133 | 128, 132 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β πΉ:dom πΉβΆβ) |
134 | 131 | simprbi 498 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β (β
βpm β) β dom πΉ β β) |
135 | 128, 134 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β dom πΉ β β) |
136 | | iccssre 13353 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β§ π¦ β β) β (π₯[,]π¦) β β) |
137 | 93, 92, 136 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (π₯[,]π¦) β β) |
138 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(TopOpenββfld) =
(TopOpenββfld) |
139 | 138 | tgioo2 24182 |
. . . . . . . . . . . . . . . . . 18
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
140 | 138, 139 | dvres 25291 |
. . . . . . . . . . . . . . . . 17
β’
(((β β β β§ πΉ:dom πΉβΆβ) β§ (dom πΉ β β β§ (π₯[,]π¦) β β)) β (β D (πΉ βΎ (π₯[,]π¦))) = ((β D πΉ) βΎ ((intβ(topGenβran
(,)))β(π₯[,]π¦)))) |
141 | 126, 133,
135, 137, 140 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (β D (πΉ βΎ (π₯[,]π¦))) = ((β D πΉ) βΎ ((intβ(topGenβran
(,)))β(π₯[,]π¦)))) |
142 | | iccntr 24200 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β§ π¦ β β) β
((intβ(topGenβran (,)))β(π₯[,]π¦)) = (π₯(,)π¦)) |
143 | 93, 92, 142 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((intβ(topGenβran
(,)))β(π₯[,]π¦)) = (π₯(,)π¦)) |
144 | 143 | reseq2d 5942 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((β D πΉ) βΎ ((intβ(topGenβran
(,)))β(π₯[,]π¦))) = ((β D πΉ) βΎ (π₯(,)π¦))) |
145 | 141, 144 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (β D (πΉ βΎ (π₯[,]π¦))) = ((β D πΉ) βΎ (π₯(,)π¦))) |
146 | 145 | dmeqd 5866 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β dom (β D (πΉ βΎ (π₯[,]π¦))) = dom ((β D πΉ) βΎ (π₯(,)π¦))) |
147 | | ioossicc 13357 |
. . . . . . . . . . . . . . . . 17
β’ (π₯(,)π¦) β (π₯[,]π¦) |
148 | 147, 120 | sstrid 3960 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (π₯(,)π¦) β (π΄[,]π΅)) |
149 | 17 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (π΄[,]π΅) β dom (β D πΉ)) |
150 | 148, 149 | sstrd 3959 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (π₯(,)π¦) β dom (β D πΉ)) |
151 | | ssdmres 5965 |
. . . . . . . . . . . . . . 15
β’ ((π₯(,)π¦) β dom (β D πΉ) β dom ((β D πΉ) βΎ (π₯(,)π¦)) = (π₯(,)π¦)) |
152 | 150, 151 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β dom ((β D πΉ) βΎ (π₯(,)π¦)) = (π₯(,)π¦)) |
153 | 146, 152 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β dom (β D (πΉ βΎ (π₯[,]π¦))) = (π₯(,)π¦)) |
154 | 93, 92, 96, 125, 153 | mvth 25372 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β βπ β (π₯(,)π¦)((β D (πΉ βΎ (π₯[,]π¦)))βπ) = ((((πΉ βΎ (π₯[,]π¦))βπ¦) β ((πΉ βΎ (π₯[,]π¦))βπ₯)) / (π¦ β π₯))) |
155 | 145 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((β D (πΉ βΎ (π₯[,]π¦)))βπ) = (((β D πΉ) βΎ (π₯(,)π¦))βπ)) |
156 | 155 | adantrr 716 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ (π₯ < π¦ β§ π β (π₯(,)π¦))) β ((β D (πΉ βΎ (π₯[,]π¦)))βπ) = (((β D πΉ) βΎ (π₯(,)π¦))βπ)) |
157 | | fvres 6866 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π₯(,)π¦) β (((β D πΉ) βΎ (π₯(,)π¦))βπ) = ((β D πΉ)βπ)) |
158 | 157 | ad2antll 728 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ (π₯ < π¦ β§ π β (π₯(,)π¦))) β (((β D πΉ) βΎ (π₯(,)π¦))βπ) = ((β D πΉ)βπ)) |
159 | 156, 158 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ (π₯ < π¦ β§ π β (π₯(,)π¦))) β ((β D (πΉ βΎ (π₯[,]π¦)))βπ) = ((β D πΉ)βπ)) |
160 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ (π₯ < π¦ β§ π β (π₯(,)π¦))) β Fun (β D πΉ)) |
161 | 17 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ (π₯ < π¦ β§ π β (π₯(,)π¦))) β (π΄[,]π΅) β dom (β D πΉ)) |
162 | 148 | sseld 3948 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (π β (π₯(,)π¦) β π β (π΄[,]π΅))) |
163 | 162 | impr 456 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ (π₯ < π¦ β§ π β (π₯(,)π¦))) β π β (π΄[,]π΅)) |
164 | | funfvima2 7186 |
. . . . . . . . . . . . . . . . . 18
β’ ((Fun
(β D πΉ) β§ (π΄[,]π΅) β dom (β D πΉ)) β (π β (π΄[,]π΅) β ((β D πΉ)βπ) β ((β D πΉ) β (π΄[,]π΅)))) |
165 | 164 | imp 408 |
. . . . . . . . . . . . . . . . 17
β’ (((Fun
(β D πΉ) β§ (π΄[,]π΅) β dom (β D πΉ)) β§ π β (π΄[,]π΅)) β ((β D πΉ)βπ) β ((β D πΉ) β (π΄[,]π΅))) |
166 | 160, 161,
163, 165 | syl21anc 837 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ (π₯ < π¦ β§ π β (π₯(,)π¦))) β ((β D πΉ)βπ) β ((β D πΉ) β (π΄[,]π΅))) |
167 | 159, 166 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ (π₯ < π¦ β§ π β (π₯(,)π¦))) β ((β D (πΉ βΎ (π₯[,]π¦)))βπ) β ((β D πΉ) β (π΄[,]π΅))) |
168 | | eleq1 2826 |
. . . . . . . . . . . . . . 15
β’
(((β D (πΉ
βΎ (π₯[,]π¦)))βπ) = ((((πΉ βΎ (π₯[,]π¦))βπ¦) β ((πΉ βΎ (π₯[,]π¦))βπ₯)) / (π¦ β π₯)) β (((β D (πΉ βΎ (π₯[,]π¦)))βπ) β ((β D πΉ) β (π΄[,]π΅)) β ((((πΉ βΎ (π₯[,]π¦))βπ¦) β ((πΉ βΎ (π₯[,]π¦))βπ₯)) / (π¦ β π₯)) β ((β D πΉ) β (π΄[,]π΅)))) |
169 | 167, 168 | syl5ibcom 244 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ (π₯ < π¦ β§ π β (π₯(,)π¦))) β (((β D (πΉ βΎ (π₯[,]π¦)))βπ) = ((((πΉ βΎ (π₯[,]π¦))βπ¦) β ((πΉ βΎ (π₯[,]π¦))βπ₯)) / (π¦ β π₯)) β ((((πΉ βΎ (π₯[,]π¦))βπ¦) β ((πΉ βΎ (π₯[,]π¦))βπ₯)) / (π¦ β π₯)) β ((β D πΉ) β (π΄[,]π΅)))) |
170 | 169 | expr 458 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (π β (π₯(,)π¦) β (((β D (πΉ βΎ (π₯[,]π¦)))βπ) = ((((πΉ βΎ (π₯[,]π¦))βπ¦) β ((πΉ βΎ (π₯[,]π¦))βπ₯)) / (π¦ β π₯)) β ((((πΉ βΎ (π₯[,]π¦))βπ¦) β ((πΉ βΎ (π₯[,]π¦))βπ₯)) / (π¦ β π₯)) β ((β D πΉ) β (π΄[,]π΅))))) |
171 | 170 | rexlimdv 3151 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (βπ β (π₯(,)π¦)((β D (πΉ βΎ (π₯[,]π¦)))βπ) = ((((πΉ βΎ (π₯[,]π¦))βπ¦) β ((πΉ βΎ (π₯[,]π¦))βπ₯)) / (π¦ β π₯)) β ((((πΉ βΎ (π₯[,]π¦))βπ¦) β ((πΉ βΎ (π₯[,]π¦))βπ₯)) / (π¦ β π₯)) β ((β D πΉ) β (π΄[,]π΅)))) |
172 | 154, 171 | mpd 15 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((((πΉ βΎ (π₯[,]π¦))βπ¦) β ((πΉ βΎ (π₯[,]π¦))βπ₯)) / (π¦ β π₯)) β ((β D πΉ) β (π΄[,]π΅))) |
173 | 118, 172 | eqeltrrd 2839 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) β ((β D πΉ) β (π΄[,]π΅))) |
174 | | funfvima 7185 |
. . . . . . . . . . 11
β’ ((Fun abs
β§ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) β dom abs) β ((((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) β ((β D πΉ) β (π΄[,]π΅)) β (absβ(((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) β (abs β ((β D πΉ) β (π΄[,]π΅))))) |
175 | 174 | imp 408 |
. . . . . . . . . 10
β’ (((Fun
abs β§ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) β dom abs) β§ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) β ((β D πΉ) β (π΄[,]π΅))) β (absβ(((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) β (abs β ((β D πΉ) β (π΄[,]π΅)))) |
176 | 105, 107,
173, 175 | syl21anc 837 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (absβ(((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) β (abs β ((β D πΉ) β (π΄[,]π΅)))) |
177 | 102, 103,
104, 176 | suprubd 12124 |
. . . . . . . 8
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (absβ(((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) β€ sup((abs β ((β D πΉ) β (π΄[,]π΅))), β, < )) |
178 | 177, 1 | breqtrrdi 5152 |
. . . . . . 7
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (absβ(((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) β€ πΎ) |
179 | 101, 178 | eqbrtrrd 5134 |
. . . . . 6
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((absβ((πΉβπ¦) β (πΉβπ₯))) / (absβ(π¦ β π₯))) β€ πΎ) |
180 | 88 | abscld 15328 |
. . . . . . 7
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (absβ((πΉβπ¦) β (πΉβπ₯))) β β) |
181 | 73 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β πΎ β β) |
182 | 95, 100 | absrpcld 15340 |
. . . . . . 7
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (absβ(π¦ β π₯)) β
β+) |
183 | 180, 181,
182 | ledivmuld 13017 |
. . . . . 6
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (((absβ((πΉβπ¦) β (πΉβπ₯))) / (absβ(π¦ β π₯))) β€ πΎ β (absβ((πΉβπ¦) β (πΉβπ₯))) β€ ((absβ(π¦ β π₯)) Β· πΎ))) |
184 | 179, 183 | mpbid 231 |
. . . . 5
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (absβ((πΉβπ¦) β (πΉβπ₯))) β€ ((absβ(π¦ β π₯)) Β· πΎ)) |
185 | 182 | rpcnd 12966 |
. . . . . 6
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (absβ(π¦ β π₯)) β β) |
186 | 181 | recnd 11190 |
. . . . . 6
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β πΎ β β) |
187 | 185, 186 | mulcomd 11183 |
. . . . 5
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β ((absβ(π¦ β π₯)) Β· πΎ) = (πΎ Β· (absβ(π¦ β π₯)))) |
188 | 184, 187 | breqtrd 5136 |
. . . 4
β’ (((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β§ π₯ < π¦) β (absβ((πΉβπ¦) β (πΉβπ₯))) β€ (πΎ Β· (absβ(π¦ β π₯)))) |
189 | 188 | ex 414 |
. . 3
β’ ((π β§ (π₯ β (π΄[,]π΅) β§ π¦ β (π΄[,]π΅))) β (π₯ < π¦ β (absβ((πΉβπ¦) β (πΉβπ₯))) β€ (πΎ Β· (absβ(π¦ β π₯))))) |
190 | 189 | ralrimivva 3198 |
. 2
β’ (π β βπ₯ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(π₯ < π¦ β (absβ((πΉβπ¦) β (πΉβπ₯))) β€ (πΎ Β· (absβ(π¦ β π₯))))) |
191 | 73, 190 | jca 513 |
1
β’ (π β (πΎ β β β§ βπ₯ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(π₯ < π¦ β (absβ((πΉβπ¦) β (πΉβπ₯))) β€ (πΎ Β· (absβ(π¦ β π₯)))))) |