Theorem logblebd

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

	Ref	Expression
Hypotheses	logblebd.1	|- ( ph -> B e. ZZ )
	logblebd.2	|- ( ph -> 2 <_ B )
	logblebd.3	|- ( ph -> X e. RR )
	logblebd.4	|- ( ph -> 0 < X )
	logblebd.5	|- ( ph -> Y e. RR )
	logblebd.6	|- ( ph -> 0 < Y )
	logblebd.7	|- ( ph -> X <_ Y )
Assertion	logblebd	|- ( ph -> ( B logb X ) <_ ( B logb Y ) )

Proof

Step	Hyp	Ref	Expression
1		logblebd.1	|- ( ph -> B e. ZZ )
2		logblebd.2	|- ( ph -> 2 <_ B )
3		logblebd.3	|- ( ph -> X e. RR )
4		logblebd.4	|- ( ph -> 0 < X )
5		logblebd.5	|- ( ph -> Y e. RR )
6		logblebd.6	|- ( ph -> 0 < Y )
7		logblebd.7	|- ( ph -> X <_ Y )
8	1 2	jca	|- ( ph -> ( B e. ZZ /\ 2 <_ B ) )
9		2z	|- 2 e. ZZ
10		eluz1	|- ( 2 e. ZZ -> ( B e. ( ZZ>= ` 2 ) <-> ( B e. ZZ /\ 2 <_ B ) ) )
11	9 10	ax-mp	|- ( B e. ( ZZ>= ` 2 ) <-> ( B e. ZZ /\ 2 <_ B ) )
12	8 11	sylibr	|- ( ph -> B e. ( ZZ>= ` 2 ) )
13	3 4	elrpd	|- ( ph -> X e. RR+ )
14	5 6	elrpd	|- ( ph -> Y e. RR+ )
15	12 13 14	3jca	|- ( ph -> ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) )
16		logbleb	|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( X <_ Y <-> ( B logb X ) <_ ( B logb Y ) ) )
17	15 16	syl	|- ( ph -> ( X <_ Y <-> ( B logb X ) <_ ( B logb Y ) ) )
18	7 17	mpbid	|- ( ph -> ( B logb X ) <_ ( B logb Y ) )