Theorem reglogleb

Description: General logarithm preserves <_ . (Contributed by Stefan O'Rear, 19-Oct-2014) (New usage is discouraged.) Use logbleb instead.

	Ref	Expression
Assertion	reglogleb	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐶 ∈ ℝ+ ∧ 1 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( ( log ‘ 𝐴 ) / ( log ‘ 𝐶 ) ) ≤ ( ( log ‘ 𝐵 ) / ( log ‘ 𝐶 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		logleb	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 ↔ ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ) )
2	1	adantr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐶 ∈ ℝ+ ∧ 1 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ) )
3		relogcl	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
4	3	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐶 ∈ ℝ+ ∧ 1 < 𝐶 ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
5		relogcl	⊢ ( 𝐵 ∈ ℝ+ → ( log ‘ 𝐵 ) ∈ ℝ )
6	5	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐶 ∈ ℝ+ ∧ 1 < 𝐶 ) ) → ( log ‘ 𝐵 ) ∈ ℝ )
7		relogcl	⊢ ( 𝐶 ∈ ℝ+ → ( log ‘ 𝐶 ) ∈ ℝ )
8	7	ad2antrl	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐶 ∈ ℝ+ ∧ 1 < 𝐶 ) ) → ( log ‘ 𝐶 ) ∈ ℝ )
9		log1	⊢ ( log ‘ 1 ) = 0
10		1rp	⊢ 1 ∈ ℝ+
11		logltb	⊢ ( ( 1 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( 1 < 𝐶 ↔ ( log ‘ 1 ) < ( log ‘ 𝐶 ) ) )
12	10 11	mpan	⊢ ( 𝐶 ∈ ℝ+ → ( 1 < 𝐶 ↔ ( log ‘ 1 ) < ( log ‘ 𝐶 ) ) )
13	12	biimpa	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 1 < 𝐶 ) → ( log ‘ 1 ) < ( log ‘ 𝐶 ) )
14	9 13	eqbrtrrid	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 1 < 𝐶 ) → 0 < ( log ‘ 𝐶 ) )
15	14	adantl	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐶 ∈ ℝ+ ∧ 1 < 𝐶 ) ) → 0 < ( log ‘ 𝐶 ) )
16		lediv1	⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ ( log ‘ 𝐵 ) ∈ ℝ ∧ ( ( log ‘ 𝐶 ) ∈ ℝ ∧ 0 < ( log ‘ 𝐶 ) ) ) → ( ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ↔ ( ( log ‘ 𝐴 ) / ( log ‘ 𝐶 ) ) ≤ ( ( log ‘ 𝐵 ) / ( log ‘ 𝐶 ) ) ) )
17	4 6 8 15 16	syl112anc	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐶 ∈ ℝ+ ∧ 1 < 𝐶 ) ) → ( ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ↔ ( ( log ‘ 𝐴 ) / ( log ‘ 𝐶 ) ) ≤ ( ( log ‘ 𝐵 ) / ( log ‘ 𝐶 ) ) ) )
18	2 17	bitrd	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ ( 𝐶 ∈ ℝ+ ∧ 1 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( ( log ‘ 𝐴 ) / ( log ‘ 𝐶 ) ) ≤ ( ( log ‘ 𝐵 ) / ( log ‘ 𝐶 ) ) ) )