Step | Hyp | Ref
| Expression |
1 | | lmmbr.3 |
. . . 4
β’ (π β π· β (βMetβπ)) |
2 | | lmmbrf.8 |
. . . 4
β’ (π β πΉ:πβΆπ) |
3 | | elfvdm 6883 |
. . . . . 6
β’ (π· β (βMetβπ) β π β dom βMet) |
4 | | cnex 11140 |
. . . . . 6
β’ β
β V |
5 | 3, 4 | jctir 522 |
. . . . 5
β’ (π· β (βMetβπ) β (π β dom βMet β§ β β
V)) |
6 | | lmmbr3.5 |
. . . . . . 7
β’ π =
(β€β₯βπ) |
7 | | uzssz 12792 |
. . . . . . . 8
β’
(β€β₯βπ) β β€ |
8 | | zsscn 12515 |
. . . . . . . 8
β’ β€
β β |
9 | 7, 8 | sstri 3957 |
. . . . . . 7
β’
(β€β₯βπ) β β |
10 | 6, 9 | eqsstri 3982 |
. . . . . 6
β’ π β
β |
11 | 10 | jctr 526 |
. . . . 5
β’ (πΉ:πβΆπ β (πΉ:πβΆπ β§ π β β)) |
12 | | elpm2r 8789 |
. . . . 5
β’ (((π β dom βMet β§
β β V) β§ (πΉ:πβΆπ β§ π β β)) β πΉ β (π βpm
β)) |
13 | 5, 11, 12 | syl2an 597 |
. . . 4
β’ ((π· β (βMetβπ) β§ πΉ:πβΆπ) β πΉ β (π βpm
β)) |
14 | 1, 2, 13 | syl2anc 585 |
. . 3
β’ (π β πΉ β (π βpm
β)) |
15 | 14 | biantrurd 534 |
. 2
β’ (π β ((π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)) β (πΉ β (π βpm β) β§ (π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))))) |
16 | 6 | uztrn2 12790 |
. . . . . . . 8
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
17 | 16 | adantll 713 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
18 | | lmmbrf.7 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
19 | 18 | oveq1d 7376 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β ((πΉβπ)π·π) = (π΄π·π)) |
20 | 19 | breq1d 5119 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (((πΉβπ)π·π) < π₯ β (π΄π·π) < π₯)) |
21 | 20 | adantrl 715 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π)) β (((πΉβπ)π·π) < π₯ β (π΄π·π) < π₯)) |
22 | 2 | fdmd 6683 |
. . . . . . . . . . . . . . 15
β’ (π β dom πΉ = π) |
23 | 22 | eleq2d 2820 |
. . . . . . . . . . . . . 14
β’ (π β (π β dom πΉ β π β π)) |
24 | 23 | biimpar 479 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β dom πΉ) |
25 | 2 | ffvelcdmda 7039 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (πΉβπ) β π) |
26 | 24, 25 | jca 513 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (π β dom πΉ β§ (πΉβπ) β π)) |
27 | 26 | biantrurd 534 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (((πΉβπ)π·π) < π₯ β ((π β dom πΉ β§ (πΉβπ) β π) β§ ((πΉβπ)π·π) < π₯))) |
28 | | df-3an 1090 |
. . . . . . . . . . 11
β’ ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯) β ((π β dom πΉ β§ (πΉβπ) β π) β§ ((πΉβπ)π·π) < π₯)) |
29 | 27, 28 | bitr4di 289 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (((πΉβπ)π·π) < π₯ β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
30 | 29 | adantrl 715 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π)) β (((πΉβπ)π·π) < π₯ β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
31 | 21, 30 | bitr3d 281 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π)) β ((π΄π·π) < π₯ β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
32 | 31 | anassrs 469 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β π) β ((π΄π·π) < π₯ β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
33 | 17, 32 | syldan 592 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β ((π΄π·π) < π₯ β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
34 | 33 | ralbidva 3169 |
. . . . 5
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)(π΄π·π) < π₯ β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
35 | 34 | rexbidva 3170 |
. . . 4
β’ (π β (βπ β π βπ β (β€β₯βπ)(π΄π·π) < π₯ β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
36 | 35 | ralbidv 3171 |
. . 3
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(π΄π·π) < π₯ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
37 | 36 | anbi2d 630 |
. 2
β’ (π β ((π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΄π·π) < π₯) β (π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) |
38 | | lmmbr.2 |
. . . 4
β’ π½ = (MetOpenβπ·) |
39 | | lmmbr3.6 |
. . . 4
β’ (π β π β β€) |
40 | 38, 1, 6, 39 | lmmbr3 24647 |
. . 3
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) |
41 | | 3anass 1096 |
. . 3
β’ ((πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)) β (πΉ β (π βpm β) β§ (π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) |
42 | 40, 41 | bitrdi 287 |
. 2
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ (π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))))) |
43 | 15, 37, 42 | 3bitr4rd 312 |
1
β’ (π β (πΉ(βπ‘βπ½)π β (π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΄π·π) < π₯))) |