Theorem logblebd

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

	Ref	Expression
Hypotheses	logblebd.1	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
	logblebd.2	⊢ ( 𝜑 → 2 ≤ 𝐵 )
	logblebd.3	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	logblebd.4	⊢ ( 𝜑 → 0 < 𝑋 )
	logblebd.5	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
	logblebd.6	⊢ ( 𝜑 → 0 < 𝑌 )
	logblebd.7	⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
Assertion	logblebd	⊢ ( 𝜑 → ( 𝐵 logb 𝑋 ) ≤ ( 𝐵 logb 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		logblebd.1	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
2		logblebd.2	⊢ ( 𝜑 → 2 ≤ 𝐵 )
3		logblebd.3	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
4		logblebd.4	⊢ ( 𝜑 → 0 < 𝑋 )
5		logblebd.5	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
6		logblebd.6	⊢ ( 𝜑 → 0 < 𝑌 )
7		logblebd.7	⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
8	1 2	jca	⊢ ( 𝜑 → ( 𝐵 ∈ ℤ ∧ 2 ≤ 𝐵 ) )
9		2z	⊢ 2 ∈ ℤ
10		eluz1	⊢ ( 2 ∈ ℤ → ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐵 ∈ ℤ ∧ 2 ≤ 𝐵 ) ) )
11	9 10	ax-mp	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐵 ∈ ℤ ∧ 2 ≤ 𝐵 ) )
12	8 11	sylibr	⊢ ( 𝜑 → 𝐵 ∈ ( ℤ≥ ‘ 2 ) )
13	3 4	elrpd	⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
14	5 6	elrpd	⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
15	12 13 14	3jca	⊢ ( 𝜑 → ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) )
16		logbleb	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( 𝑋 ≤ 𝑌 ↔ ( 𝐵 logb 𝑋 ) ≤ ( 𝐵 logb 𝑌 ) ) )
17	15 16	syl	⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ( 𝐵 logb 𝑋 ) ≤ ( 𝐵 logb 𝑌 ) ) )
18	7 17	mpbid	⊢ ( 𝜑 → ( 𝐵 logb 𝑋 ) ≤ ( 𝐵 logb 𝑌 ) )