Step | Hyp | Ref
| Expression |
1 | | rpxr 9661 |
. . . 4
β’ (π
β β+
β π
β
β*) |
2 | | rpgt0 9665 |
. . . 4
β’ (π
β β+
β 0 < π
) |
3 | 1, 2 | jca 306 |
. . 3
β’ (π
β β+
β (π
β
β* β§ 0 < π
)) |
4 | | stdbdmet.1 |
. . . . 5
β’ π· = (π₯ β π, π¦ β π β¦ inf({(π₯πΆπ¦), π
}, β*, <
)) |
5 | 4 | bdxmet 14004 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β π· β (βMetβπ)) |
6 | 5 | 3expb 1204 |
. . 3
β’ ((πΆ β (βMetβπ) β§ (π
β β* β§ 0 <
π
)) β π· β (βMetβπ)) |
7 | 3, 6 | sylan2 286 |
. 2
β’ ((πΆ β (βMetβπ) β§ π
β β+) β π· β (βMetβπ)) |
8 | | xmetcl 13855 |
. . . . . . . 8
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ π¦ β π) β (π₯πΆπ¦) β
β*) |
9 | 8 | 3expb 1204 |
. . . . . . 7
β’ ((πΆ β (βMetβπ) β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β
β*) |
10 | 9 | adantlr 477 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β
β*) |
11 | 1 | ad2antlr 489 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β π
β
β*) |
12 | | xrmincl 11274 |
. . . . . 6
β’ (((π₯πΆπ¦) β β* β§ π
β β*)
β inf({(π₯πΆπ¦), π
}, β*, < ) β
β*) |
13 | 10, 11, 12 | syl2anc 411 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β inf({(π₯πΆπ¦), π
}, β*, < ) β
β*) |
14 | | rpre 9660 |
. . . . . 6
β’ (π
β β+
β π
β
β) |
15 | 14 | ad2antlr 489 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β π
β β) |
16 | | xmetge0 13868 |
. . . . . . . 8
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ π¦ β π) β 0 β€ (π₯πΆπ¦)) |
17 | 16 | 3expb 1204 |
. . . . . . 7
β’ ((πΆ β (βMetβπ) β§ (π₯ β π β§ π¦ β π)) β 0 β€ (π₯πΆπ¦)) |
18 | 17 | adantlr 477 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β 0 β€ (π₯πΆπ¦)) |
19 | | rpge0 9666 |
. . . . . . 7
β’ (π
β β+
β 0 β€ π
) |
20 | 19 | ad2antlr 489 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β 0 β€ π
) |
21 | | 0xr 8004 |
. . . . . . 7
β’ 0 β
β* |
22 | | xrlemininf 11279 |
. . . . . . 7
β’ ((0
β β* β§ (π₯πΆπ¦) β β* β§ π
β β*)
β (0 β€ inf({(π₯πΆπ¦), π
}, β*, < ) β (0
β€ (π₯πΆπ¦) β§ 0 β€ π
))) |
23 | 21, 10, 11, 22 | mp3an2i 1342 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β (0 β€ inf({(π₯πΆπ¦), π
}, β*, < ) β (0
β€ (π₯πΆπ¦) β§ 0 β€ π
))) |
24 | 18, 20, 23 | mpbir2and 944 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β 0 β€ inf({(π₯πΆπ¦), π
}, β*, <
)) |
25 | | xrmin2inf 11276 |
. . . . . 6
β’ (((π₯πΆπ¦) β β* β§ π
β β*)
β inf({(π₯πΆπ¦), π
}, β*, < ) β€ π
) |
26 | 10, 11, 25 | syl2anc 411 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β inf({(π₯πΆπ¦), π
}, β*, < ) β€ π
) |
27 | | xrrege0 9825 |
. . . . 5
β’
(((inf({(π₯πΆπ¦), π
}, β*, < ) β
β* β§ π
β β) β§ (0 β€ inf({(π₯πΆπ¦), π
}, β*, < ) β§
inf({(π₯πΆπ¦), π
}, β*, < ) β€ π
)) β inf({(π₯πΆπ¦), π
}, β*, < ) β
β) |
28 | 13, 15, 24, 26, 27 | syl22anc 1239 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β inf({(π₯πΆπ¦), π
}, β*, < ) β
β) |
29 | 28 | ralrimivva 2559 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π
β β+) β
βπ₯ β π βπ¦ β π inf({(π₯πΆπ¦), π
}, β*, < ) β
β) |
30 | 4 | fmpo 6202 |
. . 3
β’
(βπ₯ β
π βπ¦ β π inf({(π₯πΆπ¦), π
}, β*, < ) β
β β π·:(π Γ π)βΆβ) |
31 | 29, 30 | sylib 122 |
. 2
β’ ((πΆ β (βMetβπ) β§ π
β β+) β π·:(π Γ π)βΆβ) |
32 | | ismet2 13857 |
. 2
β’ (π· β (Metβπ) β (π· β (βMetβπ) β§ π·:(π Γ π)βΆβ)) |
33 | 7, 31, 32 | sylanbrc 417 |
1
β’ ((πΆ β (βMetβπ) β§ π
β β+) β π· β (Metβπ)) |