Step | Hyp | Ref
| Expression |
1 | | imaco 6244 |
. . 3
β’ ((abs
β πΉ) β β)
= (abs β (πΉ β
β)) |
2 | | imassrn 6064 |
. . . 4
β’ ((abs
β πΉ) β β)
β ran (abs β πΉ) |
3 | | imo72b2lem1.1 |
. . . . . 6
β’ (π β πΉ:ββΆβ) |
4 | | absf 15290 |
. . . . . . . 8
β’
abs:ββΆβ |
5 | 4 | a1i 11 |
. . . . . . 7
β’ (π β
abs:ββΆβ) |
6 | | ax-resscn 11169 |
. . . . . . . 8
β’ β
β β |
7 | 6 | a1i 11 |
. . . . . . 7
β’ (π β β β
β) |
8 | 5, 7 | fssresd 6752 |
. . . . . 6
β’ (π β (abs βΎ
β):ββΆβ) |
9 | 3, 8 | fco2d 43495 |
. . . . 5
β’ (π β (abs β πΉ):ββΆβ) |
10 | 9 | frnd 6719 |
. . . 4
β’ (π β ran (abs β πΉ) β
β) |
11 | 2, 10 | sstrid 3988 |
. . 3
β’ (π β ((abs β πΉ) β β) β
β) |
12 | 1, 11 | eqsstrrid 4026 |
. 2
β’ (π β (abs β (πΉ β β)) β
β) |
13 | | 0re 11220 |
. . . . . 6
β’ 0 β
β |
14 | 13 | ne0ii 4332 |
. . . . 5
β’ β
β β
|
15 | 14 | a1i 11 |
. . . 4
β’ (π β β β
β
) |
16 | 15, 9 | wnefimgd 43494 |
. . 3
β’ (π β ((abs β πΉ) β β) β
β
) |
17 | 1, 16 | eqnetrrid 3010 |
. 2
β’ (π β (abs β (πΉ β β)) β
β
) |
18 | | 1red 11219 |
. . 3
β’ (π β 1 β
β) |
19 | | simpr 484 |
. . . . 5
β’ ((π β§ π = 1) β π = 1) |
20 | 19 | breq2d 5153 |
. . . 4
β’ ((π β§ π = 1) β (π‘ β€ π β π‘ β€ 1)) |
21 | 20 | ralbidv 3171 |
. . 3
β’ ((π β§ π = 1) β (βπ‘ β (abs β (πΉ β β))π‘ β€ π β βπ‘ β (abs β (πΉ β β))π‘ β€ 1)) |
22 | | imo72b2lem1.6 |
. . . 4
β’ (π β βπ¦ β β (absβ(πΉβπ¦)) β€ 1) |
23 | 3, 22 | extoimad 43497 |
. . 3
β’ (π β βπ‘ β (abs β (πΉ β β))π‘ β€ 1) |
24 | 18, 21, 23 | rspcedvd 3608 |
. 2
β’ (π β βπ β β βπ‘ β (abs β (πΉ β β))π‘ β€ π) |
25 | | 0red 11221 |
. 2
β’ (π β 0 β
β) |
26 | | imo72b2lem1.7 |
. . 3
β’ (π β βπ₯ β β (πΉβπ₯) β 0) |
27 | 3 | adantr 480 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β πΉ:ββΆβ) |
28 | | simprl 768 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β π₯ β β) |
29 | 27, 28 | fvco3d 6985 |
. . . . 5
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β ((abs β πΉ)βπ₯) = (absβ(πΉβπ₯))) |
30 | 9 | funfvima2d 7229 |
. . . . . . 7
β’ ((π β§ π₯ β β) β ((abs β πΉ)βπ₯) β ((abs β πΉ) β β)) |
31 | 30 | adantrr 714 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β ((abs β πΉ)βπ₯) β ((abs β πΉ) β β)) |
32 | 31, 1 | eleqtrdi 2837 |
. . . . 5
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β ((abs β πΉ)βπ₯) β (abs β (πΉ β β))) |
33 | 29, 32 | eqeltrrd 2828 |
. . . 4
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β (absβ(πΉβπ₯)) β (abs β (πΉ β β))) |
34 | | simpr 484 |
. . . . 5
β’ (((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β§ π§ = (absβ(πΉβπ₯))) β π§ = (absβ(πΉβπ₯))) |
35 | 34 | breq2d 5153 |
. . . 4
β’ (((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β§ π§ = (absβ(πΉβπ₯))) β (0 < π§ β 0 < (absβ(πΉβπ₯)))) |
36 | 3 | ffvelcdmda 7080 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (πΉβπ₯) β β) |
37 | 36 | adantrr 714 |
. . . . . . 7
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β (πΉβπ₯) β β) |
38 | 37 | recnd 11246 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β (πΉβπ₯) β β) |
39 | | simprr 770 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β (πΉβπ₯) β 0) |
40 | 38, 39 | absrpcld 15401 |
. . . . 5
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β (absβ(πΉβπ₯)) β
β+) |
41 | 40 | rpgt0d 13025 |
. . . 4
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β 0 < (absβ(πΉβπ₯))) |
42 | 33, 35, 41 | rspcedvd 3608 |
. . 3
β’ ((π β§ (π₯ β β β§ (πΉβπ₯) β 0)) β βπ§ β (abs β (πΉ β β))0 < π§) |
43 | 26, 42 | rexlimddv 3155 |
. 2
β’ (π β βπ§ β (abs β (πΉ β β))0 < π§) |
44 | 12, 17, 24, 25, 43 | suprlubrd 43501 |
1
β’ (π β 0 < sup((abs β
(πΉ β β)),
β, < )) |