This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem logblt

Description: The general logarithm function is strictly monotone/increasing. Property 2 of Cohen4 p. 377. See logltb . (Contributed by Stefan O'Rear, 19-Oct-2014) (Revised by Thierry Arnoux, 27-Sep-2017)

Ref Expression
Assertion logblt 
|- ( ( 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 simp1 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> B e. ( ZZ>= ` 2 ) )
6 eluzelz 
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. ZZ )
7 5 6 syl 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> B e. ZZ )
8 7 zred 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> B e. RR )
9 1z 
 |-  1 e. ZZ
10 1p1e2 
 |-  ( 1 + 1 ) = 2
11 10 fveq2i 
 |-  ( ZZ>= ` ( 1 + 1 ) ) = ( ZZ>= ` 2 )
12 5 11 eleqtrrdi 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> B e. ( ZZ>= ` ( 1 + 1 ) ) )
13 eluzp1l 
 |-  ( ( 1 e. ZZ /\ B e. ( ZZ>= ` ( 1 + 1 ) ) ) -> 1 < B )
14 9 12 13 sylancr 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> 1 < B )
15 8 14 rplogcld 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( log ` B ) e. RR+ )
16 2 4 15 ltdiv1d 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( ( log ` X ) < ( log ` Y ) <-> ( ( log ` X ) / ( log ` B ) ) < ( ( log ` Y ) / ( log ` B ) ) ) )
17 logltb 
 |-  ( ( X e. RR+ /\ Y e. RR+ ) -> ( X < Y <-> ( log ` X ) < ( log ` Y ) ) )
18 17 3adant1 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( X < Y <-> ( log ` X ) < ( log ` Y ) ) )
19 relogbval 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
20 19 3adant3 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
21 relogbval 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ Y e. RR+ ) -> ( B logb Y ) = ( ( log ` Y ) / ( log ` B ) ) )
22 21 3adant2 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( B logb Y ) = ( ( log ` Y ) / ( log ` B ) ) )
23 20 22 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 ) ) ) )
24 16 18 23 3bitr4d 
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( X < Y <-> ( B logb X ) < ( B logb Y ) ) )