Step | Hyp | Ref
| Expression |
1 | | logf1o 26065 |
. . . . . 6
β’
log:(β β {0})β1-1-ontoβran
log |
2 | | f1ofun 6833 |
. . . . . 6
β’
(log:(β β {0})β1-1-ontoβran
log β Fun log) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
β’ Fun
log |
4 | | logcn.d |
. . . . . . 7
β’ π· = (β β
(-β(,]0)) |
5 | 4 | logdmss 26142 |
. . . . . 6
β’ π· β (β β
{0}) |
6 | | f1odm 6835 |
. . . . . . 7
β’
(log:(β β {0})β1-1-ontoβran
log β dom log = (β β {0})) |
7 | 1, 6 | ax-mp 5 |
. . . . . 6
β’ dom log =
(β β {0}) |
8 | 5, 7 | sseqtrri 4019 |
. . . . 5
β’ π· β dom
log |
9 | | funimass4 6954 |
. . . . 5
β’ ((Fun log
β§ π· β dom log)
β ((log β π·)
β (β‘β β
(-Ο(,)Ο)) β βπ₯ β π· (logβπ₯) β (β‘β β
(-Ο(,)Ο)))) |
10 | 3, 8, 9 | mp2an 691 |
. . . 4
β’ ((log
β π·) β (β‘β β (-Ο(,)Ο)) β
βπ₯ β π· (logβπ₯) β (β‘β β
(-Ο(,)Ο))) |
11 | 4 | ellogdm 26139 |
. . . . . . 7
β’ (π₯ β π· β (π₯ β β β§ (π₯ β β β π₯ β
β+))) |
12 | 11 | simplbi 499 |
. . . . . 6
β’ (π₯ β π· β π₯ β β) |
13 | 4 | logdmn0 26140 |
. . . . . 6
β’ (π₯ β π· β π₯ β 0) |
14 | 12, 13 | logcld 26071 |
. . . . 5
β’ (π₯ β π· β (logβπ₯) β β) |
15 | 14 | imcld 15139 |
. . . . . 6
β’ (π₯ β π· β (ββ(logβπ₯)) β
β) |
16 | 12, 13 | logimcld 26072 |
. . . . . . 7
β’ (π₯ β π· β (-Ο <
(ββ(logβπ₯)) β§ (ββ(logβπ₯)) β€ Ο)) |
17 | 16 | simpld 496 |
. . . . . 6
β’ (π₯ β π· β -Ο <
(ββ(logβπ₯))) |
18 | | pire 25960 |
. . . . . . . 8
β’ Ο
β β |
19 | 18 | a1i 11 |
. . . . . . 7
β’ (π₯ β π· β Ο β
β) |
20 | 16 | simprd 497 |
. . . . . . 7
β’ (π₯ β π· β (ββ(logβπ₯)) β€ Ο) |
21 | 4 | logdmnrp 26141 |
. . . . . . . . 9
β’ (π₯ β π· β Β¬ -π₯ β β+) |
22 | | lognegb 26090 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π₯ β 0) β (-π₯ β β+
β (ββ(logβπ₯)) = Ο)) |
23 | 12, 13, 22 | syl2anc 585 |
. . . . . . . . . 10
β’ (π₯ β π· β (-π₯ β β+ β
(ββ(logβπ₯)) = Ο)) |
24 | 23 | necon3bbid 2979 |
. . . . . . . . 9
β’ (π₯ β π· β (Β¬ -π₯ β β+ β
(ββ(logβπ₯)) β Ο)) |
25 | 21, 24 | mpbid 231 |
. . . . . . . 8
β’ (π₯ β π· β (ββ(logβπ₯)) β Ο) |
26 | 25 | necomd 2997 |
. . . . . . 7
β’ (π₯ β π· β Ο β
(ββ(logβπ₯))) |
27 | 15, 19, 20, 26 | leneltd 11365 |
. . . . . 6
β’ (π₯ β π· β (ββ(logβπ₯)) < Ο) |
28 | 18 | renegcli 11518 |
. . . . . . . 8
β’ -Ο
β β |
29 | 28 | rexri 11269 |
. . . . . . 7
β’ -Ο
β β* |
30 | 18 | rexri 11269 |
. . . . . . 7
β’ Ο
β β* |
31 | | elioo2 13362 |
. . . . . . 7
β’ ((-Ο
β β* β§ Ο β β*) β
((ββ(logβπ₯)) β (-Ο(,)Ο) β
((ββ(logβπ₯)) β β β§ -Ο <
(ββ(logβπ₯)) β§ (ββ(logβπ₯)) < Ο))) |
32 | 29, 30, 31 | mp2an 691 |
. . . . . 6
β’
((ββ(logβπ₯)) β (-Ο(,)Ο) β
((ββ(logβπ₯)) β β β§ -Ο <
(ββ(logβπ₯)) β§ (ββ(logβπ₯)) < Ο)) |
33 | 15, 17, 27, 32 | syl3anbrc 1344 |
. . . . 5
β’ (π₯ β π· β (ββ(logβπ₯)) β
(-Ο(,)Ο)) |
34 | | imf 15057 |
. . . . . 6
β’
β:ββΆβ |
35 | | ffn 6715 |
. . . . . 6
β’
(β:ββΆβ β β Fn
β) |
36 | | elpreima 7057 |
. . . . . 6
β’ (β
Fn β β ((logβπ₯) β (β‘β β (-Ο(,)Ο)) β
((logβπ₯) β
β β§ (ββ(logβπ₯)) β (-Ο(,)Ο)))) |
37 | 34, 35, 36 | mp2b 10 |
. . . . 5
β’
((logβπ₯)
β (β‘β β
(-Ο(,)Ο)) β ((logβπ₯) β β β§
(ββ(logβπ₯)) β (-Ο(,)Ο))) |
38 | 14, 33, 37 | sylanbrc 584 |
. . . 4
β’ (π₯ β π· β (logβπ₯) β (β‘β β
(-Ο(,)Ο))) |
39 | 10, 38 | mprgbir 3069 |
. . 3
β’ (log
β π·) β (β‘β β
(-Ο(,)Ο)) |
40 | | df-ioo 13325 |
. . . . . . . . . 10
β’ (,) =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ < π¦)}) |
41 | | df-ioc 13326 |
. . . . . . . . . 10
β’ (,] =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ β€ π¦)}) |
42 | | idd 24 |
. . . . . . . . . 10
β’ ((-Ο
β β* β§ π€ β β*) β (-Ο
< π€ β -Ο <
π€)) |
43 | | xrltle 13125 |
. . . . . . . . . 10
β’ ((π€ β β*
β§ Ο β β*) β (π€ < Ο β π€ β€ Ο)) |
44 | 40, 41, 42, 43 | ixxssixx 13335 |
. . . . . . . . 9
β’
(-Ο(,)Ο) β (-Ο(,]Ο) |
45 | | imass2 6099 |
. . . . . . . . 9
β’
((-Ο(,)Ο) β (-Ο(,]Ο) β (β‘β β (-Ο(,)Ο)) β
(β‘β β
(-Ο(,]Ο))) |
46 | 44, 45 | ax-mp 5 |
. . . . . . . 8
β’ (β‘β β (-Ο(,)Ο)) β
(β‘β β
(-Ο(,]Ο)) |
47 | | logrn 26059 |
. . . . . . . 8
β’ ran log =
(β‘β β
(-Ο(,]Ο)) |
48 | 46, 47 | sseqtrri 4019 |
. . . . . . 7
β’ (β‘β β (-Ο(,)Ο)) β ran
log |
49 | 48 | sseli 3978 |
. . . . . 6
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β π₯ β ran
log) |
50 | | logef 26082 |
. . . . . 6
β’ (π₯ β ran log β
(logβ(expβπ₯)) =
π₯) |
51 | 49, 50 | syl 17 |
. . . . 5
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(logβ(expβπ₯)) =
π₯) |
52 | | elpreima 7057 |
. . . . . . . . . 10
β’ (β
Fn β β (π₯ β
(β‘β β (-Ο(,)Ο))
β (π₯ β β
β§ (ββπ₯)
β (-Ο(,)Ο)))) |
53 | 34, 35, 52 | mp2b 10 |
. . . . . . . . 9
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο))) |
54 | | efcl 16023 |
. . . . . . . . . 10
β’ (π₯ β β β
(expβπ₯) β
β) |
55 | 54 | adantr 482 |
. . . . . . . . 9
β’ ((π₯ β β β§
(ββπ₯) β
(-Ο(,)Ο)) β (expβπ₯) β β) |
56 | 53, 55 | sylbi 216 |
. . . . . . . 8
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(expβπ₯) β
β) |
57 | 53 | simplbi 499 |
. . . . . . . . . . 11
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β π₯ β
β) |
58 | 57 | imcld 15139 |
. . . . . . . . . 10
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(ββπ₯) β
β) |
59 | | eliooord 13380 |
. . . . . . . . . . . 12
β’
((ββπ₯)
β (-Ο(,)Ο) β (-Ο < (ββπ₯) β§ (ββπ₯) < Ο)) |
60 | 53, 59 | simplbiim 506 |
. . . . . . . . . . 11
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(-Ο < (ββπ₯) β§ (ββπ₯) < Ο)) |
61 | 60 | simprd 497 |
. . . . . . . . . 10
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(ββπ₯) <
Ο) |
62 | 58, 61 | ltned 11347 |
. . . . . . . . 9
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(ββπ₯) β
Ο) |
63 | 51 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β (logβ(expβπ₯)) = π₯) |
64 | 63 | fveq2d 6893 |
. . . . . . . . . . . 12
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β (ββ(logβ(expβπ₯))) = (ββπ₯)) |
65 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β (expβπ₯) β (-β(,]0)) |
66 | | mnfxr 11268 |
. . . . . . . . . . . . . . . . 17
β’ -β
β β* |
67 | | 0re 11213 |
. . . . . . . . . . . . . . . . 17
β’ 0 β
β |
68 | | elioc2 13384 |
. . . . . . . . . . . . . . . . 17
β’
((-β β β* β§ 0 β β) β
((expβπ₯) β
(-β(,]0) β ((expβπ₯) β β β§ -β <
(expβπ₯) β§
(expβπ₯) β€
0))) |
69 | 66, 67, 68 | mp2an 691 |
. . . . . . . . . . . . . . . 16
β’
((expβπ₯)
β (-β(,]0) β ((expβπ₯) β β β§ -β <
(expβπ₯) β§
(expβπ₯) β€
0)) |
70 | 65, 69 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β ((expβπ₯) β β β§ -β <
(expβπ₯) β§
(expβπ₯) β€
0)) |
71 | 70 | simp1d 1143 |
. . . . . . . . . . . . . 14
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β (expβπ₯) β β) |
72 | | 0red 11214 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β 0 β β) |
73 | 70 | simp3d 1145 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β (expβπ₯) β€ 0) |
74 | | efne0 16037 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β
(expβπ₯) β
0) |
75 | 57, 74 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(expβπ₯) β
0) |
76 | 75 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β (expβπ₯) β 0) |
77 | 76 | necomd 2997 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β 0 β (expβπ₯)) |
78 | 71, 72, 73, 77 | leneltd 11365 |
. . . . . . . . . . . . . 14
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β (expβπ₯) < 0) |
79 | 71, 78 | negelrpd 13005 |
. . . . . . . . . . . . 13
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β -(expβπ₯) β
β+) |
80 | | lognegb 26090 |
. . . . . . . . . . . . . . 15
β’
(((expβπ₯)
β β β§ (expβπ₯) β 0) β (-(expβπ₯) β β+
β (ββ(logβ(expβπ₯))) = Ο)) |
81 | 56, 75, 80 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(-(expβπ₯) β
β+ β (ββ(logβ(expβπ₯))) = Ο)) |
82 | 81 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β (-(expβπ₯) β β+ β
(ββ(logβ(expβπ₯))) = Ο)) |
83 | 79, 82 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β (ββ(logβ(expβπ₯))) = Ο) |
84 | 64, 83 | eqtr3d 2775 |
. . . . . . . . . . 11
β’ ((π₯ β (β‘β β (-Ο(,)Ο)) β§
(expβπ₯) β
(-β(,]0)) β (ββπ₯) = Ο) |
85 | 84 | ex 414 |
. . . . . . . . . 10
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
((expβπ₯) β
(-β(,]0) β (ββπ₯) = Ο)) |
86 | 85 | necon3ad 2954 |
. . . . . . . . 9
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
((ββπ₯) β
Ο β Β¬ (expβπ₯) β (-β(,]0))) |
87 | 62, 86 | mpd 15 |
. . . . . . . 8
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β Β¬
(expβπ₯) β
(-β(,]0)) |
88 | 56, 87 | eldifd 3959 |
. . . . . . 7
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(expβπ₯) β
(β β (-β(,]0))) |
89 | 88, 4 | eleqtrrdi 2845 |
. . . . . 6
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(expβπ₯) β π·) |
90 | | funfvima2 7230 |
. . . . . . 7
β’ ((Fun log
β§ π· β dom log)
β ((expβπ₯)
β π· β
(logβ(expβπ₯))
β (log β π·))) |
91 | 3, 8, 90 | mp2an 691 |
. . . . . 6
β’
((expβπ₯)
β π· β
(logβ(expβπ₯))
β (log β π·)) |
92 | 89, 91 | syl 17 |
. . . . 5
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β
(logβ(expβπ₯))
β (log β π·)) |
93 | 51, 92 | eqeltrrd 2835 |
. . . 4
β’ (π₯ β (β‘β β (-Ο(,)Ο)) β π₯ β (log β π·)) |
94 | 93 | ssriv 3986 |
. . 3
β’ (β‘β β (-Ο(,)Ο)) β (log
β π·) |
95 | 39, 94 | eqssi 3998 |
. 2
β’ (log
β π·) = (β‘β β
(-Ο(,)Ο)) |
96 | | imcncf 24411 |
. . . 4
β’ β
β (ββcnββ) |
97 | | ssid 4004 |
. . . . 5
β’ β
β β |
98 | | ax-resscn 11164 |
. . . . 5
β’ β
β β |
99 | | eqid 2733 |
. . . . . 6
β’
(TopOpenββfld) =
(TopOpenββfld) |
100 | 99 | cnfldtopon 24291 |
. . . . . . 7
β’
(TopOpenββfld) β
(TopOnββ) |
101 | 100 | toponrestid 22415 |
. . . . . 6
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
102 | 99 | tgioo2 24311 |
. . . . . 6
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
103 | 99, 101, 102 | cncfcn 24418 |
. . . . 5
β’ ((β
β β β§ β β β) β (ββcnββ) =
((TopOpenββfld) Cn (topGenβran
(,)))) |
104 | 97, 98, 103 | mp2an 691 |
. . . 4
β’
(ββcnββ) =
((TopOpenββfld) Cn (topGenβran
(,))) |
105 | 96, 104 | eleqtri 2832 |
. . 3
β’ β
β ((TopOpenββfld) Cn (topGenβran
(,))) |
106 | | iooretop 24274 |
. . 3
β’
(-Ο(,)Ο) β (topGenβran (,)) |
107 | | cnima 22761 |
. . 3
β’ ((β
β ((TopOpenββfld) Cn (topGenβran (,))) β§
(-Ο(,)Ο) β (topGenβran (,))) β (β‘β β (-Ο(,)Ο)) β
(TopOpenββfld)) |
108 | 105, 106,
107 | mp2an 691 |
. 2
β’ (β‘β β (-Ο(,)Ο)) β
(TopOpenββfld) |
109 | 95, 108 | eqeltri 2830 |
1
β’ (log
β π·) β
(TopOpenββfld) |