Step | Hyp | Ref
| Expression |
1 | | 0re 11220 |
. . 3
β’ 0 β
β |
2 | | ral0 4507 |
. . . 4
β’
βπ¦ β
β
(absβ(πΉβπ¦)) β€ 0 |
3 | | simp1 1133 |
. . . . . . . 8
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β π΄ β β) |
4 | 3 | rexrd 11268 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β π΄ β
β*) |
5 | | simp2 1134 |
. . . . . . . 8
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β π΅ β β) |
6 | 5 | rexrd 11268 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β π΅ β
β*) |
7 | | icc0 13378 |
. . . . . . 7
β’ ((π΄ β β*
β§ π΅ β
β*) β ((π΄[,]π΅) = β
β π΅ < π΄)) |
8 | 4, 6, 7 | syl2anc 583 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β ((π΄[,]π΅) = β
β π΅ < π΄)) |
9 | 8 | biimpar 477 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΅ < π΄) β (π΄[,]π΅) = β
) |
10 | 9 | raleqdv 3319 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΅ < π΄) β (βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ 0 β βπ¦ β β
(absβ(πΉβπ¦)) β€ 0)) |
11 | 2, 10 | mpbiri 258 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΅ < π΄) β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ 0) |
12 | | brralrspcev 5201 |
. . 3
β’ ((0
β β β§ βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ 0) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯) |
13 | 1, 11, 12 | sylancr 586 |
. 2
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΅ < π΄) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯) |
14 | 3 | adantr 480 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β π΄ β β) |
15 | 5 | adantr 480 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β π΅ β β) |
16 | | simpr 484 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β π΄ β€ π΅) |
17 | | simp3 1135 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β πΉ β ((π΄[,]π΅)βcnββ)) |
18 | | abscncf 24776 |
. . . . . . . 8
β’ abs
β (ββcnββ) |
19 | 18 | a1i 11 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β abs β (ββcnββ)) |
20 | 17, 19 | cncfco 24782 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β (abs β πΉ) β ((π΄[,]π΅)βcnββ)) |
21 | 20 | adantr 480 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β (abs β πΉ) β ((π΄[,]π΅)βcnββ)) |
22 | 14, 15, 16, 21 | evthicc 25343 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β (βπ§ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§) β§ βπ§ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ§) β€ ((abs β πΉ)βπ¦))) |
23 | 22 | simpld 494 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β βπ§ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§)) |
24 | | cncff 24768 |
. . . . . . . 8
β’ ((abs
β πΉ) β ((π΄[,]π΅)βcnββ) β (abs β πΉ):(π΄[,]π΅)βΆβ) |
25 | 20, 24 | syl 17 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β (abs β πΉ):(π΄[,]π΅)βΆβ) |
26 | 25 | ffvelcdmda 7080 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β ((abs β πΉ)βπ§) β β) |
27 | | cncff 24768 |
. . . . . . . . . . . 12
β’ (πΉ β ((π΄[,]π΅)βcnββ) β πΉ:(π΄[,]π΅)βΆβ) |
28 | 17, 27 | syl 17 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β πΉ:(π΄[,]π΅)βΆβ) |
29 | 28 | adantr 480 |
. . . . . . . . . 10
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β πΉ:(π΄[,]π΅)βΆβ) |
30 | | fvco3 6984 |
. . . . . . . . . 10
β’ ((πΉ:(π΄[,]π΅)βΆβ β§ π¦ β (π΄[,]π΅)) β ((abs β πΉ)βπ¦) = (absβ(πΉβπ¦))) |
31 | 29, 30 | sylan 579 |
. . . . . . . . 9
β’ ((((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β§ π¦ β (π΄[,]π΅)) β ((abs β πΉ)βπ¦) = (absβ(πΉβπ¦))) |
32 | 31 | breq1d 5151 |
. . . . . . . 8
β’ ((((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β§ π¦ β (π΄[,]π΅)) β (((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§) β (absβ(πΉβπ¦)) β€ ((abs β πΉ)βπ§))) |
33 | 32 | ralbidva 3169 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β (βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§) β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ ((abs β πΉ)βπ§))) |
34 | 33 | biimpd 228 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β (βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§) β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ ((abs β πΉ)βπ§))) |
35 | | brralrspcev 5201 |
. . . . . 6
β’ ((((abs
β πΉ)βπ§) β β β§
βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ ((abs β πΉ)βπ§)) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯) |
36 | 26, 34, 35 | syl6an 681 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β (βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯)) |
37 | 36 | rexlimdva 3149 |
. . . 4
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β (βπ§ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯)) |
38 | 37 | imp 406 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ βπ§ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§)) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯) |
39 | 23, 38 | syldan 590 |
. 2
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯) |
40 | 13, 39, 5, 3 | ltlecasei 11326 |
1
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯) |