Step |
Hyp |
Ref |
Expression |
1 |
|
relogf1o |
|- ( log |` RR+ ) : RR+ -1-1-onto-> RR |
2 |
|
f1of |
|- ( ( log |` RR+ ) : RR+ -1-1-onto-> RR -> ( log |` RR+ ) : RR+ --> RR ) |
3 |
1 2
|
ax-mp |
|- ( log |` RR+ ) : RR+ --> RR |
4 |
|
ax-resscn |
|- RR C_ CC |
5 |
|
fss |
|- ( ( ( log |` RR+ ) : RR+ --> RR /\ RR C_ CC ) -> ( log |` RR+ ) : RR+ --> CC ) |
6 |
3 4 5
|
mp2an |
|- ( log |` RR+ ) : RR+ --> CC |
7 |
|
rpssre |
|- RR+ C_ RR |
8 |
|
ovex |
|- ( 1 / x ) e. _V |
9 |
|
dvrelog |
|- ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) ) |
10 |
8 9
|
dmmpti |
|- dom ( RR _D ( log |` RR+ ) ) = RR+ |
11 |
|
dvcn |
|- ( ( ( RR C_ CC /\ ( log |` RR+ ) : RR+ --> CC /\ RR+ C_ RR ) /\ dom ( RR _D ( log |` RR+ ) ) = RR+ ) -> ( log |` RR+ ) e. ( RR+ -cn-> CC ) ) |
12 |
10 11
|
mpan2 |
|- ( ( RR C_ CC /\ ( log |` RR+ ) : RR+ --> CC /\ RR+ C_ RR ) -> ( log |` RR+ ) e. ( RR+ -cn-> CC ) ) |
13 |
4 6 7 12
|
mp3an |
|- ( log |` RR+ ) e. ( RR+ -cn-> CC ) |
14 |
|
cncffvrn |
|- ( ( RR C_ CC /\ ( log |` RR+ ) e. ( RR+ -cn-> CC ) ) -> ( ( log |` RR+ ) e. ( RR+ -cn-> RR ) <-> ( log |` RR+ ) : RR+ --> RR ) ) |
15 |
4 13 14
|
mp2an |
|- ( ( log |` RR+ ) e. ( RR+ -cn-> RR ) <-> ( log |` RR+ ) : RR+ --> RR ) |
16 |
3 15
|
mpbir |
|- ( log |` RR+ ) e. ( RR+ -cn-> RR ) |