| Step | Hyp | Ref
| Expression |
|---|
| 1 | | xmetcl 13992 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β π) β (ππ·π₯) β
β*) |
| 2 | 1 | 3expa 1203 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β (ππ·π₯) β
β*) |
| 3 | 2 | adantlr 477 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*))
β§ π₯ β π) β (ππ·π₯) β
β*) |
| 4 | | simplrl 535 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*))
β§ π₯ β π) β π
β
β*) |
| 5 | | simplrr 536 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*))
β§ π₯ β π) β π β
β*) |
| 6 | | xrltmininf 11281 |
. . . . 5
β’ (((ππ·π₯) β β* β§ π
β β*
β§ π β
β*) β ((ππ·π₯) < inf({π
, π}, β*, < ) β
((ππ·π₯) < π
β§ (ππ·π₯) < π))) |
| 7 | 3, 4, 5, 6 | syl3anc 1238 |
. . . 4
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*))
β§ π₯ β π) β ((ππ·π₯) < inf({π
, π}, β*, < ) β
((ππ·π₯) < π
β§ (ππ·π₯) < π))) |
| 8 | 7 | pm5.32da 452 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*))
β ((π₯ β π β§ (ππ·π₯) < inf({π
, π}, β*, < )) β
(π₯ β π β§ ((ππ·π₯) < π
β§ (ππ·π₯) < π)))) |
| 9 | | xrmincl 11277 |
. . . 4
β’ ((π
β β*
β§ π β
β*) β inf({π
, π}, β*, < ) β
β*) |
| 10 | | elbl 14031 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ inf({π
, π}, β*, < ) β
β*) β (π₯ β (π(ballβπ·)inf({π
, π}, β*, < )) β
(π₯ β π β§ (ππ·π₯) < inf({π
, π}, β*, <
)))) |
| 11 | 10 | 3expa 1203 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ inf({π
, π}, β*, < ) β
β*) β (π₯ β (π(ballβπ·)inf({π
, π}, β*, < )) β
(π₯ β π β§ (ππ·π₯) < inf({π
, π}, β*, <
)))) |
| 12 | 9, 11 | sylan2 286 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*))
β (π₯ β (π(ballβπ·)inf({π
, π}, β*, < )) β
(π₯ β π β§ (ππ·π₯) < inf({π
, π}, β*, <
)))) |
| 13 | | elbl 14031 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β (π₯ β (π(ballβπ·)π
) β (π₯ β π β§ (ππ·π₯) < π
))) |
| 14 | 13 | 3expa 1203 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π β π) β§ π
β β*) β (π₯ β (π(ballβπ·)π
) β (π₯ β π β§ (ππ·π₯) < π
))) |
| 15 | 14 | adantrr 479 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*))
β (π₯ β (π(ballβπ·)π
) β (π₯ β π β§ (ππ·π₯) < π
))) |
| 16 | | elbl 14031 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (π₯ β (π(ballβπ·)π) β (π₯ β π β§ (ππ·π₯) < π))) |
| 17 | 16 | 3expa 1203 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π β π) β§ π β β*) β (π₯ β (π(ballβπ·)π) β (π₯ β π β§ (ππ·π₯) < π))) |
| 18 | 17 | adantrl 478 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*))
β (π₯ β (π(ballβπ·)π) β (π₯ β π β§ (ππ·π₯) < π))) |
| 19 | 15, 18 | anbi12d 473 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*))
β ((π₯ β (π(ballβπ·)π
) β§ π₯ β (π(ballβπ·)π)) β ((π₯ β π β§ (ππ·π₯) < π
) β§ (π₯ β π β§ (ππ·π₯) < π)))) |
| 20 | | elin 3320 |
. . . 4
β’ (π₯ β ((π(ballβπ·)π
) β© (π(ballβπ·)π)) β (π₯ β (π(ballβπ·)π
) β§ π₯ β (π(ballβπ·)π))) |
| 21 | | anandi 590 |
. . . 4
β’ ((π₯ β π β§ ((ππ·π₯) < π
β§ (ππ·π₯) < π)) β ((π₯ β π β§ (ππ·π₯) < π
) β§ (π₯ β π β§ (ππ·π₯) < π))) |
| 22 | 19, 20, 21 | 3bitr4g 223 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*))
β (π₯ β ((π(ballβπ·)π
) β© (π(ballβπ·)π)) β (π₯ β π β§ ((ππ·π₯) < π
β§ (ππ·π₯) < π)))) |
| 23 | 8, 12, 22 | 3bitr4rd 221 |
. 2
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*))
β (π₯ β ((π(ballβπ·)π
) β© (π(ballβπ·)π)) β π₯ β (π(ballβπ·)inf({π
, π}, β*, <
)))) |
| 24 | 23 | eqrdv 2175 |
1
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*))
β ((π(ballβπ·)π
) β© (π(ballβπ·)π)) = (π(ballβπ·)inf({π
, π}, β*, <
))) |
