ledivp1i

Description: "Less than or equal to" and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 17-Sep-2005)

	Ref	Expression
Hypotheses	ltplus1.1	$⊢ A \in ℝ$
	prodgt0.2	$⊢ B \in ℝ$
	ltmul1.3	$⊢ C \in ℝ$
Assertion	ledivp1i	$⊢ (0 \leq A \land 0 \leq C \land A \leq \frac{B}{C + 1}) \to A C \leq B$

Proof

Step	Hyp	Ref	Expression
1		ltplus1.1	$⊢ A \in ℝ$
2		prodgt0.2	$⊢ B \in ℝ$
3		ltmul1.3	$⊢ C \in ℝ$
4		1re	$⊢ 1 \in ℝ$
5	3 4	readdcli	$⊢ C + 1 \in ℝ$
6	3	ltp1i	$⊢ C < C + 1$
7	3 5 6	ltleii	$⊢ C \leq C + 1$
8		lemul2a	$⊢ ((C \in ℝ \land C + 1 \in ℝ \land (A \in ℝ \land 0 \leq A)) \land C \leq C + 1) \to A C \leq A (C + 1)$
9	7 8	mpan2	$⊢ (C \in ℝ \land C + 1 \in ℝ \land (A \in ℝ \land 0 \leq A)) \to A C \leq A (C + 1)$
10	3 5 9	mp3an12	$⊢ (A \in ℝ \land 0 \leq A) \to A C \leq A (C + 1)$
11	1 10	mpan	$⊢ 0 \leq A \to A C \leq A (C + 1)$
12	11	3ad2ant1	$⊢ (0 \leq A \land 0 \leq C \land A \leq \frac{B}{C + 1}) \to A C \leq A (C + 1)$
13		0re	$⊢ 0 \in ℝ$
14	13 3 5	lelttri	$⊢ (0 \leq C \land C < C + 1) \to 0 < C + 1$
15	6 14	mpan2	$⊢ 0 \leq C \to 0 < C + 1$
16	5	gt0ne0i	$⊢ 0 < C + 1 \to C + 1 \neq 0$
17	2 5	redivclzi	$⊢ C + 1 \neq 0 \to \frac{B}{C + 1} \in ℝ$
18	16 17	syl	$⊢ 0 < C + 1 \to \frac{B}{C + 1} \in ℝ$
19		lemul1	$⊢ (A \in ℝ \land \frac{B}{C + 1} \in ℝ \land (C + 1 \in ℝ \land 0 < C + 1)) \to (A \leq \frac{B}{C + 1} \leftrightarrow A (C + 1) \leq (\frac{B}{C + 1}) (C + 1))$
20	1 19	mp3an1	$⊢ (\frac{B}{C + 1} \in ℝ \land (C + 1 \in ℝ \land 0 < C + 1)) \to (A \leq \frac{B}{C + 1} \leftrightarrow A (C + 1) \leq (\frac{B}{C + 1}) (C + 1))$
21	20	ex	$⊢ \frac{B}{C + 1} \in ℝ \to ((C + 1 \in ℝ \land 0 < C + 1) \to (A \leq \frac{B}{C + 1} \leftrightarrow A (C + 1) \leq (\frac{B}{C + 1}) (C + 1)))$
22	5 21	mpani	$⊢ \frac{B}{C + 1} \in ℝ \to (0 < C + 1 \to (A \leq \frac{B}{C + 1} \leftrightarrow A (C + 1) \leq (\frac{B}{C + 1}) (C + 1)))$
23	18 22	mpcom	$⊢ 0 < C + 1 \to (A \leq \frac{B}{C + 1} \leftrightarrow A (C + 1) \leq (\frac{B}{C + 1}) (C + 1))$
24	23	biimpd	$⊢ 0 < C + 1 \to (A \leq \frac{B}{C + 1} \to A (C + 1) \leq (\frac{B}{C + 1}) (C + 1))$
25	15 24	syl	$⊢ 0 \leq C \to (A \leq \frac{B}{C + 1} \to A (C + 1) \leq (\frac{B}{C + 1}) (C + 1))$
26	25	imp	$⊢ (0 \leq C \land A \leq \frac{B}{C + 1}) \to A (C + 1) \leq (\frac{B}{C + 1}) (C + 1)$
27	2	recni	$⊢ B \in ℂ$
28	5	recni	$⊢ C + 1 \in ℂ$
29	27 28	divcan1zi	$⊢ C + 1 \neq 0 \to (\frac{B}{C + 1}) (C + 1) = B$
30	15 16 29	3syl	$⊢ 0 \leq C \to (\frac{B}{C + 1}) (C + 1) = B$
31	30	adantr	$⊢ (0 \leq C \land A \leq \frac{B}{C + 1}) \to (\frac{B}{C + 1}) (C + 1) = B$
32	26 31	breqtrd	$⊢ (0 \leq C \land A \leq \frac{B}{C + 1}) \to A (C + 1) \leq B$
33	32	3adant1	$⊢ (0 \leq A \land 0 \leq C \land A \leq \frac{B}{C + 1}) \to A (C + 1) \leq B$
34	1 3	remulcli	$⊢ A C \in ℝ$
35	1 5	remulcli	$⊢ A (C + 1) \in ℝ$
36	34 35 2	letri	$⊢ (A C \leq A (C + 1) \land A (C + 1) \leq B) \to A C \leq B$
37	12 33 36	syl2anc	$⊢ (0 \leq A \land 0 \leq C \land A \leq \frac{B}{C + 1}) \to A C \leq B$

Metamath Proof Explorer

Theorem ledivp1i

Proof