ltmuldiv2

Description: 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004)

		Ref	Expression
	Assertion	ltmuldiv2	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (C A < B \leftrightarrow A < \frac{B}{C})$

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		recn	$⊢ C \in ℝ \to C \in ℂ$
3		mulcom	$⊢ (A \in ℂ \land C \in ℂ) \to A C = C A$
4	1 2 3	syl2an	$⊢ (A \in ℝ \land C \in ℝ) \to A C = C A$
5	4	adantrr	$⊢ (A \in ℝ \land (C \in ℝ \land 0 < C)) \to A C = C A$
6	5	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to A C = C A$
7	6	breq1d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A C < B \leftrightarrow C A < B)$
8		ltmuldiv	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A C < B \leftrightarrow A < \frac{B}{C})$
9	7 8	bitr3d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (C A < B \leftrightarrow A < \frac{B}{C})$

Metamath Proof Explorer