Step | Hyp | Ref
| Expression |
1 | | breq1 4006 |
. . . . 5
β’ (π₯ = π§ β (π₯ # 0 β π§ # 0)) |
2 | 1 | elrab 2893 |
. . . 4
β’ (π§ β {π₯ β β β£ π₯ # 0} β (π§ β β β§ π§ # 0)) |
3 | | divrecap 8644 |
. . . . 5
β’ ((π¦ β β β§ π§ β β β§ π§ # 0) β (π¦ / π§) = (π¦ Β· (1 / π§))) |
4 | 3 | 3expb 1204 |
. . . 4
β’ ((π¦ β β β§ (π§ β β β§ π§ # 0)) β (π¦ / π§) = (π¦ Β· (1 / π§))) |
5 | 2, 4 | sylan2b 287 |
. . 3
β’ ((π¦ β β β§ π§ β {π₯ β β β£ π₯ # 0}) β (π¦ / π§) = (π¦ Β· (1 / π§))) |
6 | 5 | mpoeq3ia 5939 |
. 2
β’ (π¦ β β, π§ β {π₯ β β β£ π₯ # 0} β¦ (π¦ / π§)) = (π¦ β β, π§ β {π₯ β β β£ π₯ # 0} β¦ (π¦ Β· (1 / π§))) |
7 | | addcncntop.j |
. . . . . 6
β’ π½ = (MetOpenβ(abs β
β )) |
8 | 7 | cntoptopon 13968 |
. . . . 5
β’ π½ β
(TopOnββ) |
9 | 8 | a1i 9 |
. . . 4
β’ (β€
β π½ β
(TopOnββ)) |
10 | | divcnap.k |
. . . . 5
β’ πΎ = (π½ βΎt {π₯ β β β£ π₯ # 0}) |
11 | | ssrab2 3240 |
. . . . . 6
β’ {π₯ β β β£ π₯ # 0} β
β |
12 | | resttopon 13607 |
. . . . . 6
β’ ((π½ β (TopOnββ)
β§ {π₯ β β
β£ π₯ # 0} β
β) β (π½
βΎt {π₯
β β β£ π₯ #
0}) β (TopOnβ{π₯
β β β£ π₯ #
0})) |
13 | 9, 11, 12 | sylancl 413 |
. . . . 5
β’ (β€
β (π½
βΎt {π₯
β β β£ π₯ #
0}) β (TopOnβ{π₯
β β β£ π₯ #
0})) |
14 | 10, 13 | eqeltrid 2264 |
. . . 4
β’ (β€
β πΎ β
(TopOnβ{π₯ β
β β£ π₯ #
0})) |
15 | 9, 14 | cnmpt1st 13724 |
. . . 4
β’ (β€
β (π¦ β β,
π§ β {π₯ β β β£ π₯ # 0} β¦ π¦) β ((π½ Γt πΎ) Cn π½)) |
16 | 9, 14 | cnmpt2nd 13725 |
. . . . 5
β’ (β€
β (π¦ β β,
π§ β {π₯ β β β£ π₯ # 0} β¦ π§) β ((π½ Γt πΎ) Cn πΎ)) |
17 | | eqid 2177 |
. . . . . . . 8
β’ (π β {π₯ β β β£ π₯ # 0} β¦ (1 / π)) = (π β {π₯ β β β£ π₯ # 0} β¦ (1 / π)) |
18 | | breq1 4006 |
. . . . . . . . . 10
β’ (π₯ = π β (π₯ # 0 β π # 0)) |
19 | 18 | elrab 2893 |
. . . . . . . . 9
β’ (π β {π₯ β β β£ π₯ # 0} β (π β β β§ π # 0)) |
20 | | recclap 8635 |
. . . . . . . . 9
β’ ((π β β β§ π # 0) β (1 / π) β
β) |
21 | 19, 20 | sylbi 121 |
. . . . . . . 8
β’ (π β {π₯ β β β£ π₯ # 0} β (1 / π) β β) |
22 | 17, 21 | fmpti 5668 |
. . . . . . 7
β’ (π β {π₯ β β β£ π₯ # 0} β¦ (1 / π)):{π₯ β β β£ π₯ # 0}βΆβ |
23 | | breq1 4006 |
. . . . . . . . . . 11
β’ (π₯ = π β (π₯ # 0 β π # 0)) |
24 | 23 | elrab 2893 |
. . . . . . . . . 10
β’ (π β {π₯ β β β£ π₯ # 0} β (π β β β§ π # 0)) |
25 | | eqid 2177 |
. . . . . . . . . . . 12
β’ (inf({1,
((absβπ) Β·
π)}, β, < )
Β· ((absβπ) /
2)) = (inf({1, ((absβπ) Β· π)}, β, < ) Β·
((absβπ) /
2)) |
26 | 25 | reccn2ap 11320 |
. . . . . . . . . . 11
β’ ((π β β β§ π # 0 β§ π β β+) β
βπ’ β
β+ βπ€ β {π₯ β β β£ π₯ # 0} ((absβ(π€ β π)) < π’ β (absβ((1 / π€) β (1 / π))) < π)) |
27 | 26 | 3expa 1203 |
. . . . . . . . . 10
β’ (((π β β β§ π # 0) β§ π β β+) β
βπ’ β
β+ βπ€ β {π₯ β β β£ π₯ # 0} ((absβ(π€ β π)) < π’ β (absβ((1 / π€) β (1 / π))) < π)) |
28 | 24, 27 | sylanb 284 |
. . . . . . . . 9
β’ ((π β {π₯ β β β£ π₯ # 0} β§ π β β+) β
βπ’ β
β+ βπ€ β {π₯ β β β£ π₯ # 0} ((absβ(π€ β π)) < π’ β (absβ((1 / π€) β (1 / π))) < π)) |
29 | | ovres 6013 |
. . . . . . . . . . . . . . 15
β’ ((π β {π₯ β β β£ π₯ # 0} β§ π€ β {π₯ β β β£ π₯ # 0}) β (π((abs β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0}))π€) = (π(abs β β )π€)) |
30 | | elrabi 2890 |
. . . . . . . . . . . . . . . 16
β’ (π β {π₯ β β β£ π₯ # 0} β π β β) |
31 | | elrabi 2890 |
. . . . . . . . . . . . . . . 16
β’ (π€ β {π₯ β β β£ π₯ # 0} β π€ β β) |
32 | | eqid 2177 |
. . . . . . . . . . . . . . . . . 18
β’ (abs
β β ) = (abs β β ) |
33 | 32 | cnmetdval 13965 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π€ β β) β (π(abs β β )π€) = (absβ(π β π€))) |
34 | | abssub 11109 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π€ β β) β
(absβ(π β π€)) = (absβ(π€ β π))) |
35 | 33, 34 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π€ β β) β (π(abs β β )π€) = (absβ(π€ β π))) |
36 | 30, 31, 35 | syl2an 289 |
. . . . . . . . . . . . . . 15
β’ ((π β {π₯ β β β£ π₯ # 0} β§ π€ β {π₯ β β β£ π₯ # 0}) β (π(abs β β )π€) = (absβ(π€ β π))) |
37 | 29, 36 | eqtrd 2210 |
. . . . . . . . . . . . . 14
β’ ((π β {π₯ β β β£ π₯ # 0} β§ π€ β {π₯ β β β£ π₯ # 0}) β (π((abs β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0}))π€) = (absβ(π€ β π))) |
38 | 37 | breq1d 4013 |
. . . . . . . . . . . . 13
β’ ((π β {π₯ β β β£ π₯ # 0} β§ π€ β {π₯ β β β£ π₯ # 0}) β ((π((abs β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0}))π€) < π’ β (absβ(π€ β π)) < π’)) |
39 | 24 | simprbi 275 |
. . . . . . . . . . . . . . . . . 18
β’ (π β {π₯ β β β£ π₯ # 0} β π # 0) |
40 | 30, 39 | recclapd 8737 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π₯ β β β£ π₯ # 0} β (1 / π) β β) |
41 | | oveq2 5882 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (1 / π) = (1 / π)) |
42 | 41, 17 | fvmptg 5592 |
. . . . . . . . . . . . . . . . 17
β’ ((π β {π₯ β β β£ π₯ # 0} β§ (1 / π) β β) β ((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ) = (1 / π)) |
43 | 40, 42 | mpdan 421 |
. . . . . . . . . . . . . . . 16
β’ (π β {π₯ β β β£ π₯ # 0} β ((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ) = (1 / π)) |
44 | | breq1 4006 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π€ β (π₯ # 0 β π€ # 0)) |
45 | 44 | elrab 2893 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ β {π₯ β β β£ π₯ # 0} β (π€ β β β§ π€ # 0)) |
46 | 45 | simprbi 275 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β {π₯ β β β£ π₯ # 0} β π€ # 0) |
47 | 31, 46 | recclapd 8737 |
. . . . . . . . . . . . . . . . 17
β’ (π€ β {π₯ β β β£ π₯ # 0} β (1 / π€) β β) |
48 | | oveq2 5882 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π€ β (1 / π) = (1 / π€)) |
49 | 48, 17 | fvmptg 5592 |
. . . . . . . . . . . . . . . . 17
β’ ((π€ β {π₯ β β β£ π₯ # 0} β§ (1 / π€) β β) β ((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ€) = (1 / π€)) |
50 | 47, 49 | mpdan 421 |
. . . . . . . . . . . . . . . 16
β’ (π€ β {π₯ β β β£ π₯ # 0} β ((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ€) = (1 / π€)) |
51 | 43, 50 | oveqan12d 5893 |
. . . . . . . . . . . . . . 15
β’ ((π β {π₯ β β β£ π₯ # 0} β§ π€ β {π₯ β β β£ π₯ # 0}) β (((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ)(abs β β )((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ€)) = ((1 / π)(abs β β )(1 / π€))) |
52 | 32 | cnmetdval 13965 |
. . . . . . . . . . . . . . . . 17
β’ (((1 /
π) β β β§ (1
/ π€) β β) β
((1 / π)(abs β
β )(1 / π€)) =
(absβ((1 / π) β
(1 / π€)))) |
53 | | abssub 11109 |
. . . . . . . . . . . . . . . . 17
β’ (((1 /
π) β β β§ (1
/ π€) β β) β
(absβ((1 / π) β
(1 / π€))) = (absβ((1
/ π€) β (1 / π)))) |
54 | 52, 53 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
β’ (((1 /
π) β β β§ (1
/ π€) β β) β
((1 / π)(abs β
β )(1 / π€)) =
(absβ((1 / π€) β
(1 / π)))) |
55 | 40, 47, 54 | syl2an 289 |
. . . . . . . . . . . . . . 15
β’ ((π β {π₯ β β β£ π₯ # 0} β§ π€ β {π₯ β β β£ π₯ # 0}) β ((1 / π)(abs β β )(1 / π€)) = (absβ((1 / π€) β (1 / π)))) |
56 | 51, 55 | eqtrd 2210 |
. . . . . . . . . . . . . 14
β’ ((π β {π₯ β β β£ π₯ # 0} β§ π€ β {π₯ β β β£ π₯ # 0}) β (((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ)(abs β β )((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ€)) = (absβ((1 / π€) β (1 / π)))) |
57 | 56 | breq1d 4013 |
. . . . . . . . . . . . 13
β’ ((π β {π₯ β β β£ π₯ # 0} β§ π€ β {π₯ β β β£ π₯ # 0}) β ((((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ)(abs β β )((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ€)) < π β (absβ((1 / π€) β (1 / π))) < π)) |
58 | 38, 57 | imbi12d 234 |
. . . . . . . . . . . 12
β’ ((π β {π₯ β β β£ π₯ # 0} β§ π€ β {π₯ β β β£ π₯ # 0}) β (((π((abs β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0}))π€) < π’ β (((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ)(abs β β )((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ€)) < π) β ((absβ(π€ β π)) < π’ β (absβ((1 / π€) β (1 / π))) < π))) |
59 | 58 | ralbidva 2473 |
. . . . . . . . . . 11
β’ (π β {π₯ β β β£ π₯ # 0} β (βπ€ β {π₯ β β β£ π₯ # 0} ((π((abs β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0}))π€) < π’ β (((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ)(abs β β )((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ€)) < π) β βπ€ β {π₯ β β β£ π₯ # 0} ((absβ(π€ β π)) < π’ β (absβ((1 / π€) β (1 / π))) < π))) |
60 | 59 | rexbidv 2478 |
. . . . . . . . . 10
β’ (π β {π₯ β β β£ π₯ # 0} β (βπ’ β β+ βπ€ β {π₯ β β β£ π₯ # 0} ((π((abs β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0}))π€) < π’ β (((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ)(abs β β )((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ€)) < π) β βπ’ β β+ βπ€ β {π₯ β β β£ π₯ # 0} ((absβ(π€ β π)) < π’ β (absβ((1 / π€) β (1 / π))) < π))) |
61 | 60 | adantr 276 |
. . . . . . . . 9
β’ ((π β {π₯ β β β£ π₯ # 0} β§ π β β+) β
(βπ’ β
β+ βπ€ β {π₯ β β β£ π₯ # 0} ((π((abs β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0}))π€) < π’ β (((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ)(abs β β )((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ€)) < π) β βπ’ β β+ βπ€ β {π₯ β β β£ π₯ # 0} ((absβ(π€ β π)) < π’ β (absβ((1 / π€) β (1 / π))) < π))) |
62 | 28, 61 | mpbird 167 |
. . . . . . . 8
β’ ((π β {π₯ β β β£ π₯ # 0} β§ π β β+) β
βπ’ β
β+ βπ€ β {π₯ β β β£ π₯ # 0} ((π((abs β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0}))π€) < π’ β (((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ)(abs β β )((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ€)) < π)) |
63 | 62 | rgen2 2563 |
. . . . . . 7
β’
βπ β
{π₯ β β β£
π₯ # 0}βπ β β+
βπ’ β
β+ βπ€ β {π₯ β β β£ π₯ # 0} ((π((abs β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0}))π€) < π’ β (((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ)(abs β β )((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ€)) < π) |
64 | | cnxmet 13967 |
. . . . . . . . 9
β’ (abs
β β ) β (βMetββ) |
65 | | xmetres2 13815 |
. . . . . . . . 9
β’ (((abs
β β ) β (βMetββ) β§ {π₯ β β β£ π₯ # 0} β β) β ((abs β
β ) βΎ ({π₯
β β β£ π₯ #
0} Γ {π₯ β
β β£ π₯ # 0}))
β (βMetβ{π₯
β β β£ π₯ #
0})) |
66 | 64, 11, 65 | mp2an 426 |
. . . . . . . 8
β’ ((abs
β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0})) β (βMetβ{π₯ β β β£ π₯ # 0}) |
67 | | eqid 2177 |
. . . . . . . . . . . 12
β’ ((abs
β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0})) = ((abs β β ) βΎ
({π₯ β β β£
π₯ # 0} Γ {π₯ β β β£ π₯ # 0})) |
68 | | eqid 2177 |
. . . . . . . . . . . 12
β’
(MetOpenβ((abs β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0}))) = (MetOpenβ((abs β
β ) βΎ ({π₯
β β β£ π₯ #
0} Γ {π₯ β
β β£ π₯ #
0}))) |
69 | 67, 7, 68 | metrest 13942 |
. . . . . . . . . . 11
β’ (((abs
β β ) β (βMetββ) β§ {π₯ β β β£ π₯ # 0} β β) β (π½ βΎt {π₯ β β β£ π₯ # 0}) = (MetOpenβ((abs
β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0})))) |
70 | 64, 11, 69 | mp2an 426 |
. . . . . . . . . 10
β’ (π½ βΎt {π₯ β β β£ π₯ # 0}) = (MetOpenβ((abs
β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0}))) |
71 | 10, 70 | eqtri 2198 |
. . . . . . . . 9
β’ πΎ = (MetOpenβ((abs β
β ) βΎ ({π₯
β β β£ π₯ #
0} Γ {π₯ β
β β£ π₯ #
0}))) |
72 | 71, 7 | metcn 13950 |
. . . . . . . 8
β’ ((((abs
β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0})) β (βMetβ{π₯ β β β£ π₯ # 0}) β§ (abs β
β ) β (βMetββ)) β ((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π)) β (πΎ Cn π½) β ((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π)):{π₯ β β β£ π₯ # 0}βΆβ β§ βπ β {π₯ β β β£ π₯ # 0}βπ β β+ βπ’ β β+
βπ€ β {π₯ β β β£ π₯ # 0} ((π((abs β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0}))π€) < π’ β (((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ)(abs β β )((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ€)) < π)))) |
73 | 66, 64, 72 | mp2an 426 |
. . . . . . 7
β’ ((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π)) β (πΎ Cn π½) β ((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π)):{π₯ β β β£ π₯ # 0}βΆβ β§ βπ β {π₯ β β β£ π₯ # 0}βπ β β+ βπ’ β β+
βπ€ β {π₯ β β β£ π₯ # 0} ((π((abs β β ) βΎ ({π₯ β β β£ π₯ # 0} Γ {π₯ β β β£ π₯ # 0}))π€) < π’ β (((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ)(abs β β )((π β {π₯ β β β£ π₯ # 0} β¦ (1 / π))βπ€)) < π))) |
74 | 22, 63, 73 | mpbir2an 942 |
. . . . . 6
β’ (π β {π₯ β β β£ π₯ # 0} β¦ (1 / π)) β (πΎ Cn π½) |
75 | 74 | a1i 9 |
. . . . 5
β’ (β€
β (π β {π₯ β β β£ π₯ # 0} β¦ (1 / π)) β (πΎ Cn π½)) |
76 | | oveq2 5882 |
. . . . 5
β’ (π = π§ β (1 / π) = (1 / π§)) |
77 | 9, 14, 16, 14, 75, 76 | cnmpt21 13727 |
. . . 4
β’ (β€
β (π¦ β β,
π§ β {π₯ β β β£ π₯ # 0} β¦ (1 / π§)) β ((π½ Γt πΎ) Cn π½)) |
78 | 7 | mulcncntop 13990 |
. . . . 5
β’ Β·
β ((π½
Γt π½) Cn
π½) |
79 | 78 | a1i 9 |
. . . 4
β’ (β€
β Β· β ((π½
Γt π½) Cn
π½)) |
80 | 9, 14, 15, 77, 79 | cnmpt22f 13731 |
. . 3
β’ (β€
β (π¦ β β,
π§ β {π₯ β β β£ π₯ # 0} β¦ (π¦ Β· (1 / π§))) β ((π½ Γt πΎ) Cn π½)) |
81 | 80 | mptru 1362 |
. 2
β’ (π¦ β β, π§ β {π₯ β β β£ π₯ # 0} β¦ (π¦ Β· (1 / π§))) β ((π½ Γt πΎ) Cn π½) |
82 | 6, 81 | eqeltri 2250 |
1
β’ (π¦ β β, π§ β {π₯ β β β£ π₯ # 0} β¦ (π¦ / π§)) β ((π½ Γt πΎ) Cn π½) |