Step | Hyp | Ref
| Expression |
1 | | rpxr 12929 |
. . . 4
β’ (π
β β+
β π
β
β*) |
2 | | rpgt0 12932 |
. . . 4
β’ (π
β β+
β 0 < π
) |
3 | 1, 2 | jca 513 |
. . 3
β’ (π
β β+
β (π
β
β* β§ 0 < π
)) |
4 | | stdbdmet.1 |
. . . . 5
β’ π· = (π₯ β π, π¦ β π β¦ if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
)) |
5 | 4 | stdbdxmet 23887 |
. . . 4
β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β π· β (βMetβπ)) |
6 | 5 | 3expb 1121 |
. . 3
β’ ((πΆ β (βMetβπ) β§ (π
β β* β§ 0 <
π
)) β π· β (βMetβπ)) |
7 | 3, 6 | sylan2 594 |
. 2
β’ ((πΆ β (βMetβπ) β§ π
β β+) β π· β (βMetβπ)) |
8 | | xmetcl 23700 |
. . . . . . . 8
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ π¦ β π) β (π₯πΆπ¦) β
β*) |
9 | 8 | 3expb 1121 |
. . . . . . 7
β’ ((πΆ β (βMetβπ) β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β
β*) |
10 | 9 | adantlr 714 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β
β*) |
11 | 1 | ad2antlr 726 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β π
β
β*) |
12 | 10, 11 | ifcld 4533 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
) β
β*) |
13 | | rpre 12928 |
. . . . . 6
β’ (π
β β+
β π
β
β) |
14 | 13 | ad2antlr 726 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β π
β β) |
15 | | xmetge0 23713 |
. . . . . . . 8
β’ ((πΆ β (βMetβπ) β§ π₯ β π β§ π¦ β π) β 0 β€ (π₯πΆπ¦)) |
16 | 15 | 3expb 1121 |
. . . . . . 7
β’ ((πΆ β (βMetβπ) β§ (π₯ β π β§ π¦ β π)) β 0 β€ (π₯πΆπ¦)) |
17 | 16 | adantlr 714 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β 0 β€ (π₯πΆπ¦)) |
18 | | rpge0 12933 |
. . . . . . 7
β’ (π
β β+
β 0 β€ π
) |
19 | 18 | ad2antlr 726 |
. . . . . 6
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β 0 β€ π
) |
20 | | breq2 5110 |
. . . . . . 7
β’ ((π₯πΆπ¦) = if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
) β (0 β€ (π₯πΆπ¦) β 0 β€ if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
))) |
21 | | breq2 5110 |
. . . . . . 7
β’ (π
= if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
) β (0 β€ π
β 0 β€ if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
))) |
22 | 20, 21 | ifboth 4526 |
. . . . . 6
β’ ((0 β€
(π₯πΆπ¦) β§ 0 β€ π
) β 0 β€ if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
)) |
23 | 17, 19, 22 | syl2anc 585 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β 0 β€ if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
)) |
24 | | xrmin2 13103 |
. . . . . 6
β’ (((π₯πΆπ¦) β β* β§ π
β β*)
β if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
) β€ π
) |
25 | 10, 11, 24 | syl2anc 585 |
. . . . 5
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
) β€ π
) |
26 | | xrrege0 13099 |
. . . . 5
β’
(((if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
) β β* β§ π
β β) β§ (0 β€
if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
) β§ if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
) β€ π
)) β if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
) β β) |
27 | 12, 14, 23, 25, 26 | syl22anc 838 |
. . . 4
β’ (((πΆ β (βMetβπ) β§ π
β β+) β§ (π₯ β π β§ π¦ β π)) β if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
) β β) |
28 | 27 | ralrimivva 3194 |
. . 3
β’ ((πΆ β (βMetβπ) β§ π
β β+) β
βπ₯ β π βπ¦ β π if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
) β β) |
29 | 4 | fmpo 8001 |
. . 3
β’
(βπ₯ β
π βπ¦ β π if((π₯πΆπ¦) β€ π
, (π₯πΆπ¦), π
) β β β π·:(π Γ π)βΆβ) |
30 | 28, 29 | sylib 217 |
. 2
β’ ((πΆ β (βMetβπ) β§ π
β β+) β π·:(π Γ π)βΆβ) |
31 | | ismet2 23702 |
. 2
β’ (π· β (Metβπ) β (π· β (βMetβπ) β§ π·:(π Γ π)βΆβ)) |
32 | 7, 30, 31 | sylanbrc 584 |
1
β’ ((πΆ β (βMetβπ) β§ π
β β+) β π· β (Metβπ)) |