Step | Hyp | Ref
| Expression |
1 | | metcn.2 |
. . 3
β’ π½ = (MetOpenβπΆ) |
2 | | metcn.4 |
. . 3
β’ πΎ = (MetOpenβπ·) |
3 | 1, 2 | metcnpi2 23924 |
. 2
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β
βπ§ β
β+ βπ¦ β π ((π¦πΆπ) < π§ β ((πΉβπ¦)π·(πΉβπ)) < π΄)) |
4 | | rphalfcl 12950 |
. . . 4
β’ (π§ β β+
β (π§ / 2) β
β+) |
5 | 4 | ad2antrl 727 |
. . 3
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ βπ¦ β
π ((π¦πΆπ) < π§ β ((πΉβπ¦)π·(πΉβπ)) < π΄))) β (π§ / 2) β
β+) |
6 | | simplll 774 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β πΆ β (βMetβπ)) |
7 | | simprr 772 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β π¦ β π) |
8 | | simplrl 776 |
. . . . . . . . . . 11
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β πΉ β ((π½ CnP πΎ)βπ)) |
9 | | eqid 2733 |
. . . . . . . . . . . 12
β’ βͺ π½ =
βͺ π½ |
10 | 9 | cnprcl 22619 |
. . . . . . . . . . 11
β’ (πΉ β ((π½ CnP πΎ)βπ) β π β βͺ π½) |
11 | 8, 10 | syl 17 |
. . . . . . . . . 10
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β π β βͺ π½) |
12 | 1 | mopnuni 23817 |
. . . . . . . . . . 11
β’ (πΆ β (βMetβπ) β π = βͺ π½) |
13 | 6, 12 | syl 17 |
. . . . . . . . . 10
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β π = βͺ π½) |
14 | 11, 13 | eleqtrrd 2837 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β π β π) |
15 | | xmetcl 23707 |
. . . . . . . . 9
β’ ((πΆ β (βMetβπ) β§ π¦ β π β§ π β π) β (π¦πΆπ) β
β*) |
16 | 6, 7, 14, 15 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β (π¦πΆπ) β
β*) |
17 | 4 | ad2antrl 727 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β (π§ / 2) β
β+) |
18 | 17 | rpxrd 12966 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β (π§ / 2) β
β*) |
19 | | rpxr 12932 |
. . . . . . . . 9
β’ (π§ β β+
β π§ β
β*) |
20 | 19 | ad2antrl 727 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β π§ β β*) |
21 | | rphalflt 12952 |
. . . . . . . . 9
β’ (π§ β β+
β (π§ / 2) < π§) |
22 | 21 | ad2antrl 727 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β (π§ / 2) < π§) |
23 | | xrlelttr 13084 |
. . . . . . . . . 10
β’ (((π¦πΆπ) β β* β§ (π§ / 2) β β*
β§ π§ β
β*) β (((π¦πΆπ) β€ (π§ / 2) β§ (π§ / 2) < π§) β (π¦πΆπ) < π§)) |
24 | 23 | expcomd 418 |
. . . . . . . . 9
β’ (((π¦πΆπ) β β* β§ (π§ / 2) β β*
β§ π§ β
β*) β ((π§ / 2) < π§ β ((π¦πΆπ) β€ (π§ / 2) β (π¦πΆπ) < π§))) |
25 | 24 | imp 408 |
. . . . . . . 8
β’ ((((π¦πΆπ) β β* β§ (π§ / 2) β β*
β§ π§ β
β*) β§ (π§ / 2) < π§) β ((π¦πΆπ) β€ (π§ / 2) β (π¦πΆπ) < π§)) |
26 | 16, 18, 20, 22, 25 | syl31anc 1374 |
. . . . . . 7
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β ((π¦πΆπ) β€ (π§ / 2) β (π¦πΆπ) < π§)) |
27 | | simpllr 775 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β π· β (βMetβπ)) |
28 | 1 | mopntopon 23815 |
. . . . . . . . . . . 12
β’ (πΆ β (βMetβπ) β π½ β (TopOnβπ)) |
29 | 6, 28 | syl 17 |
. . . . . . . . . . 11
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β π½ β (TopOnβπ)) |
30 | 2 | mopntopon 23815 |
. . . . . . . . . . . 12
β’ (π· β (βMetβπ) β πΎ β (TopOnβπ)) |
31 | 27, 30 | syl 17 |
. . . . . . . . . . 11
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β πΎ β (TopOnβπ)) |
32 | | cnpf2 22624 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ:πβΆπ) |
33 | 29, 31, 8, 32 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β πΉ:πβΆπ) |
34 | 33, 7 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β (πΉβπ¦) β π) |
35 | 33, 14 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β (πΉβπ) β π) |
36 | | xmetcl 23707 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ (πΉβπ¦) β π β§ (πΉβπ) β π) β ((πΉβπ¦)π·(πΉβπ)) β
β*) |
37 | 27, 34, 35, 36 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β ((πΉβπ¦)π·(πΉβπ)) β
β*) |
38 | | simplrr 777 |
. . . . . . . . 9
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β π΄ β
β+) |
39 | 38 | rpxrd 12966 |
. . . . . . . 8
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β π΄ β
β*) |
40 | | xrltle 13077 |
. . . . . . . 8
β’ ((((πΉβπ¦)π·(πΉβπ)) β β* β§ π΄ β β*)
β (((πΉβπ¦)π·(πΉβπ)) < π΄ β ((πΉβπ¦)π·(πΉβπ)) β€ π΄)) |
41 | 37, 39, 40 | syl2anc 585 |
. . . . . . 7
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β (((πΉβπ¦)π·(πΉβπ)) < π΄ β ((πΉβπ¦)π·(πΉβπ)) β€ π΄)) |
42 | 26, 41 | imim12d 81 |
. . . . . 6
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ π¦ β π)) β (((π¦πΆπ) < π§ β ((πΉβπ¦)π·(πΉβπ)) < π΄) β ((π¦πΆπ) β€ (π§ / 2) β ((πΉβπ¦)π·(πΉβπ)) β€ π΄))) |
43 | 42 | anassrs 469 |
. . . . 5
β’
(((((πΆ β
(βMetβπ) β§
π· β
(βMetβπ)) β§
(πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ π§ β β+)
β§ π¦ β π) β (((π¦πΆπ) < π§ β ((πΉβπ¦)π·(πΉβπ)) < π΄) β ((π¦πΆπ) β€ (π§ / 2) β ((πΉβπ¦)π·(πΉβπ)) β€ π΄))) |
44 | 43 | ralimdva 3161 |
. . . 4
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ π§ β β+)
β (βπ¦ β
π ((π¦πΆπ) < π§ β ((πΉβπ¦)π·(πΉβπ)) < π΄) β βπ¦ β π ((π¦πΆπ) β€ (π§ / 2) β ((πΉβπ¦)π·(πΉβπ)) β€ π΄))) |
45 | 44 | impr 456 |
. . 3
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ βπ¦ β
π ((π¦πΆπ) < π§ β ((πΉβπ¦)π·(πΉβπ)) < π΄))) β βπ¦ β π ((π¦πΆπ) β€ (π§ / 2) β ((πΉβπ¦)π·(πΉβπ)) β€ π΄)) |
46 | | breq2 5113 |
. . . 4
β’ (π₯ = (π§ / 2) β ((π¦πΆπ) β€ π₯ β (π¦πΆπ) β€ (π§ / 2))) |
47 | 46 | rspceaimv 3587 |
. . 3
β’ (((π§ / 2) β β+
β§ βπ¦ β
π ((π¦πΆπ) β€ (π§ / 2) β ((πΉβπ¦)π·(πΉβπ)) β€ π΄)) β βπ₯ β β+ βπ¦ β π ((π¦πΆπ) β€ π₯ β ((πΉβπ¦)π·(πΉβπ)) β€ π΄)) |
48 | 5, 45, 47 | syl2anc 585 |
. 2
β’ ((((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β§ (π§ β β+
β§ βπ¦ β
π ((π¦πΆπ) < π§ β ((πΉβπ¦)π·(πΉβπ)) < π΄))) β βπ₯ β β+ βπ¦ β π ((π¦πΆπ) β€ π₯ β ((πΉβπ¦)π·(πΉβπ)) β€ π΄)) |
49 | 3, 48 | rexlimddv 3155 |
1
β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β
βπ₯ β
β+ βπ¦ β π ((π¦πΆπ) β€ π₯ β ((πΉβπ¦)π·(πΉβπ)) β€ π΄)) |