Step | Hyp | Ref
| Expression |
1 | | logf1o 26306 |
. . . . . . . 8
β’
log:(β β {0})β1-1-ontoβran
log |
2 | | f1orn 6844 |
. . . . . . . . 9
β’
(log:(β β {0})β1-1-ontoβran
log β (log Fn (β β {0}) β§ Fun β‘log)) |
3 | 2 | simprbi 496 |
. . . . . . . 8
β’
(log:(β β {0})β1-1-ontoβran
log β Fun β‘log) |
4 | | funcnvres 6627 |
. . . . . . . 8
β’ (Fun
β‘log β β‘(log βΎ (β β
(-β(,]0))) = (β‘log βΎ (log
β (β β (-β(,]0))))) |
5 | 1, 3, 4 | mp2b 10 |
. . . . . . 7
β’ β‘(log βΎ (β β
(-β(,]0))) = (β‘log βΎ (log
β (β β (-β(,]0)))) |
6 | | df-log 26298 |
. . . . . . . . . 10
β’ log =
β‘(exp βΎ (β‘β β
(-Ο(,]Ο))) |
7 | 6 | cnveqi 5875 |
. . . . . . . . 9
β’ β‘log = β‘β‘(exp βΎ (β‘β β
(-Ο(,]Ο))) |
8 | | relres 6011 |
. . . . . . . . . 10
β’ Rel (exp
βΎ (β‘β β
(-Ο(,]Ο))) |
9 | | dfrel2 6189 |
. . . . . . . . . 10
β’ (Rel (exp
βΎ (β‘β β
(-Ο(,]Ο))) β β‘β‘(exp βΎ (β‘β β (-Ο(,]Ο))) = (exp
βΎ (β‘β β
(-Ο(,]Ο)))) |
10 | 8, 9 | mpbi 229 |
. . . . . . . . 9
β’ β‘β‘(exp βΎ (β‘β β (-Ο(,]Ο))) = (exp
βΎ (β‘β β
(-Ο(,]Ο))) |
11 | 7, 10 | eqtri 2759 |
. . . . . . . 8
β’ β‘log = (exp βΎ (β‘β β
(-Ο(,]Ο))) |
12 | 11 | reseq1i 5978 |
. . . . . . 7
β’ (β‘log βΎ (log β (β β
(-β(,]0)))) = ((exp βΎ (β‘β β (-Ο(,]Ο))) βΎ
(log β (β β (-β(,]0)))) |
13 | | imassrn 6071 |
. . . . . . . . 9
β’ (log
β (β β (-β(,]0))) β ran log |
14 | | logrn 26300 |
. . . . . . . . 9
β’ ran log =
(β‘β β
(-Ο(,]Ο)) |
15 | 13, 14 | sseqtri 4019 |
. . . . . . . 8
β’ (log
β (β β (-β(,]0))) β (β‘β β
(-Ο(,]Ο)) |
16 | | resabs1 6012 |
. . . . . . . 8
β’ ((log
β (β β (-β(,]0))) β (β‘β β (-Ο(,]Ο)) β ((exp
βΎ (β‘β β
(-Ο(,]Ο))) βΎ (log β (β β (-β(,]0)))) = (exp
βΎ (log β (β β (-β(,]0))))) |
17 | 15, 16 | ax-mp 5 |
. . . . . . 7
β’ ((exp
βΎ (β‘β β
(-Ο(,]Ο))) βΎ (log β (β β (-β(,]0)))) = (exp
βΎ (log β (β β (-β(,]0)))) |
18 | 5, 12, 17 | 3eqtri 2763 |
. . . . . 6
β’ β‘(log βΎ (β β
(-β(,]0))) = (exp βΎ (log β (β β
(-β(,]0)))) |
19 | 18 | imaeq1i 6057 |
. . . . 5
β’ (β‘(log βΎ (β β
(-β(,]0))) β (0(ballβ(abs β β ))π
)) = ((exp βΎ (log β (β
β (-β(,]0)))) β (0(ballβ(abs β β ))π
)) |
20 | | cnxmet 24510 |
. . . . . . . . . . . 12
β’ (abs
β β ) β (βMetββ) |
21 | | 0cnd 11212 |
. . . . . . . . . . . 12
β’ ((π
β β+
β§ π
< Ο) β 0
β β) |
22 | | rpxr 12988 |
. . . . . . . . . . . . 13
β’ (π
β β+
β π
β
β*) |
23 | 22 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π
β β+
β§ π
< Ο) β
π
β
β*) |
24 | | blssm 24145 |
. . . . . . . . . . . 12
β’ (((abs
β β ) β (βMetββ) β§ 0 β β
β§ π
β
β*) β (0(ballβ(abs β β ))π
) β
β) |
25 | 20, 21, 23, 24 | mp3an2i 1465 |
. . . . . . . . . . 11
β’ ((π
β β+
β§ π
< Ο) β
(0(ballβ(abs β β ))π
) β β) |
26 | 25 | sselda 3983 |
. . . . . . . . . 10
β’ (((π
β β+
β§ π
< Ο) β§
π₯ β (0(ballβ(abs
β β ))π
))
β π₯ β
β) |
27 | 26 | imcld 15147 |
. . . . . . . . . . 11
β’ (((π
β β+
β§ π
< Ο) β§
π₯ β (0(ballβ(abs
β β ))π
))
β (ββπ₯)
β β) |
28 | | efopnlem1 26397 |
. . . . . . . . . . . . 13
β’ (((π
β β+
β§ π
< Ο) β§
π₯ β (0(ballβ(abs
β β ))π
))
β (absβ(ββπ₯)) < Ο) |
29 | | pire 26201 |
. . . . . . . . . . . . . 14
β’ Ο
β β |
30 | | abslt 15266 |
. . . . . . . . . . . . . 14
β’
(((ββπ₯)
β β β§ Ο β β) β
((absβ(ββπ₯)) < Ο β (-Ο <
(ββπ₯) β§
(ββπ₯) <
Ο))) |
31 | 27, 29, 30 | sylancl 585 |
. . . . . . . . . . . . 13
β’ (((π
β β+
β§ π
< Ο) β§
π₯ β (0(ballβ(abs
β β ))π
))
β ((absβ(ββπ₯)) < Ο β (-Ο <
(ββπ₯) β§
(ββπ₯) <
Ο))) |
32 | 28, 31 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π
β β+
β§ π
< Ο) β§
π₯ β (0(ballβ(abs
β β ))π
))
β (-Ο < (ββπ₯) β§ (ββπ₯) < Ο)) |
33 | 32 | simpld 494 |
. . . . . . . . . . 11
β’ (((π
β β+
β§ π
< Ο) β§
π₯ β (0(ballβ(abs
β β ))π
))
β -Ο < (ββπ₯)) |
34 | 32 | simprd 495 |
. . . . . . . . . . 11
β’ (((π
β β+
β§ π
< Ο) β§
π₯ β (0(ballβ(abs
β β ))π
))
β (ββπ₯)
< Ο) |
35 | 29 | renegcli 11526 |
. . . . . . . . . . . . 13
β’ -Ο
β β |
36 | 35 | rexri 11277 |
. . . . . . . . . . . 12
β’ -Ο
β β* |
37 | 29 | rexri 11277 |
. . . . . . . . . . . 12
β’ Ο
β β* |
38 | | elioo2 13370 |
. . . . . . . . . . . 12
β’ ((-Ο
β β* β§ Ο β β*) β
((ββπ₯) β
(-Ο(,)Ο) β ((ββπ₯) β β β§ -Ο <
(ββπ₯) β§
(ββπ₯) <
Ο))) |
39 | 36, 37, 38 | mp2an 689 |
. . . . . . . . . . 11
β’
((ββπ₯)
β (-Ο(,)Ο) β ((ββπ₯) β β β§ -Ο <
(ββπ₯) β§
(ββπ₯) <
Ο)) |
40 | 27, 33, 34, 39 | syl3anbrc 1342 |
. . . . . . . . . 10
β’ (((π
β β+
β§ π
< Ο) β§
π₯ β (0(ballβ(abs
β β ))π
))
β (ββπ₯)
β (-Ο(,)Ο)) |
41 | | imf 15065 |
. . . . . . . . . . 11
β’
β:ββΆβ |
42 | | ffn 6718 |
. . . . . . . . . . 11
β’
(β:ββΆβ β β Fn
β) |
43 | | elpreima 7060 |
. . . . . . . . . . 11
β’ (β
Fn β β (π₯ β
(β‘β β (-Ο(,)Ο))
β (π₯ β β
β§ (ββπ₯)
β (-Ο(,)Ο)))) |
44 | 41, 42, 43 | mp2b 10 |
. . . . . . . . . 10
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο))) |
45 | 26, 40, 44 | sylanbrc 582 |
. . . . . . . . 9
β’ (((π
β β+
β§ π
< Ο) β§
π₯ β (0(ballβ(abs
β β ))π
))
β π₯ β (β‘β β
(-Ο(,)Ο))) |
46 | 45 | ex 412 |
. . . . . . . 8
β’ ((π
β β+
β§ π
< Ο) β
(π₯ β
(0(ballβ(abs β β ))π
) β π₯ β (β‘β β
(-Ο(,)Ο)))) |
47 | 46 | ssrdv 3989 |
. . . . . . 7
β’ ((π
β β+
β§ π
< Ο) β
(0(ballβ(abs β β ))π
) β (β‘β β
(-Ο(,)Ο))) |
48 | | df-ima 5690 |
. . . . . . . 8
β’ (log
β (β β (-β(,]0))) = ran (log βΎ (β β
(-β(,]0))) |
49 | | eqid 2731 |
. . . . . . . . . 10
β’ (β
β (-β(,]0)) = (β β (-β(,]0)) |
50 | 49 | logf1o2 26391 |
. . . . . . . . 9
β’ (log
βΎ (β β (-β(,]0))):(β β
(-β(,]0))β1-1-ontoβ(β‘β β
(-Ο(,)Ο)) |
51 | | f1ofo 6841 |
. . . . . . . . 9
β’ ((log
βΎ (β β (-β(,]0))):(β β
(-β(,]0))β1-1-ontoβ(β‘β β (-Ο(,)Ο)) β (log
βΎ (β β (-β(,]0))):(β β
(-β(,]0))βontoβ(β‘β β
(-Ο(,)Ο))) |
52 | | forn 6809 |
. . . . . . . . 9
β’ ((log
βΎ (β β (-β(,]0))):(β β
(-β(,]0))βontoβ(β‘β β (-Ο(,)Ο)) β ran
(log βΎ (β β (-β(,]0))) = (β‘β β
(-Ο(,)Ο))) |
53 | 50, 51, 52 | mp2b 10 |
. . . . . . . 8
β’ ran (log
βΎ (β β (-β(,]0))) = (β‘β β
(-Ο(,)Ο)) |
54 | 48, 53 | eqtri 2759 |
. . . . . . 7
β’ (log
β (β β (-β(,]0))) = (β‘β β
(-Ο(,)Ο)) |
55 | 47, 54 | sseqtrrdi 4034 |
. . . . . 6
β’ ((π
β β+
β§ π
< Ο) β
(0(ballβ(abs β β ))π
) β (log β (β β
(-β(,]0)))) |
56 | | resima2 6017 |
. . . . . 6
β’
((0(ballβ(abs β β ))π
) β (log β (β β
(-β(,]0))) β ((exp βΎ (log β (β β
(-β(,]0)))) β (0(ballβ(abs β β ))π
)) = (exp β
(0(ballβ(abs β β ))π
))) |
57 | 55, 56 | syl 17 |
. . . . 5
β’ ((π
β β+
β§ π
< Ο) β
((exp βΎ (log β (β β (-β(,]0)))) β
(0(ballβ(abs β β ))π
)) = (exp β (0(ballβ(abs β
β ))π
))) |
58 | 19, 57 | eqtrid 2783 |
. . . 4
β’ ((π
β β+
β§ π
< Ο) β
(β‘(log βΎ (β β
(-β(,]0))) β (0(ballβ(abs β β ))π
)) = (exp β (0(ballβ(abs β
β ))π
))) |
59 | 49 | logcn 26388 |
. . . . . 6
β’ (log
βΎ (β β (-β(,]0))) β ((β β
(-β(,]0))βcnββ) |
60 | | difss 4132 |
. . . . . . 7
β’ (β
β (-β(,]0)) β β |
61 | | ssid 4005 |
. . . . . . 7
β’ β
β β |
62 | | efopn.j |
. . . . . . . 8
β’ π½ =
(TopOpenββfld) |
63 | | eqid 2731 |
. . . . . . . 8
β’ (π½ βΎt (β
β (-β(,]0))) = (π½ βΎt (β β
(-β(,]0))) |
64 | 62 | cnfldtopon 24520 |
. . . . . . . . 9
β’ π½ β
(TopOnββ) |
65 | 64 | toponrestid 22644 |
. . . . . . . 8
β’ π½ = (π½ βΎt
β) |
66 | 62, 63, 65 | cncfcn 24651 |
. . . . . . 7
β’
(((β β (-β(,]0)) β β β§ β β
β) β ((β β (-β(,]0))βcnββ) = ((π½ βΎt (β β
(-β(,]0))) Cn π½)) |
67 | 60, 61, 66 | mp2an 689 |
. . . . . 6
β’ ((β
β (-β(,]0))βcnββ) = ((π½ βΎt (β β
(-β(,]0))) Cn π½) |
68 | 59, 67 | eleqtri 2830 |
. . . . 5
β’ (log
βΎ (β β (-β(,]0))) β ((π½ βΎt (β β
(-β(,]0))) Cn π½) |
69 | 62 | cnfldtopn 24519 |
. . . . . . 7
β’ π½ = (MetOpenβ(abs β
β )) |
70 | 69 | blopn 24230 |
. . . . . 6
β’ (((abs
β β ) β (βMetββ) β§ 0 β β
β§ π
β
β*) β (0(ballβ(abs β β ))π
) β π½) |
71 | 20, 21, 23, 70 | mp3an2i 1465 |
. . . . 5
β’ ((π
β β+
β§ π
< Ο) β
(0(ballβ(abs β β ))π
) β π½) |
72 | | cnima 22990 |
. . . . 5
β’ (((log
βΎ (β β (-β(,]0))) β ((π½ βΎt (β β
(-β(,]0))) Cn π½)
β§ (0(ballβ(abs β β ))π
) β π½) β (β‘(log βΎ (β β
(-β(,]0))) β (0(ballβ(abs β β ))π
)) β (π½ βΎt (β β
(-β(,]0)))) |
73 | 68, 71, 72 | sylancr 586 |
. . . 4
β’ ((π
β β+
β§ π
< Ο) β
(β‘(log βΎ (β β
(-β(,]0))) β (0(ballβ(abs β β ))π
)) β (π½ βΎt (β β
(-β(,]0)))) |
74 | 58, 73 | eqeltrrd 2833 |
. . 3
β’ ((π
β β+
β§ π
< Ο) β
(exp β (0(ballβ(abs β β ))π
)) β (π½ βΎt (β β
(-β(,]0)))) |
75 | 62 | cnfldtop 24521 |
. . . 4
β’ π½ β Top |
76 | 49 | logdmopn 26390 |
. . . . 5
β’ (β
β (-β(,]0)) β
(TopOpenββfld) |
77 | 76, 62 | eleqtrri 2831 |
. . . 4
β’ (β
β (-β(,]0)) β π½ |
78 | | restopn2 22902 |
. . . 4
β’ ((π½ β Top β§ (β
β (-β(,]0)) β π½) β ((exp β (0(ballβ(abs
β β ))π
))
β (π½
βΎt (β β (-β(,]0))) β ((exp β
(0(ballβ(abs β β ))π
)) β π½ β§ (exp β (0(ballβ(abs
β β ))π
))
β (β β (-β(,]0))))) |
79 | 75, 77, 78 | mp2an 689 |
. . 3
β’ ((exp
β (0(ballβ(abs β β ))π
)) β (π½ βΎt (β β
(-β(,]0))) β ((exp β (0(ballβ(abs β β
))π
)) β π½ β§ (exp β
(0(ballβ(abs β β ))π
)) β (β β
(-β(,]0)))) |
80 | 74, 79 | sylib 217 |
. 2
β’ ((π
β β+
β§ π
< Ο) β
((exp β (0(ballβ(abs β β ))π
)) β π½ β§ (exp β (0(ballβ(abs
β β ))π
))
β (β β (-β(,]0)))) |
81 | 80 | simpld 494 |
1
β’ ((π
β β+
β§ π
< Ο) β
(exp β (0(ballβ(abs β β ))π
)) β π½) |