Metamath Proof Explorer

Theorem logltb

Description: The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007)

Ref Expression
Assertion logltb 
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( log ` A ) < ( log ` B ) ) )

Proof

Step Hyp Ref Expression
1 relogiso 
 |-  ( log |` RR+ ) Isom < , < ( RR+ , RR )
2 df-isom 
 |-  ( ( log |` RR+ ) Isom < , < ( RR+ , RR ) <-> ( ( log |` RR+ ) : RR+ -1-1-onto-> RR /\ A. x e. RR+ A. y e. RR+ ( x < y <-> ( ( log |` RR+ ) ` x ) < ( ( log |` RR+ ) ` y ) ) ) )
3 1 2 mpbi 
 |-  ( ( log |` RR+ ) : RR+ -1-1-onto-> RR /\ A. x e. RR+ A. y e. RR+ ( x < y <-> ( ( log |` RR+ ) ` x ) < ( ( log |` RR+ ) ` y ) ) )
4 3 simpri 
 |-  A. x e. RR+ A. y e. RR+ ( x < y <-> ( ( log |` RR+ ) ` x ) < ( ( log |` RR+ ) ` y ) )
5 breq1 
 |-  ( x = A -> ( x < y <-> A < y ) )
6 fveq2 
 |-  ( x = A -> ( ( log |` RR+ ) ` x ) = ( ( log |` RR+ ) ` A ) )
7 6 breq1d 
 |-  ( x = A -> ( ( ( log |` RR+ ) ` x ) < ( ( log |` RR+ ) ` y ) <-> ( ( log |` RR+ ) ` A ) < ( ( log |` RR+ ) ` y ) ) )
8 5 7 bibi12d 
 |-  ( x = A -> ( ( x < y <-> ( ( log |` RR+ ) ` x ) < ( ( log |` RR+ ) ` y ) ) <-> ( A < y <-> ( ( log |` RR+ ) ` A ) < ( ( log |` RR+ ) ` y ) ) ) )
9 breq2 
 |-  ( y = B -> ( A < y <-> A < B ) )
10 fveq2 
 |-  ( y = B -> ( ( log |` RR+ ) ` y ) = ( ( log |` RR+ ) ` B ) )
11 10 breq2d 
 |-  ( y = B -> ( ( ( log |` RR+ ) ` A ) < ( ( log |` RR+ ) ` y ) <-> ( ( log |` RR+ ) ` A ) < ( ( log |` RR+ ) ` B ) ) )
12 9 11 bibi12d 
 |-  ( y = B -> ( ( A < y <-> ( ( log |` RR+ ) ` A ) < ( ( log |` RR+ ) ` y ) ) <-> ( A < B <-> ( ( log |` RR+ ) ` A ) < ( ( log |` RR+ ) ` B ) ) ) )
13 8 12 rspc2v 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( A. x e. RR+ A. y e. RR+ ( x < y <-> ( ( log |` RR+ ) ` x ) < ( ( log |` RR+ ) ` y ) ) -> ( A < B <-> ( ( log |` RR+ ) ` A ) < ( ( log |` RR+ ) ` B ) ) ) )
14 4 13 mpi 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( ( log |` RR+ ) ` A ) < ( ( log |` RR+ ) ` B ) ) )
15 fvres 
 |-  ( A e. RR+ -> ( ( log |` RR+ ) ` A ) = ( log ` A ) )
16 fvres 
 |-  ( B e. RR+ -> ( ( log |` RR+ ) ` B ) = ( log ` B ) )
17 15 16 breqan12d 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( ( ( log |` RR+ ) ` A ) < ( ( log |` RR+ ) ` B ) <-> ( log ` A ) < ( log ` B ) ) )
18 14 17 bitrd 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( log ` A ) < ( log ` B ) ) )