Step | Hyp | Ref
| Expression |
1 | | metnrmlem.4 |
. . . . . 6
β’ (π β (π β© π) = β
) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ β π) β (π β© π) = β
) |
3 | | inelcm 4423 |
. . . . . . . 8
β’ ((π΄ β π β§ π΄ β π) β (π β© π) β β
) |
4 | 3 | expcom 415 |
. . . . . . 7
β’ (π΄ β π β (π΄ β π β (π β© π) β β
)) |
5 | 4 | adantl 483 |
. . . . . 6
β’ ((π β§ π΄ β π) β (π΄ β π β (π β© π) β β
)) |
6 | 5 | necon2bd 2958 |
. . . . 5
β’ ((π β§ π΄ β π) β ((π β© π) = β
β Β¬ π΄ β π)) |
7 | 2, 6 | mpd 15 |
. . . 4
β’ ((π β§ π΄ β π) β Β¬ π΄ β π) |
8 | | eqcom 2745 |
. . . . . 6
β’ (0 =
(πΉβπ΄) β (πΉβπ΄) = 0) |
9 | | metnrmlem.1 |
. . . . . . . 8
β’ (π β π· β (βMetβπ)) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ β π) β π· β (βMetβπ)) |
11 | | metnrmlem.2 |
. . . . . . . . . 10
β’ (π β π β (Clsdβπ½)) |
12 | 11 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π΄ β π) β π β (Clsdβπ½)) |
13 | | eqid 2738 |
. . . . . . . . . 10
β’ βͺ π½ =
βͺ π½ |
14 | 13 | cldss 22302 |
. . . . . . . . 9
β’ (π β (Clsdβπ½) β π β βͺ π½) |
15 | 12, 14 | syl 17 |
. . . . . . . 8
β’ ((π β§ π΄ β π) β π β βͺ π½) |
16 | | metdscn.j |
. . . . . . . . . 10
β’ π½ = (MetOpenβπ·) |
17 | 16 | mopnuni 23716 |
. . . . . . . . 9
β’ (π· β (βMetβπ) β π = βͺ π½) |
18 | 10, 17 | syl 17 |
. . . . . . . 8
β’ ((π β§ π΄ β π) β π = βͺ π½) |
19 | 15, 18 | sseqtrrd 3984 |
. . . . . . 7
β’ ((π β§ π΄ β π) β π β π) |
20 | | metnrmlem.3 |
. . . . . . . . . . 11
β’ (π β π β (Clsdβπ½)) |
21 | 20 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π΄ β π) β π β (Clsdβπ½)) |
22 | 13 | cldss 22302 |
. . . . . . . . . 10
β’ (π β (Clsdβπ½) β π β βͺ π½) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π΄ β π) β π β βͺ π½) |
24 | 23, 18 | sseqtrrd 3984 |
. . . . . . . 8
β’ ((π β§ π΄ β π) β π β π) |
25 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π΄ β π) β π΄ β π) |
26 | 24, 25 | sseldd 3944 |
. . . . . . 7
β’ ((π β§ π΄ β π) β π΄ β π) |
27 | | metdscn.f |
. . . . . . . 8
β’ πΉ = (π₯ β π β¦ inf(ran (π¦ β π β¦ (π₯π·π¦)), β*, <
)) |
28 | 27, 16 | metdseq0 24139 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π β π β§ π΄ β π) β ((πΉβπ΄) = 0 β π΄ β ((clsβπ½)βπ))) |
29 | 10, 19, 26, 28 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π΄ β π) β ((πΉβπ΄) = 0 β π΄ β ((clsβπ½)βπ))) |
30 | 8, 29 | bitrid 283 |
. . . . 5
β’ ((π β§ π΄ β π) β (0 = (πΉβπ΄) β π΄ β ((clsβπ½)βπ))) |
31 | | cldcls 22315 |
. . . . . . 7
β’ (π β (Clsdβπ½) β ((clsβπ½)βπ) = π) |
32 | 12, 31 | syl 17 |
. . . . . 6
β’ ((π β§ π΄ β π) β ((clsβπ½)βπ) = π) |
33 | 32 | eleq2d 2824 |
. . . . 5
β’ ((π β§ π΄ β π) β (π΄ β ((clsβπ½)βπ) β π΄ β π)) |
34 | 30, 33 | bitrd 279 |
. . . 4
β’ ((π β§ π΄ β π) β (0 = (πΉβπ΄) β π΄ β π)) |
35 | 7, 34 | mtbird 325 |
. . 3
β’ ((π β§ π΄ β π) β Β¬ 0 = (πΉβπ΄)) |
36 | 27 | metdsf 24133 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π β π) β πΉ:πβΆ(0[,]+β)) |
37 | 10, 19, 36 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π΄ β π) β πΉ:πβΆ(0[,]+β)) |
38 | 37, 26 | ffvelcdmd 7031 |
. . . . . 6
β’ ((π β§ π΄ β π) β (πΉβπ΄) β (0[,]+β)) |
39 | | elxrge0 13303 |
. . . . . . 7
β’ ((πΉβπ΄) β (0[,]+β) β ((πΉβπ΄) β β* β§ 0 β€
(πΉβπ΄))) |
40 | 39 | simprbi 498 |
. . . . . 6
β’ ((πΉβπ΄) β (0[,]+β) β 0 β€ (πΉβπ΄)) |
41 | 38, 40 | syl 17 |
. . . . 5
β’ ((π β§ π΄ β π) β 0 β€ (πΉβπ΄)) |
42 | | 0xr 11136 |
. . . . . 6
β’ 0 β
β* |
43 | | eliccxr 13281 |
. . . . . . 7
β’ ((πΉβπ΄) β (0[,]+β) β (πΉβπ΄) β
β*) |
44 | 38, 43 | syl 17 |
. . . . . 6
β’ ((π β§ π΄ β π) β (πΉβπ΄) β
β*) |
45 | | xrleloe 12992 |
. . . . . 6
β’ ((0
β β* β§ (πΉβπ΄) β β*) β (0 β€
(πΉβπ΄) β (0 < (πΉβπ΄) β¨ 0 = (πΉβπ΄)))) |
46 | 42, 44, 45 | sylancr 588 |
. . . . 5
β’ ((π β§ π΄ β π) β (0 β€ (πΉβπ΄) β (0 < (πΉβπ΄) β¨ 0 = (πΉβπ΄)))) |
47 | 41, 46 | mpbid 231 |
. . . 4
β’ ((π β§ π΄ β π) β (0 < (πΉβπ΄) β¨ 0 = (πΉβπ΄))) |
48 | 47 | ord 863 |
. . 3
β’ ((π β§ π΄ β π) β (Β¬ 0 < (πΉβπ΄) β 0 = (πΉβπ΄))) |
49 | 35, 48 | mt3d 148 |
. 2
β’ ((π β§ π΄ β π) β 0 < (πΉβπ΄)) |
50 | | 1xr 11148 |
. . . . 5
β’ 1 β
β* |
51 | | ifcl 4530 |
. . . . 5
β’ ((1
β β* β§ (πΉβπ΄) β β*) β if(1
β€ (πΉβπ΄), 1, (πΉβπ΄)) β
β*) |
52 | 50, 44, 51 | sylancr 588 |
. . . 4
β’ ((π β§ π΄ β π) β if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)) β
β*) |
53 | | 1red 11090 |
. . . 4
β’ ((π β§ π΄ β π) β 1 β β) |
54 | | 0lt1 11611 |
. . . . . 6
β’ 0 <
1 |
55 | | breq2 5108 |
. . . . . . 7
β’ (1 = if(1
β€ (πΉβπ΄), 1, (πΉβπ΄)) β (0 < 1 β 0 < if(1 β€
(πΉβπ΄), 1, (πΉβπ΄)))) |
56 | | breq2 5108 |
. . . . . . 7
β’ ((πΉβπ΄) = if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)) β (0 < (πΉβπ΄) β 0 < if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)))) |
57 | 55, 56 | ifboth 4524 |
. . . . . 6
β’ ((0 <
1 β§ 0 < (πΉβπ΄)) β 0 < if(1 β€ (πΉβπ΄), 1, (πΉβπ΄))) |
58 | 54, 49, 57 | sylancr 588 |
. . . . 5
β’ ((π β§ π΄ β π) β 0 < if(1 β€ (πΉβπ΄), 1, (πΉβπ΄))) |
59 | | xrltle 12997 |
. . . . . 6
β’ ((0
β β* β§ if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)) β β*) β (0
< if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)) β 0 β€ if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)))) |
60 | 42, 52, 59 | sylancr 588 |
. . . . 5
β’ ((π β§ π΄ β π) β (0 < if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)) β 0 β€ if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)))) |
61 | 58, 60 | mpd 15 |
. . . 4
β’ ((π β§ π΄ β π) β 0 β€ if(1 β€ (πΉβπ΄), 1, (πΉβπ΄))) |
62 | | xrmin1 13025 |
. . . . 5
β’ ((1
β β* β§ (πΉβπ΄) β β*) β if(1
β€ (πΉβπ΄), 1, (πΉβπ΄)) β€ 1) |
63 | 50, 44, 62 | sylancr 588 |
. . . 4
β’ ((π β§ π΄ β π) β if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)) β€ 1) |
64 | | xrrege0 13022 |
. . . 4
β’ (((if(1
β€ (πΉβπ΄), 1, (πΉβπ΄)) β β* β§ 1 β
β) β§ (0 β€ if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)) β§ if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)) β€ 1)) β if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)) β β) |
65 | 52, 53, 61, 63, 64 | syl22anc 838 |
. . 3
β’ ((π β§ π΄ β π) β if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)) β β) |
66 | 65, 58 | elrpd 12883 |
. 2
β’ ((π β§ π΄ β π) β if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)) β
β+) |
67 | 49, 66 | jca 513 |
1
β’ ((π β§ π΄ β π) β (0 < (πΉβπ΄) β§ if(1 β€ (πΉβπ΄), 1, (πΉβπ΄)) β
β+)) |