Step | Hyp | Ref
| Expression |
1 | | breq2 5113 |
. . . . 5
β’ (π₯ = π
β (((πΉβπ)π·π) < π₯ β ((πΉβπ)π·π) < π
)) |
2 | 1 | 3anbi3d 1443 |
. . . 4
β’ (π₯ = π
β ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯) β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π
))) |
3 | 2 | rexralbidv 3211 |
. . 3
β’ (π₯ = π
β (βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯) β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π
))) |
4 | | lmmcvg.8 |
. . . . 5
β’ (π β πΉ(βπ‘βπ½)π) |
5 | | lmmbr.2 |
. . . . . 6
β’ π½ = (MetOpenβπ·) |
6 | | lmmbr.3 |
. . . . . 6
β’ (π β π· β (βMetβπ)) |
7 | | lmmbr3.5 |
. . . . . 6
β’ π =
(β€β₯βπ) |
8 | | lmmbr3.6 |
. . . . . 6
β’ (π β π β β€) |
9 | 5, 6, 7, 8 | lmmbr3 24647 |
. . . . 5
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) |
10 | 4, 9 | mpbid 231 |
. . . 4
β’ (π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯))) |
11 | 10 | simp3d 1145 |
. . 3
β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)) |
12 | | lmmcvg.9 |
. . 3
β’ (π β π
β
β+) |
13 | 3, 11, 12 | rspcdva 3584 |
. 2
β’ (π β βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π
)) |
14 | 7 | uztrn2 12790 |
. . . . . 6
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
15 | | 3simpc 1151 |
. . . . . . 7
β’ ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π
) β ((πΉβπ) β π β§ ((πΉβπ)π·π) < π
)) |
16 | | lmmbrf.7 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
17 | 16 | eleq1d 2819 |
. . . . . . . 8
β’ ((π β§ π β π) β ((πΉβπ) β π β π΄ β π)) |
18 | 16 | oveq1d 7376 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((πΉβπ)π·π) = (π΄π·π)) |
19 | 18 | breq1d 5119 |
. . . . . . . 8
β’ ((π β§ π β π) β (((πΉβπ)π·π) < π
β (π΄π·π) < π
)) |
20 | 17, 19 | anbi12d 632 |
. . . . . . 7
β’ ((π β§ π β π) β (((πΉβπ) β π β§ ((πΉβπ)π·π) < π
) β (π΄ β π β§ (π΄π·π) < π
))) |
21 | 15, 20 | imbitrid 243 |
. . . . . 6
β’ ((π β§ π β π) β ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π
) β (π΄ β π β§ (π΄π·π) < π
))) |
22 | 14, 21 | sylan2 594 |
. . . . 5
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π
) β (π΄ β π β§ (π΄π·π) < π
))) |
23 | 22 | anassrs 469 |
. . . 4
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π
) β (π΄ β π β§ (π΄π·π) < π
))) |
24 | 23 | ralimdva 3161 |
. . 3
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π
) β βπ β (β€β₯βπ)(π΄ β π β§ (π΄π·π) < π
))) |
25 | 24 | reximdva 3162 |
. 2
β’ (π β (βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π
) β βπ β π βπ β (β€β₯βπ)(π΄ β π β§ (π΄π·π) < π
))) |
26 | 13, 25 | mpd 15 |
1
β’ (π β βπ β π βπ β (β€β₯βπ)(π΄ β π β§ (π΄π·π) < π
)) |