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