Step | Hyp | Ref
| Expression |
1 | | dvbdfbdioo.f |
. . . . . . . 8
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
2 | | dvbdfbdioo.a |
. . . . . . . . . 10
β’ (π β π΄ β β) |
3 | 2 | rexrd 11264 |
. . . . . . . . 9
β’ (π β π΄ β
β*) |
4 | | dvbdfbdioo.b |
. . . . . . . . . 10
β’ (π β π΅ β β) |
5 | 4 | rexrd 11264 |
. . . . . . . . 9
β’ (π β π΅ β
β*) |
6 | 2, 4 | readdcld 11243 |
. . . . . . . . . 10
β’ (π β (π΄ + π΅) β β) |
7 | 6 | rehalfcld 12459 |
. . . . . . . . 9
β’ (π β ((π΄ + π΅) / 2) β β) |
8 | | dvbdfbdioo.altb |
. . . . . . . . . 10
β’ (π β π΄ < π΅) |
9 | | avglt1 12450 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β π΄ < ((π΄ + π΅) / 2))) |
10 | 2, 4, 9 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (π΄ < π΅ β π΄ < ((π΄ + π΅) / 2))) |
11 | 8, 10 | mpbid 231 |
. . . . . . . . 9
β’ (π β π΄ < ((π΄ + π΅) / 2)) |
12 | | avglt2 12451 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β ((π΄ + π΅) / 2) < π΅)) |
13 | 2, 4, 12 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (π΄ < π΅ β ((π΄ + π΅) / 2) < π΅)) |
14 | 8, 13 | mpbid 231 |
. . . . . . . . 9
β’ (π β ((π΄ + π΅) / 2) < π΅) |
15 | 3, 5, 7, 11, 14 | eliood 44211 |
. . . . . . . 8
β’ (π β ((π΄ + π΅) / 2) β (π΄(,)π΅)) |
16 | 1, 15 | ffvelcdmd 7088 |
. . . . . . 7
β’ (π β (πΉβ((π΄ + π΅) / 2)) β β) |
17 | 16 | recnd 11242 |
. . . . . 6
β’ (π β (πΉβ((π΄ + π΅) / 2)) β β) |
18 | 17 | abscld 15383 |
. . . . 5
β’ (π β (absβ(πΉβ((π΄ + π΅) / 2))) β β) |
19 | 18 | ad2antrr 725 |
. . . 4
β’ (((π β§ π β β) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β (absβ(πΉβ((π΄ + π΅) / 2))) β β) |
20 | | simplr 768 |
. . . . 5
β’ (((π β§ π β β) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β π β β) |
21 | 4 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β π΅ β β) |
22 | 2 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β π΄ β β) |
23 | 21, 22 | resubcld 11642 |
. . . . 5
β’ (((π β§ π β β) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β (π΅ β π΄) β β) |
24 | 20, 23 | remulcld 11244 |
. . . 4
β’ (((π β§ π β β) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β (π Β· (π΅ β π΄)) β β) |
25 | 19, 24 | readdcld 11243 |
. . 3
β’ (((π β§ π β β) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β ((absβ(πΉβ((π΄ + π΅) / 2))) + (π Β· (π΅ β π΄))) β β) |
26 | 8 | ad2antrr 725 |
. . . 4
β’ (((π β§ π β β) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β π΄ < π΅) |
27 | 1 | ad2antrr 725 |
. . . 4
β’ (((π β§ π β β) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β πΉ:(π΄(,)π΅)βΆβ) |
28 | | dvbdfbdioo.dmdv |
. . . . 5
β’ (π β dom (β D πΉ) = (π΄(,)π΅)) |
29 | 28 | ad2antrr 725 |
. . . 4
β’ (((π β§ π β β) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β dom (β D πΉ) = (π΄(,)π΅)) |
30 | | 2fveq3 6897 |
. . . . . . . 8
β’ (π₯ = π¦ β (absβ((β D πΉ)βπ₯)) = (absβ((β D πΉ)βπ¦))) |
31 | 30 | breq1d 5159 |
. . . . . . 7
β’ (π₯ = π¦ β ((absβ((β D πΉ)βπ₯)) β€ π β (absβ((β D πΉ)βπ¦)) β€ π)) |
32 | 31 | cbvralvw 3235 |
. . . . . 6
β’
(βπ₯ β
(π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π β βπ¦ β (π΄(,)π΅)(absβ((β D πΉ)βπ¦)) β€ π) |
33 | 32 | biimpi 215 |
. . . . 5
β’
(βπ₯ β
(π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π β βπ¦ β (π΄(,)π΅)(absβ((β D πΉ)βπ¦)) β€ π) |
34 | 33 | adantl 483 |
. . . 4
β’ (((π β§ π β β) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β βπ¦ β (π΄(,)π΅)(absβ((β D πΉ)βπ¦)) β€ π) |
35 | | eqid 2733 |
. . . 4
β’
((absβ(πΉβ((π΄ + π΅) / 2))) + (π Β· (π΅ β π΄))) = ((absβ(πΉβ((π΄ + π΅) / 2))) + (π Β· (π΅ β π΄))) |
36 | 22, 21, 26, 27, 29, 20, 34, 35 | dvbdfbdioolem2 44645 |
. . 3
β’ (((π β§ π β β) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β βπ¦ β (π΄(,)π΅)(absβ(πΉβπ¦)) β€ ((absβ(πΉβ((π΄ + π΅) / 2))) + (π Β· (π΅ β π΄)))) |
37 | | 2fveq3 6897 |
. . . . . . 7
β’ (π₯ = π¦ β (absβ(πΉβπ₯)) = (absβ(πΉβπ¦))) |
38 | 37 | breq1d 5159 |
. . . . . 6
β’ (π₯ = π¦ β ((absβ(πΉβπ₯)) β€ π β (absβ(πΉβπ¦)) β€ π)) |
39 | 38 | cbvralvw 3235 |
. . . . 5
β’
(βπ₯ β
(π΄(,)π΅)(absβ(πΉβπ₯)) β€ π β βπ¦ β (π΄(,)π΅)(absβ(πΉβπ¦)) β€ π) |
40 | | breq2 5153 |
. . . . . 6
β’ (π = ((absβ(πΉβ((π΄ + π΅) / 2))) + (π Β· (π΅ β π΄))) β ((absβ(πΉβπ¦)) β€ π β (absβ(πΉβπ¦)) β€ ((absβ(πΉβ((π΄ + π΅) / 2))) + (π Β· (π΅ β π΄))))) |
41 | 40 | ralbidv 3178 |
. . . . 5
β’ (π = ((absβ(πΉβ((π΄ + π΅) / 2))) + (π Β· (π΅ β π΄))) β (βπ¦ β (π΄(,)π΅)(absβ(πΉβπ¦)) β€ π β βπ¦ β (π΄(,)π΅)(absβ(πΉβπ¦)) β€ ((absβ(πΉβ((π΄ + π΅) / 2))) + (π Β· (π΅ β π΄))))) |
42 | 39, 41 | bitrid 283 |
. . . 4
β’ (π = ((absβ(πΉβ((π΄ + π΅) / 2))) + (π Β· (π΅ β π΄))) β (βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π β βπ¦ β (π΄(,)π΅)(absβ(πΉβπ¦)) β€ ((absβ(πΉβ((π΄ + π΅) / 2))) + (π Β· (π΅ β π΄))))) |
43 | 42 | rspcev 3613 |
. . 3
β’
((((absβ(πΉβ((π΄ + π΅) / 2))) + (π Β· (π΅ β π΄))) β β β§ βπ¦ β (π΄(,)π΅)(absβ(πΉβπ¦)) β€ ((absβ(πΉβ((π΄ + π΅) / 2))) + (π Β· (π΅ β π΄)))) β βπ β β βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) |
44 | 25, 36, 43 | syl2anc 585 |
. 2
β’ (((π β§ π β β) β§ βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) β βπ β β βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) |
45 | | dvbdfbdioo.dvbd |
. 2
β’ (π β βπ β β βπ₯ β (π΄(,)π΅)(absβ((β D πΉ)βπ₯)) β€ π) |
46 | 44, 45 | r19.29a 3163 |
1
β’ (π β βπ β β βπ₯ β (π΄(,)π΅)(absβ(πΉβπ₯)) β€ π) |