# 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 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to \left({X}<{Y}↔{\mathrm{log}}_{{B}}{X}<{\mathrm{log}}_{{B}}{Y}\right)$

### Proof

Step Hyp Ref Expression
1 simp2 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to {X}\in {ℝ}^{+}$
2 1 relogcld ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to \mathrm{log}{X}\in ℝ$
3 simp3 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to {Y}\in {ℝ}^{+}$
4 3 relogcld ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to \mathrm{log}{Y}\in ℝ$
5 simp1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to {B}\in {ℤ}_{\ge 2}$
6 eluzelz ${⊢}{B}\in {ℤ}_{\ge 2}\to {B}\in ℤ$
7 5 6 syl ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to {B}\in ℤ$
8 7 zred ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to {B}\in ℝ$
9 1z ${⊢}1\in ℤ$
10 1p1e2 ${⊢}1+1=2$
11 10 fveq2i ${⊢}{ℤ}_{\ge \left(1+1\right)}={ℤ}_{\ge 2}$
12 5 11 syl6eleqr ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to {B}\in {ℤ}_{\ge \left(1+1\right)}$
13 eluzp1l ${⊢}\left(1\in ℤ\wedge {B}\in {ℤ}_{\ge \left(1+1\right)}\right)\to 1<{B}$
14 9 12 13 sylancr ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to 1<{B}$
15 8 14 rplogcld ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to \mathrm{log}{B}\in {ℝ}^{+}$
16 2 4 15 ltdiv1d ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to \left(\mathrm{log}{X}<\mathrm{log}{Y}↔\frac{\mathrm{log}{X}}{\mathrm{log}{B}}<\frac{\mathrm{log}{Y}}{\mathrm{log}{B}}\right)$
17 logltb ${⊢}\left({X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to \left({X}<{Y}↔\mathrm{log}{X}<\mathrm{log}{Y}\right)$
18 17 3adant1 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to \left({X}<{Y}↔\mathrm{log}{X}<\mathrm{log}{Y}\right)$
19 relogbval ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\right)\to {\mathrm{log}}_{{B}}{X}=\frac{\mathrm{log}{X}}{\mathrm{log}{B}}$
20 19 3adant3 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to {\mathrm{log}}_{{B}}{X}=\frac{\mathrm{log}{X}}{\mathrm{log}{B}}$
21 relogbval ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {Y}\in {ℝ}^{+}\right)\to {\mathrm{log}}_{{B}}{Y}=\frac{\mathrm{log}{Y}}{\mathrm{log}{B}}$
22 21 3adant2 ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to {\mathrm{log}}_{{B}}{Y}=\frac{\mathrm{log}{Y}}{\mathrm{log}{B}}$
23 20 22 breq12d ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to \left({\mathrm{log}}_{{B}}{X}<{\mathrm{log}}_{{B}}{Y}↔\frac{\mathrm{log}{X}}{\mathrm{log}{B}}<\frac{\mathrm{log}{Y}}{\mathrm{log}{B}}\right)$
24 16 18 23 3bitr4d ${⊢}\left({B}\in {ℤ}_{\ge 2}\wedge {X}\in {ℝ}^{+}\wedge {Y}\in {ℝ}^{+}\right)\to \left({X}<{Y}↔{\mathrm{log}}_{{B}}{X}<{\mathrm{log}}_{{B}}{Y}\right)$