ledivmul2

Description: 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005)

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

Step	Hyp	Ref	Expression
1		ledivmul	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (\frac{A}{C} \leq B \leftrightarrow A \leq 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 \leq B C \leftrightarrow A \leq C B)$
9	1 8	bitr4d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (\frac{A}{C} \leq B \leftrightarrow A \leq B C)$

Metamath Proof Explorer