ledivge1le

Description: If a number is less than or equal to another number, the number divided by a positive number greater than or equal to one is less than or equal to the other number. (Contributed by AV, 29-Jun-2021)

		Ref	Expression
	Assertion	ledivge1le	$⊢ (A \in ℝ \land B \in ℝ^{+} \land (C \in ℝ^{+} \land 1 \leq C)) \to (A \leq B \to \frac{A}{C} \leq B)$

Proof

Step	Hyp	Ref	Expression
1		divle1le	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (\frac{A}{B} \leq 1 \leftrightarrow A \leq B)$
2	1	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land C \in ℝ^{+}) \to (\frac{A}{B} \leq 1 \leftrightarrow A \leq B)$
3		rerpdivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ$
4	3	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land C \in ℝ^{+}) \to \frac{A}{B} \in ℝ$
5		1red	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land C \in ℝ^{+}) \to 1 \in ℝ$
6		rpre	$⊢ C \in ℝ^{+} \to C \in ℝ$
7	6	adantl	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land C \in ℝ^{+}) \to C \in ℝ$
8		letr	$⊢ (\frac{A}{B} \in ℝ \land 1 \in ℝ \land C \in ℝ) \to ((\frac{A}{B} \leq 1 \land 1 \leq C) \to \frac{A}{B} \leq C)$
9	4 5 7 8	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land C \in ℝ^{+}) \to ((\frac{A}{B} \leq 1 \land 1 \leq C) \to \frac{A}{B} \leq C)$
10	9	expd	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land C \in ℝ^{+}) \to (\frac{A}{B} \leq 1 \to (1 \leq C \to \frac{A}{B} \leq C))$
11	2 10	sylbird	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land C \in ℝ^{+}) \to (A \leq B \to (1 \leq C \to \frac{A}{B} \leq C))$
12	11	com23	$⊢ ((A \in ℝ \land B \in ℝ^{+}) \land C \in ℝ^{+}) \to (1 \leq C \to (A \leq B \to \frac{A}{B} \leq C))$
13	12	expimpd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ((C \in ℝ^{+} \land 1 \leq C) \to (A \leq B \to \frac{A}{B} \leq C))$
14	13	ex	$⊢ A \in ℝ \to (B \in ℝ^{+} \to ((C \in ℝ^{+} \land 1 \leq C) \to (A \leq B \to \frac{A}{B} \leq C)))$
15	14	3imp1	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land (C \in ℝ^{+} \land 1 \leq C)) \land A \leq B) \to \frac{A}{B} \leq C$
16		simp1	$⊢ (A \in ℝ \land B \in ℝ^{+} \land (C \in ℝ^{+} \land 1 \leq C)) \to A \in ℝ$
17	6	adantr	$⊢ (C \in ℝ^{+} \land 1 \leq C) \to C \in ℝ$
18		0lt1	$⊢ 0 < 1$
19		0red	$⊢ C \in ℝ^{+} \to 0 \in ℝ$
20		1red	$⊢ C \in ℝ^{+} \to 1 \in ℝ$
21		ltletr	$⊢ (0 \in ℝ \land 1 \in ℝ \land C \in ℝ) \to ((0 < 1 \land 1 \leq C) \to 0 < C)$
22	19 20 6 21	syl3anc	$⊢ C \in ℝ^{+} \to ((0 < 1 \land 1 \leq C) \to 0 < C)$
23	18 22	mpani	$⊢ C \in ℝ^{+} \to (1 \leq C \to 0 < C)$
24	23	imp	$⊢ (C \in ℝ^{+} \land 1 \leq C) \to 0 < C$
25	17 24	jca	$⊢ (C \in ℝ^{+} \land 1 \leq C) \to (C \in ℝ \land 0 < C)$
26	25	3ad2ant3	$⊢ (A \in ℝ \land B \in ℝ^{+} \land (C \in ℝ^{+} \land 1 \leq C)) \to (C \in ℝ \land 0 < C)$
27		rpregt0	$⊢ B \in ℝ^{+} \to (B \in ℝ \land 0 < B)$
28	27	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ^{+} \land (C \in ℝ^{+} \land 1 \leq C)) \to (B \in ℝ \land 0 < B)$
29	16 26 28	3jca	$⊢ (A \in ℝ \land B \in ℝ^{+} \land (C \in ℝ^{+} \land 1 \leq C)) \to (A \in ℝ \land (C \in ℝ \land 0 < C) \land (B \in ℝ \land 0 < B))$
30	29	adantr	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land (C \in ℝ^{+} \land 1 \leq C)) \land A \leq B) \to (A \in ℝ \land (C \in ℝ \land 0 < C) \land (B \in ℝ \land 0 < B))$
31		lediv23	$⊢ (A \in ℝ \land (C \in ℝ \land 0 < C) \land (B \in ℝ \land 0 < B)) \to (\frac{A}{C} \leq B \leftrightarrow \frac{A}{B} \leq C)$
32	30 31	syl	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land (C \in ℝ^{+} \land 1 \leq C)) \land A \leq B) \to (\frac{A}{C} \leq B \leftrightarrow \frac{A}{B} \leq C)$
33	15 32	mpbird	$⊢ ((A \in ℝ \land B \in ℝ^{+} \land (C \in ℝ^{+} \land 1 \leq C)) \land A \leq B) \to \frac{A}{C} \leq B$
34	33	ex	$⊢ (A \in ℝ \land B \in ℝ^{+} \land (C \in ℝ^{+} \land 1 \leq C)) \to (A \leq B \to \frac{A}{C} \leq B)$

Metamath Proof Explorer

Theorem ledivge1le

Proof