Step | Hyp | Ref
| Expression |
1 | | df-div 11872 |
. . 3
β’ / =
(π₯ β β, π¦ β (β β {0})
β¦ (β©π§
β β (π¦ Β·
π§) = π₯)) |
2 | | eldifsn 4791 |
. . . . 5
β’ (π¦ β (β β {0})
β (π¦ β β
β§ π¦ β
0)) |
3 | | divval 11874 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β β§ π¦ β 0) β (π₯ / π¦) = (β©π§ β β (π¦ Β· π§) = π₯)) |
4 | | divrec 11888 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β β§ π¦ β 0) β (π₯ / π¦) = (π₯ Β· (1 / π¦))) |
5 | 3, 4 | eqtr3d 2775 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β β§ π¦ β 0) β
(β©π§ β
β (π¦ Β· π§) = π₯) = (π₯ Β· (1 / π¦))) |
6 | 5 | 3expb 1121 |
. . . . 5
β’ ((π₯ β β β§ (π¦ β β β§ π¦ β 0)) β
(β©π§ β
β (π¦ Β· π§) = π₯) = (π₯ Β· (1 / π¦))) |
7 | 2, 6 | sylan2b 595 |
. . . 4
β’ ((π₯ β β β§ π¦ β (β β {0}))
β (β©π§
β β (π¦ Β·
π§) = π₯) = (π₯ Β· (1 / π¦))) |
8 | 7 | mpoeq3ia 7487 |
. . 3
β’ (π₯ β β, π¦ β (β β {0})
β¦ (β©π§
β β (π¦ Β·
π§) = π₯)) = (π₯ β β, π¦ β (β β {0}) β¦ (π₯ Β· (1 / π¦))) |
9 | 1, 8 | eqtri 2761 |
. 2
β’ / =
(π₯ β β, π¦ β (β β {0})
β¦ (π₯ Β· (1 /
π¦))) |
10 | | addcn.j |
. . . . . 6
β’ π½ =
(TopOpenββfld) |
11 | 10 | cnfldtopon 24299 |
. . . . 5
β’ π½ β
(TopOnββ) |
12 | 11 | a1i 11 |
. . . 4
β’ (β€
β π½ β
(TopOnββ)) |
13 | | divcn.k |
. . . . 5
β’ πΎ = (π½ βΎt (β β
{0})) |
14 | | difss 4132 |
. . . . . 6
β’ (β
β {0}) β β |
15 | | resttopon 22665 |
. . . . . 6
β’ ((π½ β (TopOnββ)
β§ (β β {0}) β β) β (π½ βΎt (β β {0}))
β (TopOnβ(β β {0}))) |
16 | 12, 14, 15 | sylancl 587 |
. . . . 5
β’ (β€
β (π½
βΎt (β β {0})) β (TopOnβ(β β
{0}))) |
17 | 13, 16 | eqeltrid 2838 |
. . . 4
β’ (β€
β πΎ β
(TopOnβ(β β {0}))) |
18 | 12, 17 | cnmpt1st 23172 |
. . . 4
β’ (β€
β (π₯ β β,
π¦ β (β β
{0}) β¦ π₯) β
((π½ Γt
πΎ) Cn π½)) |
19 | 12, 17 | cnmpt2nd 23173 |
. . . . 5
β’ (β€
β (π₯ β β,
π¦ β (β β
{0}) β¦ π¦) β
((π½ Γt
πΎ) Cn πΎ)) |
20 | | eqid 2733 |
. . . . . . . 8
β’ (π§ β (β β {0})
β¦ (1 / π§)) = (π§ β (β β {0})
β¦ (1 / π§)) |
21 | | eldifsn 4791 |
. . . . . . . . 9
β’ (π§ β (β β {0})
β (π§ β β
β§ π§ β
0)) |
22 | | reccl 11879 |
. . . . . . . . 9
β’ ((π§ β β β§ π§ β 0) β (1 / π§) β
β) |
23 | 21, 22 | sylbi 216 |
. . . . . . . 8
β’ (π§ β (β β {0})
β (1 / π§) β
β) |
24 | 20, 23 | fmpti 7112 |
. . . . . . 7
β’ (π§ β (β β {0})
β¦ (1 / π§)):(β
β {0})βΆβ |
25 | | eqid 2733 |
. . . . . . . . . 10
β’ (if(1
β€ ((absβπ₯)
Β· π¦), 1,
((absβπ₯) Β·
π¦)) Β·
((absβπ₯) / 2)) =
(if(1 β€ ((absβπ₯)
Β· π¦), 1,
((absβπ₯) Β·
π¦)) Β·
((absβπ₯) /
2)) |
26 | 25 | reccn2 15541 |
. . . . . . . . 9
β’ ((π₯ β (β β {0})
β§ π¦ β
β+) β βπ’ β β+ βπ€ β (β β
{0})((absβ(π€ β
π₯)) < π’ β (absβ((1 / π€) β (1 / π₯))) < π¦)) |
27 | | ovres 7573 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (β β {0})
β§ π€ β (β
β {0})) β (π₯((abs β β ) βΎ ((β
β {0}) Γ (β β {0})))π€) = (π₯(abs β β )π€)) |
28 | | eldifi 4127 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (β β {0})
β π₯ β
β) |
29 | | eldifi 4127 |
. . . . . . . . . . . . . . . 16
β’ (π€ β (β β {0})
β π€ β
β) |
30 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ (abs
β β ) = (abs β β ) |
31 | 30 | cnmetdval 24287 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π€ β β) β (π₯(abs β β )π€) = (absβ(π₯ β π€))) |
32 | | abssub 15273 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π€ β β) β
(absβ(π₯ β π€)) = (absβ(π€ β π₯))) |
33 | 31, 32 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π€ β β) β (π₯(abs β β )π€) = (absβ(π€ β π₯))) |
34 | 28, 29, 33 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (β β {0})
β§ π€ β (β
β {0})) β (π₯(abs
β β )π€) =
(absβ(π€ β π₯))) |
35 | 27, 34 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((π₯ β (β β {0})
β§ π€ β (β
β {0})) β (π₯((abs β β ) βΎ ((β
β {0}) Γ (β β {0})))π€) = (absβ(π€ β π₯))) |
36 | 35 | breq1d 5159 |
. . . . . . . . . . . . 13
β’ ((π₯ β (β β {0})
β§ π€ β (β
β {0})) β ((π₯((abs β β ) βΎ ((β
β {0}) Γ (β β {0})))π€) < π’ β (absβ(π€ β π₯)) < π’)) |
37 | | oveq2 7417 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π₯ β (1 / π§) = (1 / π₯)) |
38 | | ovex 7442 |
. . . . . . . . . . . . . . . . 17
β’ (1 /
π₯) β
V |
39 | 37, 20, 38 | fvmpt 6999 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (β β {0})
β ((π§ β (β
β {0}) β¦ (1 / π§))βπ₯) = (1 / π₯)) |
40 | | oveq2 7417 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π€ β (1 / π§) = (1 / π€)) |
41 | | ovex 7442 |
. . . . . . . . . . . . . . . . 17
β’ (1 /
π€) β
V |
42 | 40, 20, 41 | fvmpt 6999 |
. . . . . . . . . . . . . . . 16
β’ (π€ β (β β {0})
β ((π§ β (β
β {0}) β¦ (1 / π§))βπ€) = (1 / π€)) |
43 | 39, 42 | oveqan12d 7428 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (β β {0})
β§ π€ β (β
β {0})) β (((π§
β (β β {0}) β¦ (1 / π§))βπ₯)(abs β β )((π§ β (β β {0}) β¦ (1 /
π§))βπ€)) = ((1 / π₯)(abs β β )(1 / π€))) |
44 | | eldifsn 4791 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (β β {0})
β (π₯ β β
β§ π₯ β
0)) |
45 | | reccl 11879 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π₯ β 0) β (1 / π₯) β
β) |
46 | 44, 45 | sylbi 216 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (β β {0})
β (1 / π₯) β
β) |
47 | | eldifsn 4791 |
. . . . . . . . . . . . . . . . 17
β’ (π€ β (β β {0})
β (π€ β β
β§ π€ β
0)) |
48 | | reccl 11879 |
. . . . . . . . . . . . . . . . 17
β’ ((π€ β β β§ π€ β 0) β (1 / π€) β
β) |
49 | 47, 48 | sylbi 216 |
. . . . . . . . . . . . . . . 16
β’ (π€ β (β β {0})
β (1 / π€) β
β) |
50 | 30 | cnmetdval 24287 |
. . . . . . . . . . . . . . . . 17
β’ (((1 /
π₯) β β β§ (1
/ π€) β β) β
((1 / π₯)(abs β
β )(1 / π€)) =
(absβ((1 / π₯) β
(1 / π€)))) |
51 | | abssub 15273 |
. . . . . . . . . . . . . . . . 17
β’ (((1 /
π₯) β β β§ (1
/ π€) β β) β
(absβ((1 / π₯) β
(1 / π€))) = (absβ((1
/ π€) β (1 / π₯)))) |
52 | 50, 51 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ (((1 /
π₯) β β β§ (1
/ π€) β β) β
((1 / π₯)(abs β
β )(1 / π€)) =
(absβ((1 / π€) β
(1 / π₯)))) |
53 | 46, 49, 52 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (β β {0})
β§ π€ β (β
β {0})) β ((1 / π₯)(abs β β )(1 / π€)) = (absβ((1 / π€) β (1 / π₯)))) |
54 | 43, 53 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((π₯ β (β β {0})
β§ π€ β (β
β {0})) β (((π§
β (β β {0}) β¦ (1 / π§))βπ₯)(abs β β )((π§ β (β β {0}) β¦ (1 /
π§))βπ€)) = (absβ((1 / π€) β (1 / π₯)))) |
55 | 54 | breq1d 5159 |
. . . . . . . . . . . . 13
β’ ((π₯ β (β β {0})
β§ π€ β (β
β {0})) β ((((π§
β (β β {0}) β¦ (1 / π§))βπ₯)(abs β β )((π§ β (β β {0}) β¦ (1 /
π§))βπ€)) < π¦ β (absβ((1 / π€) β (1 / π₯))) < π¦)) |
56 | 36, 55 | imbi12d 345 |
. . . . . . . . . . . 12
β’ ((π₯ β (β β {0})
β§ π€ β (β
β {0})) β (((π₯((abs β β ) βΎ ((β
β {0}) Γ (β β {0})))π€) < π’ β (((π§ β (β β {0}) β¦ (1 /
π§))βπ₯)(abs β β )((π§ β (β β {0})
β¦ (1 / π§))βπ€)) < π¦) β ((absβ(π€ β π₯)) < π’ β (absβ((1 / π€) β (1 / π₯))) < π¦))) |
57 | 56 | ralbidva 3176 |
. . . . . . . . . . 11
β’ (π₯ β (β β {0})
β (βπ€ β
(β β {0})((π₯((abs β β ) βΎ ((β
β {0}) Γ (β β {0})))π€) < π’ β (((π§ β (β β {0}) β¦ (1 /
π§))βπ₯)(abs β β )((π§ β (β β {0})
β¦ (1 / π§))βπ€)) < π¦) β βπ€ β (β β
{0})((absβ(π€ β
π₯)) < π’ β (absβ((1 / π€) β (1 / π₯))) < π¦))) |
58 | 57 | rexbidv 3179 |
. . . . . . . . . 10
β’ (π₯ β (β β {0})
β (βπ’ β
β+ βπ€ β (β β {0})((π₯((abs β β ) βΎ
((β β {0}) Γ (β β {0})))π€) < π’ β (((π§ β (β β {0}) β¦ (1 /
π§))βπ₯)(abs β β )((π§ β (β β {0})
β¦ (1 / π§))βπ€)) < π¦) β βπ’ β β+ βπ€ β (β β
{0})((absβ(π€ β
π₯)) < π’ β (absβ((1 / π€) β (1 / π₯))) < π¦))) |
59 | 58 | adantr 482 |
. . . . . . . . 9
β’ ((π₯ β (β β {0})
β§ π¦ β
β+) β (βπ’ β β+ βπ€ β (β β
{0})((π₯((abs β
β ) βΎ ((β β {0}) Γ (β β {0})))π€) < π’ β (((π§ β (β β {0}) β¦ (1 /
π§))βπ₯)(abs β β )((π§ β (β β {0})
β¦ (1 / π§))βπ€)) < π¦) β βπ’ β β+ βπ€ β (β β
{0})((absβ(π€ β
π₯)) < π’ β (absβ((1 / π€) β (1 / π₯))) < π¦))) |
60 | 26, 59 | mpbird 257 |
. . . . . . . 8
β’ ((π₯ β (β β {0})
β§ π¦ β
β+) β βπ’ β β+ βπ€ β (β β
{0})((π₯((abs β
β ) βΎ ((β β {0}) Γ (β β {0})))π€) < π’ β (((π§ β (β β {0}) β¦ (1 /
π§))βπ₯)(abs β β )((π§ β (β β {0})
β¦ (1 / π§))βπ€)) < π¦)) |
61 | 60 | rgen2 3198 |
. . . . . . 7
β’
βπ₯ β
(β β {0})βπ¦ β β+ βπ’ β β+
βπ€ β (β
β {0})((π₯((abs
β β ) βΎ ((β β {0}) Γ (β β
{0})))π€) < π’ β (((π§ β (β β {0}) β¦ (1 /
π§))βπ₯)(abs β β )((π§ β (β β {0})
β¦ (1 / π§))βπ€)) < π¦) |
62 | | cnxmet 24289 |
. . . . . . . . 9
β’ (abs
β β ) β (βMetββ) |
63 | | xmetres2 23867 |
. . . . . . . . 9
β’ (((abs
β β ) β (βMetββ) β§ (β β {0})
β β) β ((abs β β ) βΎ ((β β {0})
Γ (β β {0}))) β (βMetβ(β β
{0}))) |
64 | 62, 14, 63 | mp2an 691 |
. . . . . . . 8
β’ ((abs
β β ) βΎ ((β β {0}) Γ (β β
{0}))) β (βMetβ(β β {0})) |
65 | | eqid 2733 |
. . . . . . . . . . . 12
β’ ((abs
β β ) βΎ ((β β {0}) Γ (β β
{0}))) = ((abs β β ) βΎ ((β β {0}) Γ
(β β {0}))) |
66 | 10 | cnfldtopn 24298 |
. . . . . . . . . . . 12
β’ π½ = (MetOpenβ(abs β
β )) |
67 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(MetOpenβ((abs β β ) βΎ ((β β {0})
Γ (β β {0})))) = (MetOpenβ((abs β β )
βΎ ((β β {0}) Γ (β β
{0})))) |
68 | 65, 66, 67 | metrest 24033 |
. . . . . . . . . . 11
β’ (((abs
β β ) β (βMetββ) β§ (β β {0})
β β) β (π½
βΎt (β β {0})) = (MetOpenβ((abs β
β ) βΎ ((β β {0}) Γ (β β
{0}))))) |
69 | 62, 14, 68 | mp2an 691 |
. . . . . . . . . 10
β’ (π½ βΎt (β
β {0})) = (MetOpenβ((abs β β ) βΎ ((β
β {0}) Γ (β β {0})))) |
70 | 13, 69 | eqtri 2761 |
. . . . . . . . 9
β’ πΎ = (MetOpenβ((abs β
β ) βΎ ((β β {0}) Γ (β β
{0})))) |
71 | 70, 66 | metcn 24052 |
. . . . . . . 8
β’ ((((abs
β β ) βΎ ((β β {0}) Γ (β β
{0}))) β (βMetβ(β β {0})) β§ (abs β
β ) β (βMetββ)) β ((π§ β (β β {0}) β¦ (1 /
π§)) β (πΎ Cn π½) β ((π§ β (β β {0}) β¦ (1 /
π§)):(β β
{0})βΆβ β§ βπ₯ β (β β {0})βπ¦ β β+
βπ’ β
β+ βπ€ β (β β {0})((π₯((abs β β ) βΎ
((β β {0}) Γ (β β {0})))π€) < π’ β (((π§ β (β β {0}) β¦ (1 /
π§))βπ₯)(abs β β )((π§ β (β β {0})
β¦ (1 / π§))βπ€)) < π¦)))) |
72 | 64, 62, 71 | mp2an 691 |
. . . . . . 7
β’ ((π§ β (β β {0})
β¦ (1 / π§)) β
(πΎ Cn π½) β ((π§ β (β β {0}) β¦ (1 /
π§)):(β β
{0})βΆβ β§ βπ₯ β (β β {0})βπ¦ β β+
βπ’ β
β+ βπ€ β (β β {0})((π₯((abs β β ) βΎ
((β β {0}) Γ (β β {0})))π€) < π’ β (((π§ β (β β {0}) β¦ (1 /
π§))βπ₯)(abs β β )((π§ β (β β {0})
β¦ (1 / π§))βπ€)) < π¦))) |
73 | 24, 61, 72 | mpbir2an 710 |
. . . . . 6
β’ (π§ β (β β {0})
β¦ (1 / π§)) β
(πΎ Cn π½) |
74 | 73 | a1i 11 |
. . . . 5
β’ (β€
β (π§ β (β
β {0}) β¦ (1 / π§)) β (πΎ Cn π½)) |
75 | | oveq2 7417 |
. . . . 5
β’ (π§ = π¦ β (1 / π§) = (1 / π¦)) |
76 | 12, 17, 19, 17, 74, 75 | cnmpt21 23175 |
. . . 4
β’ (β€
β (π₯ β β,
π¦ β (β β
{0}) β¦ (1 / π¦))
β ((π½
Γt πΎ) Cn
π½)) |
77 | 10 | mulcn 24383 |
. . . . 5
β’ Β·
β ((π½
Γt π½) Cn
π½) |
78 | 77 | a1i 11 |
. . . 4
β’ (β€
β Β· β ((π½
Γt π½) Cn
π½)) |
79 | 12, 17, 18, 76, 78 | cnmpt22f 23179 |
. . 3
β’ (β€
β (π₯ β β,
π¦ β (β β
{0}) β¦ (π₯ Β· (1
/ π¦))) β ((π½ Γt πΎ) Cn π½)) |
80 | 79 | mptru 1549 |
. 2
β’ (π₯ β β, π¦ β (β β {0})
β¦ (π₯ Β· (1 /
π¦))) β ((π½ Γt πΎ) Cn π½) |
81 | 9, 80 | eqeltri 2830 |
1
β’ / β
((π½ Γt
πΎ) Cn π½) |