Metamath Proof Explorer


Theorem relogcn

Description: The real logarithm function is continuous. (Contributed by Mario Carneiro, 17-Feb-2015)

Ref Expression
Assertion relogcn
|- ( log |` RR+ ) e. ( RR+ -cn-> RR )

Proof

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 )