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 {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \left(X<Y\leftrightarrow {\log }_{B}X<{\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		simp1	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to B\in {\mathbb{Z}}_{\ge 2}$$
6		eluzelz	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to B\in \mathbb{Z}$$
7	5 6	syl	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to B\in \mathbb{Z}$$
8	7	zred	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to B\in ℝ$$
9		1z	$$⊢1\in \mathbb{Z}$$
10		1p1e2	$$⊢1+1=2$$
11	10	fveq2i	$$⊢{\mathbb{Z}}_{\ge \left(1+1\right)}={\mathbb{Z}}_{\ge 2}$$
12	5 11	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)}$$
13		eluzp1l	$$⊢\left(1\in \mathbb{Z}\wedge B\in {\mathbb{Z}}_{\ge \left(1+1\right)}\right)\to 1<B$$
14	9 12 13	sylancr	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to 1<B$$
15	8 14	rplogcld	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \log B\in {ℝ}^{+}$$
16	2 4 15	ltdiv1d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \left(\log X<\log Y\leftrightarrow \frac{\log X}{\log B}<\frac{\log Y}{\log B}\right)$$
17		logltb	$$⊢\left(X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \left(X<Y\leftrightarrow \log X<\log Y\right)$$
18	17	3adant1	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \left(X<Y\leftrightarrow \log X<\log Y\right)$$
19		relogbval	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to {\log }_{B}X=\frac{\log X}{\log B}$$
20	19	3adant3	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to {\log }_{B}X=\frac{\log X}{\log B}$$
21		relogbval	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge Y\in {ℝ}^{+}\right)\to {\log }_{B}Y=\frac{\log Y}{\log B}$$
22	21	3adant2	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to {\log }_{B}Y=\frac{\log Y}{\log B}$$
23	20 22	breq12d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \left({\log }_{B}X<{\log }_{B}Y\leftrightarrow \frac{\log X}{\log B}<\frac{\log Y}{\log B}\right)$$
24	16 18 23	3bitr4d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)\to \left(X<Y\leftrightarrow {\log }_{B}X<{\log }_{B}Y\right)$$