Metamath Proof Explorer

Theorem logleb

Description: Natural logarithm preserves <_ . (Contributed by Stefan O'Rear, 19-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 logltb 
 |-  ( ( B e. RR+ /\ A e. RR+ ) -> ( B < A <-> ( log ` B ) < ( log ` A ) ) )
2 1 ancoms 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( B < A <-> ( log ` B ) < ( log ` A ) ) )
3 2 notbid 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( -. B < A <-> -. ( log ` B ) < ( log ` A ) ) )
4 rpre 
 |-  ( A e. RR+ -> A e. RR )
5 rpre 
 |-  ( B e. RR+ -> B e. RR )
6 lenlt 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
7 4 5 6 syl2an 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( A <_ B <-> -. B < A ) )
8 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
9 relogcl 
 |-  ( B e. RR+ -> ( log ` B ) e. RR )
10 lenlt 
 |-  ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR ) -> ( ( log ` A ) <_ ( log ` B ) <-> -. ( log ` B ) < ( log ` A ) ) )
11 8 9 10 syl2an 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( ( log ` A ) <_ ( log ` B ) <-> -. ( log ` B ) < ( log ` A ) ) )
12 3 7 11 3bitr4d 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( A <_ B <-> ( log ` A ) <_ ( log ` B ) ) )