Metamath Proof Explorer

Theorem lemuldiv

Description: 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006)

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

Proof

Step	Hyp	Ref	Expression
1		ltdivmul2	$⊢ (B \in ℝ \land A \in ℝ \land (C \in ℝ \land 0 < C)) \to (\frac{B}{C} < A \leftrightarrow B < A C)$
2	1	3com12	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (\frac{B}{C} < A \leftrightarrow B < A C)$
3	2	notbid	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (\neg \frac{B}{C} < A \leftrightarrow \neg B < A C)$
4		simp1	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to A \in ℝ$
5		gt0ne0	$⊢ (C \in ℝ \land 0 < C) \to C \neq 0$
6	5	3adant1	$⊢ (B \in ℝ \land C \in ℝ \land 0 < C) \to C \neq 0$
7		redivcl	$⊢ (B \in ℝ \land C \in ℝ \land C \neq 0) \to \frac{B}{C} \in ℝ$
8	6 7	syld3an3	$⊢ (B \in ℝ \land C \in ℝ \land 0 < C) \to \frac{B}{C} \in ℝ$
9	8	3expb	$⊢ (B \in ℝ \land (C \in ℝ \land 0 < C)) \to \frac{B}{C} \in ℝ$
10	9	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to \frac{B}{C} \in ℝ$
11	4 10	lenltd	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A \leq \frac{B}{C} \leftrightarrow \neg \frac{B}{C} < A)$
12		remulcl	$⊢ (A \in ℝ \land C \in ℝ) \to A C \in ℝ$
13	12	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A C \in ℝ$
14		simp2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B \in ℝ$
15	13 14	lenltd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A C \leq B \leftrightarrow \neg B < A C)$
16	15	3adant3r	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A C \leq B \leftrightarrow \neg B < A C)$
17	3 11 16	3bitr4rd	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A C \leq B \leftrightarrow A \leq \frac{B}{C})$