Step | Hyp | Ref
| Expression |
1 | | n0 4307 |
. . 3
β’ ((π(ballβπ·)π
) β β
β βπ₯ π₯ β (π(ballβπ·)π
)) |
2 | | elbl 23744 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β (π₯ β (π(ballβπ·)π
) β (π₯ β π β§ (ππ·π₯) < π
))) |
3 | | xmetge0 23700 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β π) β 0 β€ (ππ·π₯)) |
4 | 3 | 3expa 1119 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β 0 β€ (ππ·π₯)) |
5 | 4 | 3adantl3 1169 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π₯ β π) β 0 β€ (ππ·π₯)) |
6 | | 0xr 11203 |
. . . . . . . 8
β’ 0 β
β* |
7 | | xmetcl 23687 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π β π β§ π₯ β π) β (ππ·π₯) β
β*) |
8 | 7 | 3expa 1119 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π β π) β§ π₯ β π) β (ππ·π₯) β
β*) |
9 | 8 | 3adantl3 1169 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π₯ β π) β (ππ·π₯) β
β*) |
10 | | simpl3 1194 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π₯ β π) β π
β
β*) |
11 | | xrlelttr 13076 |
. . . . . . . 8
β’ ((0
β β* β§ (ππ·π₯) β β* β§ π
β β*)
β ((0 β€ (ππ·π₯) β§ (ππ·π₯) < π
) β 0 < π
)) |
12 | 6, 9, 10, 11 | mp3an2i 1467 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π₯ β π) β ((0 β€ (ππ·π₯) β§ (ππ·π₯) < π
) β 0 < π
)) |
13 | 5, 12 | mpand 694 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π β π β§ π
β β*) β§ π₯ β π) β ((ππ·π₯) < π
β 0 < π
)) |
14 | 13 | expimpd 455 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β ((π₯ β π β§ (ππ·π₯) < π
) β 0 < π
)) |
15 | 2, 14 | sylbid 239 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β (π₯ β (π(ballβπ·)π
) β 0 < π
)) |
16 | 15 | exlimdv 1937 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β
(βπ₯ π₯ β (π(ballβπ·)π
) β 0 < π
)) |
17 | 1, 16 | biimtrid 241 |
. 2
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β ((π(ballβπ·)π
) β β
β 0 < π
)) |
18 | | xblcntr 23767 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ (π
β β* β§ 0 <
π
)) β π β (π(ballβπ·)π
)) |
19 | 18 | ne0d 4296 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ (π
β β* β§ 0 <
π
)) β (π(ballβπ·)π
) β β
) |
20 | 19 | 3expa 1119 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ 0 <
π
)) β (π(ballβπ·)π
) β β
) |
21 | 20 | expr 458 |
. . 3
β’ (((π· β (βMetβπ) β§ π β π) β§ π
β β*) β (0 <
π
β (π(ballβπ·)π
) β β
)) |
22 | 21 | 3impa 1111 |
. 2
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β (0 <
π
β (π(ballβπ·)π
) β β
)) |
23 | 17, 22 | impbid 211 |
1
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β ((π(ballβπ·)π
) β β
β 0 < π
)) |