Step | Hyp | Ref
| Expression |
1 | | imaco 6207 |
. . 3
β’ ((abs
β πΉ) β β)
= (abs β (πΉ β
β)) |
2 | | imassrn 6028 |
. . . 4
β’ ((abs
β πΉ) β β)
β ran (abs β πΉ) |
3 | | imo72b2lem1.1 |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
4 | | absf 15231 |
. . . . . . . 8
β’
abs:ββΆβ |
5 | 4 | a1i 11 |
. . . . . . 7
β’ (π β
abs:ββΆβ) |
6 | | ax-resscn 11116 |
. . . . . . . 8
β’ β
β β |
7 | 6 | a1i 11 |
. . . . . . 7
β’ (π β β β
β) |
8 | 5, 7 | fssresd 6713 |
. . . . . 6
β’ (π β (abs βΎ
β):ββΆβ) |
9 | 3, 8 | fco2d 42527 |
. . . . 5
β’ (π β (abs β πΉ):ββΆβ) |
10 | 9 | frnd 6680 |
. . . 4
β’ (π β ran (abs β πΉ) β
β) |
11 | 2, 10 | sstrid 3959 |
. . 3
β’ (π β ((abs β πΉ) β β) β
β) |
12 | 1, 11 | eqsstrrid 3997 |
. 2
β’ (π β (abs β (πΉ β β)) β
β) |
13 | | 0re 11165 |
. . . . . 6
β’ 0 β
β |
14 | 13 | ne0ii 4301 |
. . . . 5
β’ β
β β
|
15 | 14 | a1i 11 |
. . . 4
β’ (π β β β
β
) |
16 | 15, 9 | wnefimgd 42526 |
. . 3
β’ (π β ((abs β πΉ) β β) β
β
) |
17 | 1, 16 | eqnetrrid 3016 |
. 2
β’ (π β (abs β (πΉ β β)) β
β
) |
18 | | 1red 11164 |
. . 3
β’ (π β 1 β
β) |
19 | | simpr 486 |
. . . . 5
β’ ((π β§ π = 1) β π = 1) |
20 | 19 | breq2d 5121 |
. . . 4
β’ ((π β§ π = 1) β (π‘ β€ π β π‘ β€ 1)) |
21 | 20 | ralbidv 3171 |
. . 3
β’ ((π β§ π = 1) β (βπ‘ β (abs β (πΉ β β))π‘ β€ π β βπ‘ β (abs β (πΉ β β))π‘ β€ 1)) |
22 | | imo72b2lem1.6 |
. . . 4
β’ (π β βπ¦ β β (absβ(πΉβπ¦)) β€ 1) |
23 | 3, 22 | extoimad 42529 |
. . 3
β’ (π β βπ‘ β (abs β (πΉ β β))π‘ β€ 1) |
24 | 18, 21, 23 | rspcedvd 3585 |
. 2
β’ (π β βπ β β βπ‘ β (abs β (πΉ β β))π‘ β€ π) |
25 | | 0red 11166 |
. 2
β’ (π β 0 β
β) |
26 | | imo72b2lem1.7 |
. . 3
β’ (π β βπ₯ β β (πΉβπ₯) β 0) |
27 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β πΉ:ββΆβ) |
28 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β π₯ β β) |
29 | 27, 28 | fvco3d 6945 |
. . . . 5
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β ((abs β πΉ)βπ₯) = (absβ(πΉβπ₯))) |
30 | 9 | funfvima2d 7186 |
. . . . . . 7
β’ ((π β§ π₯ β β) β ((abs β πΉ)βπ₯) β ((abs β πΉ) β β)) |
31 | 30 | adantrr 716 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β ((abs β πΉ)βπ₯) β ((abs β πΉ) β β)) |
32 | 31, 1 | eleqtrdi 2844 |
. . . . 5
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β ((abs β πΉ)βπ₯) β (abs β (πΉ β β))) |
33 | 29, 32 | eqeltrrd 2835 |
. . . 4
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β (absβ(πΉβπ₯)) β (abs β (πΉ β β))) |
34 | | simpr 486 |
. . . . 5
β’ (((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β§ π§ = (absβ(πΉβπ₯))) β π§ = (absβ(πΉβπ₯))) |
35 | 34 | breq2d 5121 |
. . . 4
β’ (((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β§ π§ = (absβ(πΉβπ₯))) β (0 < π§ β 0 < (absβ(πΉβπ₯)))) |
36 | 3 | ffvelcdmda 7039 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (πΉβπ₯) β β) |
37 | 36 | adantrr 716 |
. . . . . . 7
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β (πΉβπ₯) β β) |
38 | 37 | recnd 11191 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β (πΉβπ₯) β β) |
39 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β (πΉβπ₯) β 0) |
40 | 38, 39 | absrpcld 15342 |
. . . . 5
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β (absβ(πΉβπ₯)) β
β+) |
41 | 40 | rpgt0d 12968 |
. . . 4
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β 0 < (absβ(πΉβπ₯))) |
42 | 33, 35, 41 | rspcedvd 3585 |
. . 3
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β βπ§ β (abs β (πΉ β β))0 < π§) |
43 | 26, 42 | rexlimddv 3155 |
. 2
β’ (π β βπ§ β (abs β (πΉ β β))0 < π§) |
44 | 12, 17, 24, 25, 43 | suprlubrd 42533 |
1
β’ (π β 0 < sup((abs β
(πΉ β β)),
β, < )) |