Step | Hyp | Ref
| Expression |
1 | | 0re 11212 |
. . 3
β’ 0 β
β |
2 | | ral0 4511 |
. . . 4
β’
βπ¦ β
β
(absβ(πΉβπ¦)) β€ 0 |
3 | | simp1 1136 |
. . . . . . . 8
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β π΄ β β) |
4 | 3 | rexrd 11260 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β π΄ β
β*) |
5 | | simp2 1137 |
. . . . . . . 8
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β π΅ β β) |
6 | 5 | rexrd 11260 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β π΅ β
β*) |
7 | | icc0 13368 |
. . . . . . 7
β’ ((π΄ β β*
β§ π΅ β
β*) β ((π΄[,]π΅) = β
β π΅ < π΄)) |
8 | 4, 6, 7 | syl2anc 584 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β ((π΄[,]π΅) = β
β π΅ < π΄)) |
9 | 8 | biimpar 478 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΅ < π΄) β (π΄[,]π΅) = β
) |
10 | 9 | raleqdv 3325 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΅ < π΄) β (βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ 0 β βπ¦ β β
(absβ(πΉβπ¦)) β€ 0)) |
11 | 2, 10 | mpbiri 257 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΅ < π΄) β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ 0) |
12 | | brralrspcev 5207 |
. . 3
β’ ((0
β β β§ βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ 0) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯) |
13 | 1, 11, 12 | sylancr 587 |
. 2
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΅ < π΄) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯) |
14 | 3 | adantr 481 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β π΄ β β) |
15 | 5 | adantr 481 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β π΅ β β) |
16 | | simpr 485 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β π΄ β€ π΅) |
17 | | simp3 1138 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β πΉ β ((π΄[,]π΅)βcnββ)) |
18 | | abscncf 24408 |
. . . . . . . 8
β’ abs
β (ββcnββ) |
19 | 18 | a1i 11 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β abs β (ββcnββ)) |
20 | 17, 19 | cncfco 24414 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β (abs β πΉ) β ((π΄[,]π΅)βcnββ)) |
21 | 20 | adantr 481 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β (abs β πΉ) β ((π΄[,]π΅)βcnββ)) |
22 | 14, 15, 16, 21 | evthicc 24967 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β (βπ§ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§) β§ βπ§ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ§) β€ ((abs β πΉ)βπ¦))) |
23 | 22 | simpld 495 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β βπ§ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§)) |
24 | | cncff 24400 |
. . . . . . . 8
β’ ((abs
β πΉ) β ((π΄[,]π΅)βcnββ) β (abs β πΉ):(π΄[,]π΅)βΆβ) |
25 | 20, 24 | syl 17 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β (abs β πΉ):(π΄[,]π΅)βΆβ) |
26 | 25 | ffvelcdmda 7083 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β ((abs β πΉ)βπ§) β β) |
27 | | cncff 24400 |
. . . . . . . . . . . 12
β’ (πΉ β ((π΄[,]π΅)βcnββ) β πΉ:(π΄[,]π΅)βΆβ) |
28 | 17, 27 | syl 17 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β πΉ:(π΄[,]π΅)βΆβ) |
29 | 28 | adantr 481 |
. . . . . . . . . 10
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β πΉ:(π΄[,]π΅)βΆβ) |
30 | | fvco3 6987 |
. . . . . . . . . 10
β’ ((πΉ:(π΄[,]π΅)βΆβ β§ π¦ β (π΄[,]π΅)) β ((abs β πΉ)βπ¦) = (absβ(πΉβπ¦))) |
31 | 29, 30 | sylan 580 |
. . . . . . . . 9
β’ ((((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β§ π¦ β (π΄[,]π΅)) β ((abs β πΉ)βπ¦) = (absβ(πΉβπ¦))) |
32 | 31 | breq1d 5157 |
. . . . . . . 8
β’ ((((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β§ π¦ β (π΄[,]π΅)) β (((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§) β (absβ(πΉβπ¦)) β€ ((abs β πΉ)βπ§))) |
33 | 32 | ralbidva 3175 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β (βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§) β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ ((abs β πΉ)βπ§))) |
34 | 33 | biimpd 228 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β (βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§) β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ ((abs β πΉ)βπ§))) |
35 | | brralrspcev 5207 |
. . . . . 6
β’ ((((abs
β πΉ)βπ§) β β β§
βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ ((abs β πΉ)βπ§)) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯) |
36 | 26, 34, 35 | syl6an 682 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π§ β (π΄[,]π΅)) β (βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯)) |
37 | 36 | rexlimdva 3155 |
. . . 4
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β (βπ§ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯)) |
38 | 37 | imp 407 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ βπ§ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)((abs β πΉ)βπ¦) β€ ((abs β πΉ)βπ§)) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯) |
39 | 23, 38 | syldan 591 |
. 2
β’ (((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β§ π΄ β€ π΅) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯) |
40 | 13, 39, 5, 3 | ltlecasei 11318 |
1
β’ ((π΄ β β β§ π΅ β β β§ πΉ β ((π΄[,]π΅)βcnββ)) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ π₯) |