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	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \left(X\le Y\leftrightarrow {\log }_{B}X\le {\log }_{B}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		simp2	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to X\in {ℝ}^{+}$$
2	1	relogcld	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \log X\in ℝ$$
3		simp3	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to Y\in {ℝ}^{+}$$
4	3	relogcld	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \log Y\in ℝ$$
5		eluzelre	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to B\in ℝ$$
6	5	3ad2ant1	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to B\in ℝ$$
7		1z	$$⊢1\in \mathbb{Z}$$
8		simp1	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to B\in {\mathbb{Z}}_{\ge 2}$$
9		1p1e2	$$⊢1+1=2$$
10	9	fveq2i	$$⊢{\mathbb{Z}}_{\ge \left(1+1\right)}={\mathbb{Z}}_{\ge 2}$$
11	8 10	eleqtrrdi	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to B\in {\mathbb{Z}}_{\ge \left(1+1\right)}$$
12		eluzp1l	$$⊢\left(1\in \mathbb{Z}\wedge B\in {\mathbb{Z}}_{\ge \left(1+1\right)}\right)\to 1<B$$
13	7 11 12	sylancr	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to 1<B$$
14	6 13	rplogcld	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \log B\in {ℝ}^{+}$$
15	2 4 14	lediv1d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \left(\log X\le \log Y\leftrightarrow \frac{\log X}{\log B}\le \frac{\log Y}{\log B}\right)$$
16		logleb	$$⊢\left(X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \left(X\le Y\leftrightarrow \log X\le \log Y\right)$$
17	16	3adant1	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \left(X\le Y\leftrightarrow \log X\le \log Y\right)$$
18		relogbval	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to {\log }_{B}X=\frac{\log X}{\log B}$$
19	18	3adant3	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to {\log }_{B}X=\frac{\log X}{\log B}$$
20		relogbval	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge Y\in {ℝ}^{+}\right)\to {\log }_{B}Y=\frac{\log Y}{\log B}$$
21	20	3adant2	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to {\log }_{B}Y=\frac{\log Y}{\log B}$$
22	19 21	breq12d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \left({\log }_{B}X\le {\log }_{B}Y\leftrightarrow \frac{\log X}{\log B}\le \frac{\log Y}{\log B}\right)$$
23	15 17 22	3bitr4d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \left(X\le Y\leftrightarrow {\log }_{B}X\le {\log }_{B}Y\right)$$