Step | Hyp | Ref
| Expression |
1 | | cnxmet 24288 |
. . . . . . 7
β’ (abs
β β ) β (βMetββ) |
2 | | reperflem.3 |
. . . . . . . 8
β’ π β
β |
3 | 2 | sseli 3978 |
. . . . . . 7
β’ (π’ β π β π’ β β) |
4 | | recld2.1 |
. . . . . . . . 9
β’ π½ =
(TopOpenββfld) |
5 | 4 | cnfldtopn 24297 |
. . . . . . . 8
β’ π½ = (MetOpenβ(abs β
β )) |
6 | 5 | neibl 24009 |
. . . . . . 7
β’ (((abs
β β ) β (βMetββ) β§ π’ β β) β (π β ((neiβπ½)β{π’}) β (π β β β§ βπ β β+
(π’(ballβ(abs β
β ))π) β π))) |
7 | 1, 3, 6 | sylancr 587 |
. . . . . 6
β’ (π’ β π β (π β ((neiβπ½)β{π’}) β (π β β β§ βπ β β+
(π’(ballβ(abs β
β ))π) β π))) |
8 | | ssrin 4233 |
. . . . . . . . 9
β’ ((π’(ballβ(abs β β
))π) β π β ((π’(ballβ(abs β β ))π) β© (π β {π’})) β (π β© (π β {π’}))) |
9 | | reperflem.2 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β π β§ π£ β β) β (π’ + π£) β π) |
10 | 9 | ralrimiva 3146 |
. . . . . . . . . . . . . . . 16
β’ (π’ β π β βπ£ β β (π’ + π£) β π) |
11 | | rpre 12981 |
. . . . . . . . . . . . . . . . 17
β’ (π β β+
β π β
β) |
12 | 11 | rehalfcld 12458 |
. . . . . . . . . . . . . . . 16
β’ (π β β+
β (π / 2) β
β) |
13 | | oveq2 7416 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ = (π / 2) β (π’ + π£) = (π’ + (π / 2))) |
14 | 13 | eleq1d 2818 |
. . . . . . . . . . . . . . . . 17
β’ (π£ = (π / 2) β ((π’ + π£) β π β (π’ + (π / 2)) β π)) |
15 | 14 | rspccva 3611 |
. . . . . . . . . . . . . . . 16
β’
((βπ£ β
β (π’ + π£) β π β§ (π / 2) β β) β (π’ + (π / 2)) β π) |
16 | 10, 12, 15 | syl2an 596 |
. . . . . . . . . . . . . . 15
β’ ((π’ β π β§ π β β+) β (π’ + (π / 2)) β π) |
17 | 2, 16 | sselid 3980 |
. . . . . . . . . . . . . 14
β’ ((π’ β π β§ π β β+) β (π’ + (π / 2)) β β) |
18 | 3 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π’ β π β§ π β β+) β π’ β
β) |
19 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’ (abs
β β ) = (abs β β ) |
20 | 19 | cnmetdval 24286 |
. . . . . . . . . . . . . 14
β’ (((π’ + (π / 2)) β β β§ π’ β β) β ((π’ + (π / 2))(abs β β )π’) = (absβ((π’ + (π / 2)) β π’))) |
21 | 17, 18, 20 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((π’ β π β§ π β β+) β ((π’ + (π / 2))(abs β β )π’) = (absβ((π’ + (π / 2)) β π’))) |
22 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
β’ ((π’ β π β§ π β β+) β π β
β+) |
23 | 22 | rphalfcld 13027 |
. . . . . . . . . . . . . . . 16
β’ ((π’ β π β§ π β β+) β (π / 2) β
β+) |
24 | 23 | rpcnd 13017 |
. . . . . . . . . . . . . . 15
β’ ((π’ β π β§ π β β+) β (π / 2) β
β) |
25 | 18, 24 | pncan2d 11572 |
. . . . . . . . . . . . . 14
β’ ((π’ β π β§ π β β+) β ((π’ + (π / 2)) β π’) = (π / 2)) |
26 | 25 | fveq2d 6895 |
. . . . . . . . . . . . 13
β’ ((π’ β π β§ π β β+) β
(absβ((π’ + (π / 2)) β π’)) = (absβ(π / 2))) |
27 | 23 | rpred 13015 |
. . . . . . . . . . . . . 14
β’ ((π’ β π β§ π β β+) β (π / 2) β
β) |
28 | 23 | rpge0d 13019 |
. . . . . . . . . . . . . 14
β’ ((π’ β π β§ π β β+) β 0 β€
(π / 2)) |
29 | 27, 28 | absidd 15368 |
. . . . . . . . . . . . 13
β’ ((π’ β π β§ π β β+) β
(absβ(π / 2)) =
(π / 2)) |
30 | 21, 26, 29 | 3eqtrd 2776 |
. . . . . . . . . . . 12
β’ ((π’ β π β§ π β β+) β ((π’ + (π / 2))(abs β β )π’) = (π / 2)) |
31 | | rphalflt 13002 |
. . . . . . . . . . . . 13
β’ (π β β+
β (π / 2) < π) |
32 | 31 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π’ β π β§ π β β+) β (π / 2) < π) |
33 | 30, 32 | eqbrtrd 5170 |
. . . . . . . . . . 11
β’ ((π’ β π β§ π β β+) β ((π’ + (π / 2))(abs β β )π’) < π) |
34 | 1 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π’ β π β§ π β β+) β (abs
β β ) β (βMetββ)) |
35 | | rpxr 12982 |
. . . . . . . . . . . . 13
β’ (π β β+
β π β
β*) |
36 | 35 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π’ β π β§ π β β+) β π β
β*) |
37 | | elbl3 23897 |
. . . . . . . . . . . 12
β’ ((((abs
β β ) β (βMetββ) β§ π β β*) β§ (π’ β β β§ (π’ + (π / 2)) β β)) β ((π’ + (π / 2)) β (π’(ballβ(abs β β ))π) β ((π’ + (π / 2))(abs β β )π’) < π)) |
38 | 34, 36, 18, 17, 37 | syl22anc 837 |
. . . . . . . . . . 11
β’ ((π’ β π β§ π β β+) β ((π’ + (π / 2)) β (π’(ballβ(abs β β ))π) β ((π’ + (π / 2))(abs β β )π’) < π)) |
39 | 33, 38 | mpbird 256 |
. . . . . . . . . 10
β’ ((π’ β π β§ π β β+) β (π’ + (π / 2)) β (π’(ballβ(abs β β ))π)) |
40 | 23 | rpne0d 13020 |
. . . . . . . . . . . . 13
β’ ((π’ β π β§ π β β+) β (π / 2) β 0) |
41 | 25, 40 | eqnetrd 3008 |
. . . . . . . . . . . 12
β’ ((π’ β π β§ π β β+) β ((π’ + (π / 2)) β π’) β 0) |
42 | 17, 18, 41 | subne0ad 11581 |
. . . . . . . . . . 11
β’ ((π’ β π β§ π β β+) β (π’ + (π / 2)) β π’) |
43 | | eldifsn 4790 |
. . . . . . . . . . 11
β’ ((π’ + (π / 2)) β (π β {π’}) β ((π’ + (π / 2)) β π β§ (π’ + (π / 2)) β π’)) |
44 | 16, 42, 43 | sylanbrc 583 |
. . . . . . . . . 10
β’ ((π’ β π β§ π β β+) β (π’ + (π / 2)) β (π β {π’})) |
45 | | inelcm 4464 |
. . . . . . . . . 10
β’ (((π’ + (π / 2)) β (π’(ballβ(abs β β ))π) β§ (π’ + (π / 2)) β (π β {π’})) β ((π’(ballβ(abs β β ))π) β© (π β {π’})) β β
) |
46 | 39, 44, 45 | syl2anc 584 |
. . . . . . . . 9
β’ ((π’ β π β§ π β β+) β ((π’(ballβ(abs β β
))π) β© (π β {π’})) β β
) |
47 | | ssn0 4400 |
. . . . . . . . . 10
β’ ((((π’(ballβ(abs β β
))π) β© (π β {π’})) β (π β© (π β {π’})) β§ ((π’(ballβ(abs β β ))π) β© (π β {π’})) β β
) β (π β© (π β {π’})) β β
) |
48 | 47 | ex 413 |
. . . . . . . . 9
β’ (((π’(ballβ(abs β β
))π) β© (π β {π’})) β (π β© (π β {π’})) β (((π’(ballβ(abs β β ))π) β© (π β {π’})) β β
β (π β© (π β {π’})) β β
)) |
49 | 8, 46, 48 | syl2imc 41 |
. . . . . . . 8
β’ ((π’ β π β§ π β β+) β ((π’(ballβ(abs β β
))π) β π β (π β© (π β {π’})) β β
)) |
50 | 49 | rexlimdva 3155 |
. . . . . . 7
β’ (π’ β π β (βπ β β+ (π’(ballβ(abs β β
))π) β π β (π β© (π β {π’})) β β
)) |
51 | 50 | adantld 491 |
. . . . . 6
β’ (π’ β π β ((π β β β§ βπ β β+
(π’(ballβ(abs β
β ))π) β π) β (π β© (π β {π’})) β β
)) |
52 | 7, 51 | sylbid 239 |
. . . . 5
β’ (π’ β π β (π β ((neiβπ½)β{π’}) β (π β© (π β {π’})) β β
)) |
53 | 52 | ralrimiv 3145 |
. . . 4
β’ (π’ β π β βπ β ((neiβπ½)β{π’})(π β© (π β {π’})) β β
) |
54 | 4 | cnfldtop 24299 |
. . . . 5
β’ π½ β Top |
55 | 4 | cnfldtopon 24298 |
. . . . . . 7
β’ π½ β
(TopOnββ) |
56 | 55 | toponunii 22417 |
. . . . . 6
β’ β =
βͺ π½ |
57 | 56 | islp2 22648 |
. . . . 5
β’ ((π½ β Top β§ π β β β§ π’ β β) β (π’ β ((limPtβπ½)βπ) β βπ β ((neiβπ½)β{π’})(π β© (π β {π’})) β β
)) |
58 | 54, 2, 3, 57 | mp3an12i 1465 |
. . . 4
β’ (π’ β π β (π’ β ((limPtβπ½)βπ) β βπ β ((neiβπ½)β{π’})(π β© (π β {π’})) β β
)) |
59 | 53, 58 | mpbird 256 |
. . 3
β’ (π’ β π β π’ β ((limPtβπ½)βπ)) |
60 | 59 | ssriv 3986 |
. 2
β’ π β ((limPtβπ½)βπ) |
61 | | eqid 2732 |
. . . 4
β’ (π½ βΎt π) = (π½ βΎt π) |
62 | 56, 61 | restperf 22687 |
. . 3
β’ ((π½ β Top β§ π β β) β ((π½ βΎt π) β Perf β π β ((limPtβπ½)βπ))) |
63 | 54, 2, 62 | mp2an 690 |
. 2
β’ ((π½ βΎt π) β Perf β π β ((limPtβπ½)βπ)) |
64 | 60, 63 | mpbir 230 |
1
β’ (π½ βΎt π) β Perf |