Step | Hyp | Ref
| Expression |
1 | | 3anass 1096 |
. . 3
β’ ((πΉ β (β
βpm β) β§ π β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯)) β (πΉ β (β βpm
β) β§ (π β
β β§ βπ₯
β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯)))) |
2 | | lmclim.3 |
. . . . . . . . . . 11
β’ π =
(β€β₯βπ) |
3 | 2 | uztrn2 12790 |
. . . . . . . . . 10
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
4 | | 3anass 1096 |
. . . . . . . . . . 11
β’ ((π β dom πΉ β§ (πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯) β (π β dom πΉ β§ ((πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯))) |
5 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ (((π β β€ β§ π β dom πΉ) β§ π β β) β π β dom πΉ) |
6 | 5 | sselda 3948 |
. . . . . . . . . . . . 13
β’ ((((π β β€ β§ π β dom πΉ) β§ π β β) β§ π β π) β π β dom πΉ) |
7 | 6 | biantrurd 534 |
. . . . . . . . . . . 12
β’ ((((π β β€ β§ π β dom πΉ) β§ π β β) β§ π β π) β (((πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯) β (π β dom πΉ β§ ((πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯)))) |
8 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ (abs
β β ) = (abs β β ) |
9 | 8 | cnmetdval 24157 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ) β β β§ π β β) β ((πΉβπ)(abs β β )π) = (absβ((πΉβπ) β π))) |
10 | 9 | ancoms 460 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ (πΉβπ) β β) β ((πΉβπ)(abs β β )π) = (absβ((πΉβπ) β π))) |
11 | 10 | breq1d 5119 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (πΉβπ) β β) β (((πΉβπ)(abs β β )π) < π₯ β (absβ((πΉβπ) β π)) < π₯)) |
12 | 11 | pm5.32da 580 |
. . . . . . . . . . . . 13
β’ (π β β β (((πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯))) |
13 | 12 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ ((((π β β€ β§ π β dom πΉ) β§ π β β) β§ π β π) β (((πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯))) |
14 | 7, 13 | bitr3d 281 |
. . . . . . . . . . 11
β’ ((((π β β€ β§ π β dom πΉ) β§ π β β) β§ π β π) β ((π β dom πΉ β§ ((πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯)) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯))) |
15 | 4, 14 | bitrid 283 |
. . . . . . . . . 10
β’ ((((π β β€ β§ π β dom πΉ) β§ π β β) β§ π β π) β ((π β dom πΉ β§ (πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯))) |
16 | 3, 15 | sylan2 594 |
. . . . . . . . 9
β’ ((((π β β€ β§ π β dom πΉ) β§ π β β) β§ (π β π β§ π β (β€β₯βπ))) β ((π β dom πΉ β§ (πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯))) |
17 | 16 | anassrs 469 |
. . . . . . . 8
β’
(((((π β
β€ β§ π β dom
πΉ) β§ π β β) β§ π β π) β§ π β (β€β₯βπ)) β ((π β dom πΉ β§ (πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯))) |
18 | 17 | ralbidva 3169 |
. . . . . . 7
β’ ((((π β β€ β§ π β dom πΉ) β§ π β β) β§ π β π) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯) β βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯))) |
19 | 18 | rexbidva 3170 |
. . . . . 6
β’ (((π β β€ β§ π β dom πΉ) β§ π β β) β (βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯) β βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯))) |
20 | 19 | ralbidv 3171 |
. . . . 5
β’ (((π β β€ β§ π β dom πΉ) β§ π β β) β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯))) |
21 | 20 | pm5.32da 580 |
. . . 4
β’ ((π β β€ β§ π β dom πΉ) β ((π β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯)) β (π β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯)))) |
22 | 21 | anbi2d 630 |
. . 3
β’ ((π β β€ β§ π β dom πΉ) β ((πΉ β (β βpm
β) β§ (π β
β β§ βπ₯
β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯))) β (πΉ β (β βpm
β) β§ (π β
β β§ βπ₯
β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯))))) |
23 | 1, 22 | bitrid 283 |
. 2
β’ ((π β β€ β§ π β dom πΉ) β ((πΉ β (β βpm
β) β§ π β
β β§ βπ₯
β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯)) β (πΉ β (β βpm
β) β§ (π β
β β§ βπ₯
β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯))))) |
24 | | lmclim.2 |
. . . 4
β’ π½ =
(TopOpenββfld) |
25 | 24 | cnfldtopn 24168 |
. . 3
β’ π½ = (MetOpenβ(abs β
β )) |
26 | | cnxmet 24159 |
. . . 4
β’ (abs
β β ) β (βMetββ) |
27 | 26 | a1i 11 |
. . 3
β’ ((π β β€ β§ π β dom πΉ) β (abs β β ) β
(βMetββ)) |
28 | | simpl 484 |
. . 3
β’ ((π β β€ β§ π β dom πΉ) β π β β€) |
29 | 25, 27, 2, 28 | lmmbr3 24647 |
. 2
β’ ((π β β€ β§ π β dom πΉ) β (πΉ(βπ‘βπ½)π β (πΉ β (β βpm
β) β§ π β
β β§ βπ₯
β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β β β§ ((πΉβπ)(abs β β )π) < π₯)))) |
30 | | simpll 766 |
. . . 4
β’ (((π β β€ β§ π β dom πΉ) β§ πΉ β (β βpm
β)) β π β
β€) |
31 | | simpr 486 |
. . . 4
β’ (((π β β€ β§ π β dom πΉ) β§ πΉ β (β βpm
β)) β πΉ β
(β βpm β)) |
32 | | eqidd 2734 |
. . . 4
β’ ((((π β β€ β§ π β dom πΉ) β§ πΉ β (β βpm
β)) β§ π β
π) β (πΉβπ) = (πΉβπ)) |
33 | 2, 30, 31, 32 | clim2 15395 |
. . 3
β’ (((π β β€ β§ π β dom πΉ) β§ πΉ β (β βpm
β)) β (πΉ β
π β (π β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯)))) |
34 | 33 | pm5.32da 580 |
. 2
β’ ((π β β€ β§ π β dom πΉ) β ((πΉ β (β βpm
β) β§ πΉ β
π) β (πΉ β (β
βpm β) β§ (π β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π)) < π₯))))) |
35 | 23, 29, 34 | 3bitr4d 311 |
1
β’ ((π β β€ β§ π β dom πΉ) β (πΉ(βπ‘βπ½)π β (πΉ β (β βpm
β) β§ πΉ β
π))) |