Metamath Proof Explorer


Theorem reglogleb

Description: General logarithm preserves <_ . (Contributed by Stefan O'Rear, 19-Oct-2014) (New usage is discouraged.) Use logbleb instead.

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

Proof

Step Hyp Ref Expression
1 logleb
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( A <_ B <-> ( log ` A ) <_ ( log ` B ) ) )
2 1 adantr
 |-  ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( A <_ B <-> ( log ` A ) <_ ( log ` B ) ) )
3 relogcl
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
4 3 ad2antrr
 |-  ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( log ` A ) e. RR )
5 relogcl
 |-  ( B e. RR+ -> ( log ` B ) e. RR )
6 5 ad2antlr
 |-  ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( log ` B ) e. RR )
7 relogcl
 |-  ( C e. RR+ -> ( log ` C ) e. RR )
8 7 ad2antrl
 |-  ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( log ` C ) e. RR )
9 log1
 |-  ( log ` 1 ) = 0
10 1rp
 |-  1 e. RR+
11 logltb
 |-  ( ( 1 e. RR+ /\ C e. RR+ ) -> ( 1 < C <-> ( log ` 1 ) < ( log ` C ) ) )
12 10 11 mpan
 |-  ( C e. RR+ -> ( 1 < C <-> ( log ` 1 ) < ( log ` C ) ) )
13 12 biimpa
 |-  ( ( C e. RR+ /\ 1 < C ) -> ( log ` 1 ) < ( log ` C ) )
14 9 13 eqbrtrrid
 |-  ( ( C e. RR+ /\ 1 < C ) -> 0 < ( log ` C ) )
15 14 adantl
 |-  ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> 0 < ( log ` C ) )
16 lediv1
 |-  ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR /\ ( ( log ` C ) e. RR /\ 0 < ( log ` C ) ) ) -> ( ( log ` A ) <_ ( log ` B ) <-> ( ( log ` A ) / ( log ` C ) ) <_ ( ( log ` B ) / ( log ` C ) ) ) )
17 4 6 8 15 16 syl112anc
 |-  ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( ( log ` A ) <_ ( log ` B ) <-> ( ( log ` A ) / ( log ` C ) ) <_ ( ( log ` B ) / ( log ` C ) ) ) )
18 2 17 bitrd
 |-  ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( A <_ B <-> ( ( log ` A ) / ( log ` C ) ) <_ ( ( log ` B ) / ( log ` C ) ) ) )