ltdivmul2

Description: 'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005)

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

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

Metamath Proof Explorer