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 )