ltdivp1i

Description: Less-than 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	ltdivp1i	$⊢ (0 \leq A \land 0 \leq C \land A < \frac{B}{C + 1}) \to A C < 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 < \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		ltmul1	$⊢ (A \in ℝ \land \frac{B}{C + 1} \in ℝ \land (C + 1 \in ℝ \land 0 < C + 1)) \to (A < \frac{B}{C + 1} \leftrightarrow A (C + 1) < (\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 < \frac{B}{C + 1} \leftrightarrow A (C + 1) < (\frac{B}{C + 1}) (C + 1))$
21	5 20	mpanr1	$⊢ (\frac{B}{C + 1} \in ℝ \land 0 < C + 1) \to (A < \frac{B}{C + 1} \leftrightarrow A (C + 1) < (\frac{B}{C + 1}) (C + 1))$
22	18 21	mpancom	$⊢ 0 < C + 1 \to (A < \frac{B}{C + 1} \leftrightarrow A (C + 1) < (\frac{B}{C + 1}) (C + 1))$
23	22	biimpd	$⊢ 0 < C + 1 \to (A < \frac{B}{C + 1} \to A (C + 1) < (\frac{B}{C + 1}) (C + 1))$
24	15 23	syl	$⊢ 0 \leq C \to (A < \frac{B}{C + 1} \to A (C + 1) < (\frac{B}{C + 1}) (C + 1))$
25	24	imp	$⊢ (0 \leq C \land A < \frac{B}{C + 1}) \to A (C + 1) < (\frac{B}{C + 1}) (C + 1)$
26	2	recni	$⊢ B \in ℂ$
27	5	recni	$⊢ C + 1 \in ℂ$
28	26 27	divcan1zi	$⊢ C + 1 \neq 0 \to (\frac{B}{C + 1}) (C + 1) = B$
29	15 16 28	3syl	$⊢ 0 \leq C \to (\frac{B}{C + 1}) (C + 1) = B$
30	29	adantr	$⊢ (0 \leq C \land A < \frac{B}{C + 1}) \to (\frac{B}{C + 1}) (C + 1) = B$
31	25 30	breqtrd	$⊢ (0 \leq C \land A < \frac{B}{C + 1}) \to A (C + 1) < B$
32	31	3adant1	$⊢ (0 \leq A \land 0 \leq C \land A < \frac{B}{C + 1}) \to A (C + 1) < B$
33	1 3	remulcli	$⊢ A C \in ℝ$
34	1 5	remulcli	$⊢ A (C + 1) \in ℝ$
35	33 34 2	lelttri	$⊢ (A C \leq A (C + 1) \land A (C + 1) < B) \to A C < B$
36	12 32 35	syl2anc	$⊢ (0 \leq A \land 0 \leq C \land A < \frac{B}{C + 1}) \to A C < B$

Metamath Proof Explorer

Theorem ltdivp1i

Proof