Metamath Proof Explorer

Theorem reglogltb

Description: General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014) (New usage is discouraged.) Use logblt instead.

		Ref	Expression
	Assertion	reglogltb	$⊢ ((A \in ℝ^{+} \land B \in ℝ^{+}) \land (C \in ℝ^{+} \land 1 < C)) \to (A < B \leftrightarrow \frac{\log A}{\log C} < \frac{\log B}{\log C})$

Proof

Step	Hyp	Ref	Expression
1		logltb	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to (A < B \leftrightarrow \log A < \log B)$
2	1	adantr	$⊢ ((A \in ℝ^{+} \land B \in ℝ^{+}) \land (C \in ℝ^{+} \land 1 < C)) \to (A < B \leftrightarrow \log A < \log B)$
3		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
4	3	ad2antrr	$⊢ ((A \in ℝ^{+} \land B \in ℝ^{+}) \land (C \in ℝ^{+} \land 1 < C)) \to \log A \in ℝ$
5		relogcl	$⊢ B \in ℝ^{+} \to \log B \in ℝ$
6	5	ad2antlr	$⊢ ((A \in ℝ^{+} \land B \in ℝ^{+}) \land (C \in ℝ^{+} \land 1 < C)) \to \log B \in ℝ$
7		relogcl	$⊢ C \in ℝ^{+} \to \log C \in ℝ$
8	7	ad2antrl	$⊢ ((A \in ℝ^{+} \land B \in ℝ^{+}) \land (C \in ℝ^{+} \land 1 < C)) \to \log C \in ℝ$
9		log1	$⊢ \log 1 = 0$
10		1rp	$⊢ 1 \in ℝ^{+}$
11		logltb	$⊢ (1 \in ℝ^{+} \land C \in ℝ^{+}) \to (1 < C \leftrightarrow \log 1 < \log C)$
12	10 11	mpan	$⊢ C \in ℝ^{+} \to (1 < C \leftrightarrow \log 1 < \log C)$
13	12	biimpa	$⊢ (C \in ℝ^{+} \land 1 < C) \to \log 1 < \log C$
14	9 13	eqbrtrrid	$⊢ (C \in ℝ^{+} \land 1 < C) \to 0 < \log C$
15	14	adantl	$⊢ ((A \in ℝ^{+} \land B \in ℝ^{+}) \land (C \in ℝ^{+} \land 1 < C)) \to 0 < \log C$
16		ltdiv1	$⊢ (\log A \in ℝ \land \log B \in ℝ \land (\log C \in ℝ \land 0 < \log C)) \to (\log A < \log B \leftrightarrow \frac{\log A}{\log C} < \frac{\log B}{\log C})$
17	4 6 8 15 16	syl112anc	$⊢ ((A \in ℝ^{+} \land B \in ℝ^{+}) \land (C \in ℝ^{+} \land 1 < C)) \to (\log A < \log B \leftrightarrow \frac{\log A}{\log C} < \frac{\log B}{\log C})$
18	2 17	bitrd	$⊢ ((A \in ℝ^{+} \land B \in ℝ^{+}) \land (C \in ℝ^{+} \land 1 < C)) \to (A < B \leftrightarrow \frac{\log A}{\log C} < \frac{\log B}{\log C})$