Metamath Proof Explorer

Theorem lediv1

Description: Division of both sides of a less than or equal to relation by a positive number. (Contributed by NM, 18-Nov-2004)

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

Proof

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