Step | Hyp | Ref
| Expression |
1 | | blcld.3 |
. 2
β’ π = {π§ β π β£ (ππ·π§) β€ π
} |
2 | | simplr3 1214 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*
β§ π
< π)) β§ π§ β π) β π
< π) |
3 | | xmetcl 24192 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π β§ π§ β π) β (ππ·π§) β
β*) |
4 | 3 | ad4ant124 1170 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*
β§ π
< π)) β§ π§ β π) β (ππ·π§) β
β*) |
5 | | simplr1 1212 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*
β§ π
< π)) β§ π§ β π) β π
β
β*) |
6 | | simplr2 1213 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*
β§ π
< π)) β§ π§ β π) β π β
β*) |
7 | | xrlelttr 13141 |
. . . . . . . 8
β’ (((ππ·π§) β β* β§ π
β β*
β§ π β
β*) β (((ππ·π§) β€ π
β§ π
< π) β (ππ·π§) < π)) |
8 | 7 | expcomd 416 |
. . . . . . 7
β’ (((ππ·π§) β β* β§ π
β β*
β§ π β
β*) β (π
< π β ((ππ·π§) β€ π
β (ππ·π§) < π))) |
9 | 4, 5, 6, 8 | syl3anc 1368 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*
β§ π
< π)) β§ π§ β π) β (π
< π β ((ππ·π§) β€ π
β (ππ·π§) < π))) |
10 | 2, 9 | mpd 15 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*
β§ π
< π)) β§ π§ β π) β ((ππ·π§) β€ π
β (ππ·π§) < π)) |
11 | | simp2 1134 |
. . . . . . 7
β’ ((π
β β*
β§ π β
β* β§ π
< π) β π β
β*) |
12 | | elbl2 24251 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β β*) β§ (π β π β§ π§ β π)) β (π§ β (π(ballβπ·)π) β (ππ·π§) < π)) |
13 | 12 | an4s 657 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π β π) β§ (π β β* β§ π§ β π)) β (π§ β (π(ballβπ·)π) β (ππ·π§) < π)) |
14 | 11, 13 | sylanr1 679 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π β π) β§ ((π
β β* β§ π β β*
β§ π
< π) β§ π§ β π)) β (π§ β (π(ballβπ·)π) β (ππ·π§) < π)) |
15 | 14 | anassrs 467 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*
β§ π
< π)) β§ π§ β π) β (π§ β (π(ballβπ·)π) β (ππ·π§) < π)) |
16 | 10, 15 | sylibrd 259 |
. . . 4
β’ ((((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*
β§ π
< π)) β§ π§ β π) β ((ππ·π§) β€ π
β π§ β (π(ballβπ·)π))) |
17 | 16 | ralrimiva 3140 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*
β§ π
< π)) β βπ§ β π ((ππ·π§) β€ π
β π§ β (π(ballβπ·)π))) |
18 | | rabss 4064 |
. . 3
β’ ({π§ β π β£ (ππ·π§) β€ π
} β (π(ballβπ·)π) β βπ§ β π ((ππ·π§) β€ π
β π§ β (π(ballβπ·)π))) |
19 | 17, 18 | sylibr 233 |
. 2
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*
β§ π
< π)) β {π§ β π β£ (ππ·π§) β€ π
} β (π(ballβπ·)π)) |
20 | 1, 19 | eqsstrid 4025 |
1
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*
β§ π
< π)) β π β (π(ballβπ·)π)) |