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 ) ) )