Metamath Proof Explorer


Theorem logbleb

Description: The general logarithm function is monotone/increasing. See logleb . (Contributed by Stefan O'Rear, 19-Oct-2014) (Revised by AV, 31-May-2020)

Ref Expression
Assertion logbleb
|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( X <_ Y <-> ( B logb X ) <_ ( B logb Y ) ) )

Proof

Step Hyp Ref Expression
1 simp2
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> X e. RR+ )
2 1 relogcld
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( log ` X ) e. RR )
3 simp3
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> Y e. RR+ )
4 3 relogcld
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( log ` Y ) e. RR )
5 eluzelre
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. RR )
6 5 3ad2ant1
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> B e. RR )
7 1z
 |-  1 e. ZZ
8 simp1
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> B e. ( ZZ>= ` 2 ) )
9 1p1e2
 |-  ( 1 + 1 ) = 2
10 9 fveq2i
 |-  ( ZZ>= ` ( 1 + 1 ) ) = ( ZZ>= ` 2 )
11 8 10 eleqtrrdi
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> B e. ( ZZ>= ` ( 1 + 1 ) ) )
12 eluzp1l
 |-  ( ( 1 e. ZZ /\ B e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 1 < B )
13 7 11 12 sylancr
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> 1 < B )
14 6 13 rplogcld
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( log ` B ) e. RR+ )
15 2 4 14 lediv1d
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( ( log ` X ) <_ ( log ` Y ) <-> ( ( log ` X ) / ( log ` B ) ) <_ ( ( log ` Y ) / ( log ` B ) ) ) )
16 logleb
 |-  ( ( X e. RR+ /\ Y e. RR+ ) -> ( X <_ Y <-> ( log ` X ) <_ ( log ` Y ) ) )
17 16 3adant1
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( X <_ Y <-> ( log ` X ) <_ ( log ` Y ) ) )
18 relogbval
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
19 18 3adant3
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
20 relogbval
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ Y e. RR+ ) -> ( B logb Y ) = ( ( log ` Y ) / ( log ` B ) ) )
21 20 3adant2
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( B logb Y ) = ( ( log ` Y ) / ( log ` B ) ) )
22 19 21 breq12d
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( ( B logb X ) <_ ( B logb Y ) <-> ( ( log ` X ) / ( log ` B ) ) <_ ( ( log ` Y ) / ( log ` B ) ) ) )
23 15 17 22 3bitr4d
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( X <_ Y <-> ( B logb X ) <_ ( B logb Y ) ) )