Step | Hyp | Ref
| Expression |
1 | | cnplimcim.j |
. . . . . 6
β’ π½ = (πΎ βΎt π΄) |
2 | | cnplimcim.k |
. . . . . . . 8
β’ πΎ = (MetOpenβ(abs β
β )) |
3 | 2 | cntoptopon 14002 |
. . . . . . 7
β’ πΎ β
(TopOnββ) |
4 | | simpl 109 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β π΄) β π΄ β β) |
5 | | resttopon 13641 |
. . . . . . 7
β’ ((πΎ β (TopOnββ)
β§ π΄ β β)
β (πΎ
βΎt π΄)
β (TopOnβπ΄)) |
6 | 3, 4, 5 | sylancr 414 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β π΄) β (πΎ βΎt π΄) β (TopOnβπ΄)) |
7 | 1, 6 | eqeltrid 2264 |
. . . . 5
β’ ((π΄ β β β§ π΅ β π΄) β π½ β (TopOnβπ΄)) |
8 | | cnpf2 13677 |
. . . . . 6
β’ ((π½ β (TopOnβπ΄) β§ πΎ β (TopOnββ) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β πΉ:π΄βΆβ) |
9 | 8 | 3expia 1205 |
. . . . 5
β’ ((π½ β (TopOnβπ΄) β§ πΎ β (TopOnββ)) β (πΉ β ((π½ CnP πΎ)βπ΅) β πΉ:π΄βΆβ)) |
10 | 7, 3, 9 | sylancl 413 |
. . . 4
β’ ((π΄ β β β§ π΅ β π΄) β (πΉ β ((π½ CnP πΎ)βπ΅) β πΉ:π΄βΆβ)) |
11 | 10 | imp 124 |
. . 3
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β πΉ:π΄βΆβ) |
12 | | simplr 528 |
. . . . 5
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β π΅ β π΄) |
13 | 11, 12 | ffvelcdmd 5652 |
. . . 4
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β (πΉβπ΅) β β) |
14 | | simpr 110 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β πΉ β ((π½ CnP πΎ)βπ΅)) |
15 | | simpll 527 |
. . . . . . . . . 10
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ:π΄βΆβ) β π΄ β β) |
16 | | cnxmet 14001 |
. . . . . . . . . . . 12
β’ (abs
β β ) β (βMetββ) |
17 | | eqid 2177 |
. . . . . . . . . . . . 13
β’ ((abs
β β ) βΎ (π΄ Γ π΄)) = ((abs β β ) βΎ (π΄ Γ π΄)) |
18 | | eqid 2177 |
. . . . . . . . . . . . 13
β’
(MetOpenβ((abs β β ) βΎ (π΄ Γ π΄))) = (MetOpenβ((abs β β )
βΎ (π΄ Γ π΄))) |
19 | 17, 2, 18 | metrest 13976 |
. . . . . . . . . . . 12
β’ (((abs
β β ) β (βMetββ) β§ π΄ β β) β (πΎ βΎt π΄) = (MetOpenβ((abs β β )
βΎ (π΄ Γ π΄)))) |
20 | 16, 19 | mpan 424 |
. . . . . . . . . . 11
β’ (π΄ β β β (πΎ βΎt π΄) = (MetOpenβ((abs β
β ) βΎ (π΄
Γ π΄)))) |
21 | 1, 20 | eqtrid 2222 |
. . . . . . . . . 10
β’ (π΄ β β β π½ = (MetOpenβ((abs β
β ) βΎ (π΄
Γ π΄)))) |
22 | 15, 21 | syl 14 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ:π΄βΆβ) β π½ = (MetOpenβ((abs β β )
βΎ (π΄ Γ π΄)))) |
23 | 2 | a1i 9 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ:π΄βΆβ) β πΎ = (MetOpenβ(abs β β
))) |
24 | | xmetres2 13849 |
. . . . . . . . . 10
β’ (((abs
β β ) β (βMetββ) β§ π΄ β β) β ((abs β
β ) βΎ (π΄
Γ π΄)) β
(βMetβπ΄)) |
25 | 16, 15, 24 | sylancr 414 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ:π΄βΆβ) β ((abs β
β ) βΎ (π΄
Γ π΄)) β
(βMetβπ΄)) |
26 | 16 | a1i 9 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ:π΄βΆβ) β (abs β β
) β (βMetββ)) |
27 | | simplr 528 |
. . . . . . . . 9
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ:π΄βΆβ) β π΅ β π΄) |
28 | 22, 23, 25, 26, 27 | metcnpd 13990 |
. . . . . . . 8
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ:π΄βΆβ) β (πΉ β ((π½ CnP πΎ)βπ΅) β (πΉ:π΄βΆβ β§ βπ β β+
βπ β
β+ βπ§ β π΄ ((π΅((abs β β ) βΎ (π΄ Γ π΄))π§) < π β ((πΉβπ΅)(abs β β )(πΉβπ§)) < π)))) |
29 | 11, 28 | syldan 282 |
. . . . . . 7
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β (πΉ β ((π½ CnP πΎ)βπ΅) β (πΉ:π΄βΆβ β§ βπ β β+
βπ β
β+ βπ§ β π΄ ((π΅((abs β β ) βΎ (π΄ Γ π΄))π§) < π β ((πΉβπ΅)(abs β β )(πΉβπ§)) < π)))) |
30 | 14, 29 | mpbid 147 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β (πΉ:π΄βΆβ β§ βπ β β+
βπ β
β+ βπ§ β π΄ ((π΅((abs β β ) βΎ (π΄ Γ π΄))π§) < π β ((πΉβπ΅)(abs β β )(πΉβπ§)) < π))) |
31 | 30 | simprd 114 |
. . . . 5
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β βπ β β+ βπ β β+
βπ§ β π΄ ((π΅((abs β β ) βΎ (π΄ Γ π΄))π§) < π β ((πΉβπ΅)(abs β β )(πΉβπ§)) < π)) |
32 | 12 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β π΅ β π΄) |
33 | | simpr 110 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β π§ β π΄) |
34 | 32, 33 | ovresd 6014 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β (π΅((abs β β ) βΎ (π΄ Γ π΄))π§) = (π΅(abs β β )π§)) |
35 | 15, 27 | sseldd 3156 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ:π΄βΆβ) β π΅ β β) |
36 | 11, 35 | syldan 282 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β π΅ β β) |
37 | 36 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β π΅ β β) |
38 | | simpll 527 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β π΄ β β) |
39 | 38 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β π΄ β β) |
40 | 39, 33 | sseldd 3156 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β π§ β β) |
41 | | eqid 2177 |
. . . . . . . . . . . . . . 15
β’ (abs
β β ) = (abs β β ) |
42 | 41 | cnmetdval 13999 |
. . . . . . . . . . . . . 14
β’ ((π΅ β β β§ π§ β β) β (π΅(abs β β )π§) = (absβ(π΅ β π§))) |
43 | 37, 40, 42 | syl2anc 411 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β (π΅(abs β β )π§) = (absβ(π΅ β π§))) |
44 | 37, 40 | abssubd 11201 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β (absβ(π΅ β π§)) = (absβ(π§ β π΅))) |
45 | 34, 43, 44 | 3eqtrd 2214 |
. . . . . . . . . . . 12
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β (π΅((abs β β ) βΎ (π΄ Γ π΄))π§) = (absβ(π§ β π΅))) |
46 | 45 | breq1d 4013 |
. . . . . . . . . . 11
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β ((π΅((abs β β ) βΎ (π΄ Γ π΄))π§) < π β (absβ(π§ β π΅)) < π)) |
47 | 46 | biimprd 158 |
. . . . . . . . . 10
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β ((absβ(π§ β π΅)) < π β (π΅((abs β β ) βΎ (π΄ Γ π΄))π§) < π)) |
48 | 47 | adantld 278 |
. . . . . . . . 9
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (π΅((abs β β ) βΎ (π΄ Γ π΄))π§) < π)) |
49 | 13 | ad3antrrr 492 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β (πΉβπ΅) β β) |
50 | 11 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β πΉ:π΄βΆβ) |
51 | 50, 33 | ffvelcdmd 5652 |
. . . . . . . . . . . . 13
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β (πΉβπ§) β β) |
52 | 41 | cnmetdval 13999 |
. . . . . . . . . . . . 13
β’ (((πΉβπ΅) β β β§ (πΉβπ§) β β) β ((πΉβπ΅)(abs β β )(πΉβπ§)) = (absβ((πΉβπ΅) β (πΉβπ§)))) |
53 | 49, 51, 52 | syl2anc 411 |
. . . . . . . . . . . 12
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β ((πΉβπ΅)(abs β β )(πΉβπ§)) = (absβ((πΉβπ΅) β (πΉβπ§)))) |
54 | 49, 51 | abssubd 11201 |
. . . . . . . . . . . 12
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β (absβ((πΉβπ΅) β (πΉβπ§))) = (absβ((πΉβπ§) β (πΉβπ΅)))) |
55 | 53, 54 | eqtrd 2210 |
. . . . . . . . . . 11
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β ((πΉβπ΅)(abs β β )(πΉβπ§)) = (absβ((πΉβπ§) β (πΉβπ΅)))) |
56 | 55 | breq1d 4013 |
. . . . . . . . . 10
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β (((πΉβπ΅)(abs β β )(πΉβπ§)) < π β (absβ((πΉβπ§) β (πΉβπ΅))) < π)) |
57 | 56 | biimpd 144 |
. . . . . . . . 9
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β (((πΉβπ΅)(abs β β )(πΉβπ§)) < π β (absβ((πΉβπ§) β (πΉβπ΅))) < π)) |
58 | 48, 57 | imim12d 74 |
. . . . . . . 8
β’
((((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β§ π§ β π΄) β (((π΅((abs β β ) βΎ (π΄ Γ π΄))π§) < π β ((πΉβπ΅)(abs β β )(πΉβπ§)) < π) β ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β (πΉβπ΅))) < π))) |
59 | 58 | ralimdva 2544 |
. . . . . . 7
β’
(((((π΄ β
β β§ π΅ β
π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β§ π β β+)
β (βπ§ β
π΄ ((π΅((abs β β ) βΎ (π΄ Γ π΄))π§) < π β ((πΉβπ΅)(abs β β )(πΉβπ§)) < π) β βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β (πΉβπ΅))) < π))) |
60 | 59 | reximdva 2579 |
. . . . . 6
β’ ((((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β§ π β β+) β
(βπ β
β+ βπ§ β π΄ ((π΅((abs β β ) βΎ (π΄ Γ π΄))π§) < π β ((πΉβπ΅)(abs β β )(πΉβπ§)) < π) β βπ β β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β (πΉβπ΅))) < π))) |
61 | 60 | ralimdva 2544 |
. . . . 5
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β (βπ β β+ βπ β β+
βπ§ β π΄ ((π΅((abs β β ) βΎ (π΄ Γ π΄))π§) < π β ((πΉβπ΅)(abs β β )(πΉβπ§)) < π) β βπ β β+ βπ β β+
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β (πΉβπ΅))) < π))) |
62 | 31, 61 | mpd 13 |
. . . 4
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β βπ β β+ βπ β β+
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β (πΉβπ΅))) < π)) |
63 | 11, 38, 36 | ellimc3ap 14100 |
. . . 4
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β ((πΉβπ΅) β (πΉ limβ π΅) β ((πΉβπ΅) β β β§ βπ β β+
βπ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β (πΉβπ΅))) < π)))) |
64 | 13, 62, 63 | mpbir2and 944 |
. . 3
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β (πΉβπ΅) β (πΉ limβ π΅)) |
65 | 11, 64 | jca 306 |
. 2
β’ (((π΄ β β β§ π΅ β π΄) β§ πΉ β ((π½ CnP πΎ)βπ΅)) β (πΉ:π΄βΆβ β§ (πΉβπ΅) β (πΉ limβ π΅))) |
66 | 65 | ex 115 |
1
β’ ((π΄ β β β§ π΅ β π΄) β (πΉ β ((π½ CnP πΎ)βπ΅) β (πΉ:π΄βΆβ β§ (πΉβπ΅) β (πΉ limβ π΅)))) |