Metamath Proof Explorer

Theorem ltmuldiv

Description: 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to A \in ℝ$
2		simp3l	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to C \in ℝ$
3	1 2	remulcld	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to A C \in ℝ$
4		ltdiv1	$⊢ (A C \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A C < B \leftrightarrow \frac{A C}{C} < \frac{B}{C})$
5	3 4	syld3an1	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A C < B \leftrightarrow \frac{A C}{C} < \frac{B}{C})$
6	1	recnd	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to A \in ℂ$
7	2	recnd	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to C \in ℂ$
8		simp3r	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to 0 < C$
9	8	gt0ne0d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to C \neq 0$
10	6 7 9	divcan4d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to \frac{A C}{C} = A$
11	10	breq1d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (\frac{A C}{C} < \frac{B}{C} \leftrightarrow A < \frac{B}{C})$
12	5 11	bitrd	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A C < B \leftrightarrow A < \frac{B}{C})$