Theorem logblebd

Description: The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024)

	Ref	Expression
Hypotheses	logblebd.1	$$⊢\phi \to B\in \mathbb{Z}$$
	logblebd.2	$$⊢\phi \to 2\le B$$
	logblebd.3	$$⊢\phi \to X\in ℝ$$
	logblebd.4	$$⊢\phi \to 0<X$$
	logblebd.5	$$⊢\phi \to Y\in ℝ$$
	logblebd.6	$$⊢\phi \to 0<Y$$
	logblebd.7	$$⊢\phi \to X\le Y$$
Assertion	logblebd	$$⊢\phi \to {\log }_{B}X\le {\log }_{B}Y$$

Proof

Step	Hyp	Ref	Expression
1		logblebd.1	$$⊢\phi \to B\in \mathbb{Z}$$
2		logblebd.2	$$⊢\phi \to 2\le B$$
3		logblebd.3	$$⊢\phi \to X\in ℝ$$
4		logblebd.4	$$⊢\phi \to 0<X$$
5		logblebd.5	$$⊢\phi \to Y\in ℝ$$
6		logblebd.6	$$⊢\phi \to 0<Y$$
7		logblebd.7	$$⊢\phi \to X\le Y$$
8	1 2	jca	$$⊢\phi \to \left(B\in \mathbb{Z}\wedge 2\le B\right)$$
9		2z	$$⊢2\in \mathbb{Z}$$
10		eluz1	$$⊢2\in \mathbb{Z}\to \left(B\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(B\in \mathbb{Z}\wedge 2\le B\right)\right)$$
11	9 10	ax-mp	$$⊢B\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(B\in \mathbb{Z}\wedge 2\le B\right)$$
12	8 11	sylibr	$$⊢\phi \to B\in {\mathbb{Z}}_{\ge 2}$$
13	3 4	elrpd	$$⊢\phi \to X\in {ℝ}^{+}$$
14	5 6	elrpd	$$⊢\phi \to Y\in {ℝ}^{+}$$
15	12 13 14	3jca	$$⊢\phi \to \left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\wedge Y\in {ℝ}^{+}\right)$$
16		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)$$
17	15 16	syl	$$⊢\phi \to \left(X\le Y\leftrightarrow {\log }_{B}X\le {\log }_{B}Y\right)$$
18	7 17	mpbid	$$⊢\phi \to {\log }_{B}X\le {\log }_{B}Y$$