Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
(TopOpenββfld) =
(TopOpenββfld) |
2 | 1 | cnfldtopon 24291 |
. . . . 5
β’
(TopOpenββfld) β
(TopOnββ) |
3 | 2 | toponrestid 22415 |
. . . 4
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
4 | | cnelprrecn 11200 |
. . . . 5
β’ β
β {β, β} |
5 | 4 | a1i 11 |
. . . 4
β’ (β€
β β β {β, β}) |
6 | | logcn.d |
. . . . . 6
β’ π· = (β β
(-β(,]0)) |
7 | 6 | logdmopn 26149 |
. . . . 5
β’ π· β
(TopOpenββfld) |
8 | 7 | a1i 11 |
. . . 4
β’ (β€
β π· β
(TopOpenββfld)) |
9 | | logf1o 26065 |
. . . . . . . . 9
β’
log:(β β {0})β1-1-ontoβran
log |
10 | | f1of1 6830 |
. . . . . . . . 9
β’
(log:(β β {0})β1-1-ontoβran
log β log:(β β {0})β1-1βran log) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . 8
β’
log:(β β {0})β1-1βran log |
12 | 6 | logdmss 26142 |
. . . . . . . 8
β’ π· β (β β
{0}) |
13 | | f1ores 6845 |
. . . . . . . 8
β’
((log:(β β {0})β1-1βran log β§ π· β (β β {0})) β (log
βΎ π·):π·β1-1-ontoβ(log
β π·)) |
14 | 11, 12, 13 | mp2an 691 |
. . . . . . 7
β’ (log
βΎ π·):π·β1-1-ontoβ(log
β π·) |
15 | | f1ocnv 6843 |
. . . . . . 7
β’ ((log
βΎ π·):π·β1-1-ontoβ(log
β π·) β β‘(log βΎ π·):(log β π·)β1-1-ontoβπ·) |
16 | 14, 15 | ax-mp 5 |
. . . . . 6
β’ β‘(log βΎ π·):(log β π·)β1-1-ontoβπ· |
17 | | df-log 26057 |
. . . . . . . . . . 11
β’ log =
β‘(exp βΎ (β‘β β
(-Ο(,]Ο))) |
18 | 17 | reseq1i 5976 |
. . . . . . . . . 10
β’ (log
βΎ π·) = (β‘(exp βΎ (β‘β β (-Ο(,]Ο))) βΎ
π·) |
19 | 18 | cnveqi 5873 |
. . . . . . . . 9
β’ β‘(log βΎ π·) = β‘(β‘(exp βΎ (β‘β β (-Ο(,]Ο))) βΎ
π·) |
20 | | eff 16022 |
. . . . . . . . . . 11
β’
exp:ββΆβ |
21 | | cnvimass 6078 |
. . . . . . . . . . . 12
β’ (β‘β β (-Ο(,]Ο)) β dom
β |
22 | | imf 15057 |
. . . . . . . . . . . . 13
β’
β:ββΆβ |
23 | 22 | fdmi 6727 |
. . . . . . . . . . . 12
β’ dom
β = β |
24 | 21, 23 | sseqtri 4018 |
. . . . . . . . . . 11
β’ (β‘β β (-Ο(,]Ο)) β
β |
25 | | fssres 6755 |
. . . . . . . . . . 11
β’
((exp:ββΆβ β§ (β‘β β (-Ο(,]Ο)) β
β) β (exp βΎ (β‘β
β (-Ο(,]Ο))):(β‘β
β (-Ο(,]Ο))βΆβ) |
26 | 20, 24, 25 | mp2an 691 |
. . . . . . . . . 10
β’ (exp
βΎ (β‘β β
(-Ο(,]Ο))):(β‘β β
(-Ο(,]Ο))βΆβ |
27 | | ffun 6718 |
. . . . . . . . . 10
β’ ((exp
βΎ (β‘β β
(-Ο(,]Ο))):(β‘β β
(-Ο(,]Ο))βΆβ β Fun (exp βΎ (β‘β β
(-Ο(,]Ο)))) |
28 | | funcnvres2 6626 |
. . . . . . . . . 10
β’ (Fun (exp
βΎ (β‘β β
(-Ο(,]Ο))) β β‘(β‘(exp βΎ (β‘β β (-Ο(,]Ο))) βΎ
π·) = ((exp βΎ (β‘β β (-Ο(,]Ο))) βΎ
(β‘(exp βΎ (β‘β β (-Ο(,]Ο))) β
π·))) |
29 | 26, 27, 28 | mp2b 10 |
. . . . . . . . 9
β’ β‘(β‘(exp βΎ (β‘β β (-Ο(,]Ο))) βΎ
π·) = ((exp βΎ (β‘β β (-Ο(,]Ο))) βΎ
(β‘(exp βΎ (β‘β β (-Ο(,]Ο))) β
π·)) |
30 | | cnvimass 6078 |
. . . . . . . . . . 11
β’ (β‘(exp βΎ (β‘β β (-Ο(,]Ο))) β
π·) β dom (exp βΎ
(β‘β β
(-Ο(,]Ο))) |
31 | 26 | fdmi 6727 |
. . . . . . . . . . 11
β’ dom (exp
βΎ (β‘β β
(-Ο(,]Ο))) = (β‘β β
(-Ο(,]Ο)) |
32 | 30, 31 | sseqtri 4018 |
. . . . . . . . . 10
β’ (β‘(exp βΎ (β‘β β (-Ο(,]Ο))) β
π·) β (β‘β β
(-Ο(,]Ο)) |
33 | | resabs1 6010 |
. . . . . . . . . 10
β’ ((β‘(exp βΎ (β‘β β (-Ο(,]Ο))) β
π·) β (β‘β β (-Ο(,]Ο)) β ((exp
βΎ (β‘β β
(-Ο(,]Ο))) βΎ (β‘(exp βΎ
(β‘β β (-Ο(,]Ο)))
β π·)) = (exp βΎ
(β‘(exp βΎ (β‘β β (-Ο(,]Ο))) β
π·))) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . . 9
β’ ((exp
βΎ (β‘β β
(-Ο(,]Ο))) βΎ (β‘(exp βΎ
(β‘β β (-Ο(,]Ο)))
β π·)) = (exp βΎ
(β‘(exp βΎ (β‘β β (-Ο(,]Ο))) β
π·)) |
35 | 19, 29, 34 | 3eqtri 2765 |
. . . . . . . 8
β’ β‘(log βΎ π·) = (exp βΎ (β‘(exp βΎ (β‘β β (-Ο(,]Ο))) β
π·)) |
36 | 17 | imaeq1i 6055 |
. . . . . . . . 9
β’ (log
β π·) = (β‘(exp βΎ (β‘β β (-Ο(,]Ο))) β
π·) |
37 | 36 | reseq2i 5977 |
. . . . . . . 8
β’ (exp
βΎ (log β π·)) =
(exp βΎ (β‘(exp βΎ (β‘β β (-Ο(,]Ο))) β
π·)) |
38 | 35, 37 | eqtr4i 2764 |
. . . . . . 7
β’ β‘(log βΎ π·) = (exp βΎ (log β π·)) |
39 | | f1oeq1 6819 |
. . . . . . 7
β’ (β‘(log βΎ π·) = (exp βΎ (log β π·)) β (β‘(log βΎ π·):(log β π·)β1-1-ontoβπ· β (exp βΎ (log
β π·)):(log β
π·)β1-1-ontoβπ·)) |
40 | 38, 39 | ax-mp 5 |
. . . . . 6
β’ (β‘(log βΎ π·):(log β π·)β1-1-ontoβπ· β (exp βΎ (log
β π·)):(log β
π·)β1-1-ontoβπ·) |
41 | 16, 40 | mpbi 229 |
. . . . 5
β’ (exp
βΎ (log β π·)):(log β π·)β1-1-ontoβπ· |
42 | 41 | a1i 11 |
. . . 4
β’ (β€
β (exp βΎ (log β π·)):(log β π·)β1-1-ontoβπ·) |
43 | 38 | cnveqi 5873 |
. . . . . 6
β’ β‘β‘(log βΎ π·) = β‘(exp βΎ (log β π·)) |
44 | | relres 6009 |
. . . . . . 7
β’ Rel (log
βΎ π·) |
45 | | dfrel2 6186 |
. . . . . . 7
β’ (Rel (log
βΎ π·) β β‘β‘(log βΎ π·) = (log βΎ π·)) |
46 | 44, 45 | mpbi 229 |
. . . . . 6
β’ β‘β‘(log βΎ π·) = (log βΎ π·) |
47 | 43, 46 | eqtr3i 2763 |
. . . . 5
β’ β‘(exp βΎ (log β π·)) = (log βΎ π·) |
48 | | f1of 6831 |
. . . . . . 7
β’ ((log
βΎ π·):π·β1-1-ontoβ(log
β π·) β (log
βΎ π·):π·βΆ(log β π·)) |
49 | 14, 48 | mp1i 13 |
. . . . . 6
β’ (β€
β (log βΎ π·):π·βΆ(log β π·)) |
50 | | imassrn 6069 |
. . . . . . . 8
β’ (log
β π·) β ran
log |
51 | | logrncn 26063 |
. . . . . . . . 9
β’ (π₯ β ran log β π₯ β
β) |
52 | 51 | ssriv 3986 |
. . . . . . . 8
β’ ran log
β β |
53 | 50, 52 | sstri 3991 |
. . . . . . 7
β’ (log
β π·) β
β |
54 | 6 | logcn 26147 |
. . . . . . 7
β’ (log
βΎ π·) β (π·βcnββ) |
55 | | cncfcdm 24406 |
. . . . . . 7
β’ (((log
β π·) β β
β§ (log βΎ π·)
β (π·βcnββ)) β ((log βΎ π·) β (π·βcnβ(log β π·)) β (log βΎ π·):π·βΆ(log β π·))) |
56 | 53, 54, 55 | mp2an 691 |
. . . . . 6
β’ ((log
βΎ π·) β (π·βcnβ(log β π·)) β (log βΎ π·):π·βΆ(log β π·)) |
57 | 49, 56 | sylibr 233 |
. . . . 5
β’ (β€
β (log βΎ π·)
β (π·βcnβ(log β π·))) |
58 | 47, 57 | eqeltrid 2838 |
. . . 4
β’ (β€
β β‘(exp βΎ (log β π·)) β (π·βcnβ(log β π·))) |
59 | | ssid 4004 |
. . . . . . . . 9
β’ β
β β |
60 | 1, 3 | dvres 25420 |
. . . . . . . . 9
β’
(((β β β β§ exp:ββΆβ) β§
(β β β β§ (log β π·) β β)) β (β D (exp
βΎ (log β π·))) =
((β D exp) βΎ
((intβ(TopOpenββfld))β(log β π·)))) |
61 | 59, 20, 59, 53, 60 | mp4an 692 |
. . . . . . . 8
β’ (β
D (exp βΎ (log β π·))) = ((β D exp) βΎ
((intβ(TopOpenββfld))β(log β π·))) |
62 | | dvef 25489 |
. . . . . . . . 9
β’ (β
D exp) = exp |
63 | 1 | cnfldtop 24292 |
. . . . . . . . . 10
β’
(TopOpenββfld) β Top |
64 | 6 | dvloglem 26148 |
. . . . . . . . . 10
β’ (log
β π·) β
(TopOpenββfld) |
65 | | isopn3i 22578 |
. . . . . . . . . 10
β’
(((TopOpenββfld) β Top β§ (log β
π·) β
(TopOpenββfld)) β
((intβ(TopOpenββfld))β(log β π·)) = (log β π·)) |
66 | 63, 64, 65 | mp2an 691 |
. . . . . . . . 9
β’
((intβ(TopOpenββfld))β(log β
π·)) = (log β π·) |
67 | 62, 66 | reseq12i 5978 |
. . . . . . . 8
β’ ((β
D exp) βΎ ((intβ(TopOpenββfld))β(log
β π·))) = (exp βΎ
(log β π·)) |
68 | 61, 67 | eqtri 2761 |
. . . . . . 7
β’ (β
D (exp βΎ (log β π·))) = (exp βΎ (log β π·)) |
69 | 68 | dmeqi 5903 |
. . . . . 6
β’ dom
(β D (exp βΎ (log β π·))) = dom (exp βΎ (log β π·)) |
70 | | dmres 6002 |
. . . . . 6
β’ dom (exp
βΎ (log β π·)) =
((log β π·) β© dom
exp) |
71 | 20 | fdmi 6727 |
. . . . . . . 8
β’ dom exp =
β |
72 | 53, 71 | sseqtrri 4019 |
. . . . . . 7
β’ (log
β π·) β dom
exp |
73 | | df-ss 3965 |
. . . . . . 7
β’ ((log
β π·) β dom exp
β ((log β π·)
β© dom exp) = (log β π·)) |
74 | 72, 73 | mpbi 229 |
. . . . . 6
β’ ((log
β π·) β© dom exp) =
(log β π·) |
75 | 69, 70, 74 | 3eqtri 2765 |
. . . . 5
β’ dom
(β D (exp βΎ (log β π·))) = (log β π·) |
76 | 75 | a1i 11 |
. . . 4
β’ (β€
β dom (β D (exp βΎ (log β π·))) = (log β π·)) |
77 | | neirr 2950 |
. . . . . 6
β’ Β¬ 0
β 0 |
78 | | resss 6005 |
. . . . . . . . . . . . 13
β’ ((β
D exp) βΎ ((intβ(TopOpenββfld))β(log
β π·))) β
(β D exp) |
79 | 61, 78 | eqsstri 4016 |
. . . . . . . . . . . 12
β’ (β
D (exp βΎ (log β π·))) β (β D exp) |
80 | 79, 62 | sseqtri 4018 |
. . . . . . . . . . 11
β’ (β
D (exp βΎ (log β π·))) β exp |
81 | 80 | rnssi 5938 |
. . . . . . . . . 10
β’ ran
(β D (exp βΎ (log β π·))) β ran exp |
82 | | eff2 16039 |
. . . . . . . . . . 11
β’
exp:ββΆ(β β {0}) |
83 | | frn 6722 |
. . . . . . . . . . 11
β’
(exp:ββΆ(β β {0}) β ran exp β
(β β {0})) |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . . 10
β’ ran exp
β (β β {0}) |
85 | 81, 84 | sstri 3991 |
. . . . . . . . 9
β’ ran
(β D (exp βΎ (log β π·))) β (β β
{0}) |
86 | 85 | sseli 3978 |
. . . . . . . 8
β’ (0 β
ran (β D (exp βΎ (log β π·))) β 0 β (β β
{0})) |
87 | | eldifsn 4790 |
. . . . . . . 8
β’ (0 β
(β β {0}) β (0 β β β§ 0 β
0)) |
88 | 86, 87 | sylib 217 |
. . . . . . 7
β’ (0 β
ran (β D (exp βΎ (log β π·))) β (0 β β β§ 0 β
0)) |
89 | 88 | simprd 497 |
. . . . . 6
β’ (0 β
ran (β D (exp βΎ (log β π·))) β 0 β 0) |
90 | 77, 89 | mto 196 |
. . . . 5
β’ Β¬ 0
β ran (β D (exp βΎ (log β π·))) |
91 | 90 | a1i 11 |
. . . 4
β’ (β€
β Β¬ 0 β ran (β D (exp βΎ (log β π·)))) |
92 | 1, 3, 5, 8, 42, 58, 76, 91 | dvcnv 25486 |
. . 3
β’ (β€
β (β D β‘(exp βΎ (log
β π·))) = (π₯ β π· β¦ (1 / ((β D (exp βΎ (log
β π·)))β(β‘(exp βΎ (log β π·))βπ₯))))) |
93 | 92 | mptru 1549 |
. 2
β’ (β
D β‘(exp βΎ (log β π·))) = (π₯ β π· β¦ (1 / ((β D (exp βΎ (log
β π·)))β(β‘(exp βΎ (log β π·))βπ₯)))) |
94 | 47 | oveq2i 7417 |
. 2
β’ (β
D β‘(exp βΎ (log β π·))) = (β D (log βΎ
π·)) |
95 | 68 | fveq1i 6890 |
. . . . 5
β’ ((β
D (exp βΎ (log β π·)))β(β‘(exp βΎ (log β π·))βπ₯)) = ((exp βΎ (log β π·))β(β‘(exp βΎ (log β π·))βπ₯)) |
96 | | f1ocnvfv2 7272 |
. . . . . 6
β’ (((exp
βΎ (log β π·)):(log β π·)β1-1-ontoβπ· β§ π₯ β π·) β ((exp βΎ (log β π·))β(β‘(exp βΎ (log β π·))βπ₯)) = π₯) |
97 | 41, 96 | mpan 689 |
. . . . 5
β’ (π₯ β π· β ((exp βΎ (log β π·))β(β‘(exp βΎ (log β π·))βπ₯)) = π₯) |
98 | 95, 97 | eqtrid 2785 |
. . . 4
β’ (π₯ β π· β ((β D (exp βΎ (log
β π·)))β(β‘(exp βΎ (log β π·))βπ₯)) = π₯) |
99 | 98 | oveq2d 7422 |
. . 3
β’ (π₯ β π· β (1 / ((β D (exp βΎ (log
β π·)))β(β‘(exp βΎ (log β π·))βπ₯))) = (1 / π₯)) |
100 | 99 | mpteq2ia 5251 |
. 2
β’ (π₯ β π· β¦ (1 / ((β D (exp βΎ (log
β π·)))β(β‘(exp βΎ (log β π·))βπ₯)))) = (π₯ β π· β¦ (1 / π₯)) |
101 | 93, 94, 100 | 3eqtr3i 2769 |
1
β’ (β
D (log βΎ π·)) = (π₯ β π· β¦ (1 / π₯)) |