Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. 2
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β β§ π β β β§ (ππ·π) β€ (π β π
))) β π· β (βMetβπ)) |
2 | | simpl2 1193 |
. 2
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β β§ π β β β§ (ππ·π) β€ (π β π
))) β π β π) |
3 | | simpl3 1194 |
. 2
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β β§ π β β β§ (ππ·π) β€ (π β π
))) β π β π) |
4 | | simpr1 1195 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β β§ π β β β§ (ππ·π) β€ (π β π
))) β π
β β) |
5 | 4 | rexrd 11206 |
. 2
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β β§ π β β β§ (ππ·π) β€ (π β π
))) β π
β
β*) |
6 | | simpr2 1196 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β β§ π β β β§ (ππ·π) β€ (π β π
))) β π β β) |
7 | 6 | rexrd 11206 |
. 2
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β β§ π β β β§ (ππ·π) β€ (π β π
))) β π β
β*) |
8 | 6, 4 | resubcld 11584 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β β§ π β β β§ (ππ·π) β€ (π β π
))) β (π β π
) β β) |
9 | | simpr3 1197 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β β§ π β β β§ (ππ·π) β€ (π β π
))) β (ππ·π) β€ (π β π
)) |
10 | | xmetlecl 23702 |
. . 3
β’ ((π· β (βMetβπ) β§ (π β π β§ π β π) β§ ((π β π
) β β β§ (ππ·π) β€ (π β π
))) β (ππ·π) β β) |
11 | 1, 2, 3, 8, 9, 10 | syl122anc 1380 |
. 2
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β β§ π β β β§ (ππ·π) β€ (π β π
))) β (ππ·π) β β) |
12 | | rexsub 13153 |
. . . 4
β’ ((π β β β§ π
β β) β (π +π
-ππ
) =
(π β π
)) |
13 | 6, 4, 12 | syl2anc 585 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β β§ π β β β§ (ππ·π) β€ (π β π
))) β (π +π
-ππ
) =
(π β π
)) |
14 | 9, 13 | breqtrrd 5134 |
. 2
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β β§ π β β β§ (ππ·π) β€ (π β π
))) β (ππ·π) β€ (π +π
-ππ
)) |
15 | 1, 2, 3, 5, 7, 11,
14 | xblss2 23758 |
1
β’ (((π· β (βMetβπ) β§ π β π β§ π β π) β§ (π
β β β§ π β β β§ (ππ·π) β€ (π β π
))) β (π(ballβπ·)π
) β (π(ballβπ·)π)) |