ltdivmul

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

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

Step	Hyp	Ref	Expression
1		remulcl	$⊢ (C \in ℝ \land B \in ℝ) \to C B \in ℝ$
2	1	ancoms	$⊢ (B \in ℝ \land C \in ℝ) \to C B \in ℝ$
3	2	adantrr	$⊢ (B \in ℝ \land (C \in ℝ \land 0 < C)) \to C B \in ℝ$
4	3	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to C B \in ℝ$
5		ltdiv1	$⊢ (A \in ℝ \land C B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A < C B \leftrightarrow \frac{A}{C} < \frac{C B}{C})$
6	4 5	syld3an2	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A < C B \leftrightarrow \frac{A}{C} < \frac{C B}{C})$
7		recn	$⊢ B \in ℝ \to B \in ℂ$
8	7	adantr	$⊢ (B \in ℝ \land (C \in ℝ \land 0 < C)) \to B \in ℂ$
9		recn	$⊢ C \in ℝ \to C \in ℂ$
10	9	ad2antrl	$⊢ (B \in ℝ \land (C \in ℝ \land 0 < C)) \to C \in ℂ$
11		gt0ne0	$⊢ (C \in ℝ \land 0 < C) \to C \neq 0$
12	11	adantl	$⊢ (B \in ℝ \land (C \in ℝ \land 0 < C)) \to C \neq 0$
13	8 10 12	divcan3d	$⊢ (B \in ℝ \land (C \in ℝ \land 0 < C)) \to \frac{C B}{C} = B$
14	13	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to \frac{C B}{C} = B$
15	14	breq2d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (\frac{A}{C} < \frac{C B}{C} \leftrightarrow \frac{A}{C} < B)$
16	6 15	bitr2d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (\frac{A}{C} < B \leftrightarrow A < C B)$

Metamath Proof Explorer