Step | Hyp | Ref
| Expression |
1 | | metdscn.f |
. . . . . . . . . 10
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
2 | 1 | metdsf 24133 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π β π) β πΉ:πβΆ(0[,]+β)) |
3 | 2 | 3adant3 1133 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β πΉ:πβΆ(0[,]+β)) |
4 | | ssel2 3938 |
. . . . . . . . 9
β’ ((π β π β§ π΄ β π) β π΄ β π) |
5 | 4 | 3adant1 1131 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β π΄ β π) |
6 | 3, 5 | ffvelcdmd 7031 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (πΉβπ΄) β (0[,]+β)) |
7 | | eliccxr 13281 |
. . . . . . 7
β’ ((πΉβπ΄) β (0[,]+β) β (πΉβπ΄) β
β*) |
8 | 6, 7 | syl 17 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (πΉβπ΄) β
β*) |
9 | 8 | xrleidd 13000 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (πΉβπ΄) β€ (πΉβπ΄)) |
10 | | simp1 1137 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β π· β (βMetβπ)) |
11 | | simp2 1138 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β π β π) |
12 | 1 | metdsge 24134 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ (πΉβπ΄) β β*) β ((πΉβπ΄) β€ (πΉβπ΄) β (π β© (π΄(ballβπ·)(πΉβπ΄))) = β
)) |
13 | 10, 11, 5, 8, 12 | syl31anc 1374 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β ((πΉβπ΄) β€ (πΉβπ΄) β (π β© (π΄(ballβπ·)(πΉβπ΄))) = β
)) |
14 | 9, 13 | mpbid 231 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (π β© (π΄(ballβπ·)(πΉβπ΄))) = β
) |
15 | | simpl3 1194 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ 0 < (πΉβπ΄)) β π΄ β π) |
16 | 10 | adantr 482 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ 0 < (πΉβπ΄)) β π· β (βMetβπ)) |
17 | 5 | adantr 482 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ 0 < (πΉβπ΄)) β π΄ β π) |
18 | 8 | adantr 482 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ 0 < (πΉβπ΄)) β (πΉβπ΄) β
β*) |
19 | | simpr 486 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ 0 < (πΉβπ΄)) β 0 < (πΉβπ΄)) |
20 | | xblcntr 23686 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π΄ β π β§ ((πΉβπ΄) β β* β§ 0 <
(πΉβπ΄))) β π΄ β (π΄(ballβπ·)(πΉβπ΄))) |
21 | 16, 17, 18, 19, 20 | syl112anc 1375 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ 0 < (πΉβπ΄)) β π΄ β (π΄(ballβπ·)(πΉβπ΄))) |
22 | | inelcm 4423 |
. . . . . . 7
β’ ((π΄ β π β§ π΄ β (π΄(ballβπ·)(πΉβπ΄))) β (π β© (π΄(ballβπ·)(πΉβπ΄))) β β
) |
23 | 15, 21, 22 | syl2anc 585 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π β π β§ π΄ β π) β§ 0 < (πΉβπ΄)) β (π β© (π΄(ballβπ·)(πΉβπ΄))) β β
) |
24 | 23 | ex 414 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (0 < (πΉβπ΄) β (π β© (π΄(ballβπ·)(πΉβπ΄))) β β
)) |
25 | 24 | necon2bd 2958 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β ((π β© (π΄(ballβπ·)(πΉβπ΄))) = β
β Β¬ 0 < (πΉβπ΄))) |
26 | 14, 25 | mpd 15 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β Β¬ 0 < (πΉβπ΄)) |
27 | | elxrge0 13303 |
. . . . . . 7
β’ ((πΉβπ΄) β (0[,]+β) β ((πΉβπ΄) β β* β§ 0 β€
(πΉβπ΄))) |
28 | 27 | simprbi 498 |
. . . . . 6
β’ ((πΉβπ΄) β (0[,]+β) β 0 β€ (πΉβπ΄)) |
29 | 6, 28 | syl 17 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β 0 β€ (πΉβπ΄)) |
30 | | 0xr 11136 |
. . . . . 6
β’ 0 β
β* |
31 | | xrleloe 12992 |
. . . . . 6
β’ ((0
β β* β§ (πΉβπ΄) β β*) β (0 β€
(πΉβπ΄) β (0 < (πΉβπ΄) β¨ 0 = (πΉβπ΄)))) |
32 | 30, 8, 31 | sylancr 588 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (0 β€ (πΉβπ΄) β (0 < (πΉβπ΄) β¨ 0 = (πΉβπ΄)))) |
33 | 29, 32 | mpbid 231 |
. . . 4
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (0 < (πΉβπ΄) β¨ 0 = (πΉβπ΄))) |
34 | 33 | ord 863 |
. . 3
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (Β¬ 0 < (πΉβπ΄) β 0 = (πΉβπ΄))) |
35 | 26, 34 | mpd 15 |
. 2
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β 0 = (πΉβπ΄)) |
36 | 35 | eqcomd 2744 |
1
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β (πΉβπ΄) = 0) |