ltmul12a

Description: Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005)

		Ref	Expression
	Assertion	ltmul12a	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land ((C \in ℝ \land D \in ℝ) \land (0 \leq C \land C < D))) \to A C < B D$

Proof

Step	Hyp	Ref	Expression
1		simplll	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land ((0 \leq A \land A < B) \land (0 \leq C \land C < D))) \to A \in ℝ$
2		simpllr	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land ((0 \leq A \land A < B) \land (0 \leq C \land C < D))) \to B \in ℝ$
3		simpll	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 \leq C \land C < D)) \to C \in ℝ$
4		simprl	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 \leq C \land C < D)) \to 0 \leq C$
5	3 4	jca	$⊢ ((C \in ℝ \land D \in ℝ) \land (0 \leq C \land C < D)) \to (C \in ℝ \land 0 \leq C)$
6	5	ad2ant2l	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land ((0 \leq A \land A < B) \land (0 \leq C \land C < D))) \to (C \in ℝ \land 0 \leq C)$
7		ltle	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \to A \leq B)$
8	7	imp	$⊢ ((A \in ℝ \land B \in ℝ) \land A < B) \to A \leq B$
9	8	adantrl	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to A \leq B$
10	9	ad2ant2r	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land ((0 \leq A \land A < B) \land (0 \leq C \land C < D))) \to A \leq B$
11		lemul1a	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 \leq C)) \land A \leq B) \to A C \leq B C$
12	1 2 6 10 11	syl31anc	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land ((0 \leq A \land A < B) \land (0 \leq C \land C < D))) \to A C \leq B C$
13		simplrl	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land (0 \leq A \land A < B)) \to C \in ℝ$
14		simplrr	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land (0 \leq A \land A < B)) \to D \in ℝ$
15		simpllr	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land (0 \leq A \land A < B)) \to B \in ℝ$
16		0re	$⊢ 0 \in ℝ$
17		lelttr	$⊢ (0 \in ℝ \land A \in ℝ \land B \in ℝ) \to ((0 \leq A \land A < B) \to 0 < B)$
18	16 17	mp3an1	$⊢ (A \in ℝ \land B \in ℝ) \to ((0 \leq A \land A < B) \to 0 < B)$
19	18	imp	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \to 0 < B$
20	19	adantlr	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land (0 \leq A \land A < B)) \to 0 < B$
21		ltmul2	$⊢ (C \in ℝ \land D \in ℝ \land (B \in ℝ \land 0 < B)) \to (C < D \leftrightarrow B C < B D)$
22	13 14 15 20 21	syl112anc	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land (0 \leq A \land A < B)) \to (C < D \leftrightarrow B C < B D)$
23	22	biimpa	$⊢ ((((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land (0 \leq A \land A < B)) \land C < D) \to B C < B D$
24	23	anasss	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land ((0 \leq A \land A < B) \land C < D)) \to B C < B D$
25	24	adantrrl	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land ((0 \leq A \land A < B) \land (0 \leq C \land C < D))) \to B C < B D$
26		remulcl	$⊢ (A \in ℝ \land C \in ℝ) \to A C \in ℝ$
27	26	ad2ant2r	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A C \in ℝ$
28		remulcl	$⊢ (B \in ℝ \land C \in ℝ) \to B C \in ℝ$
29	28	ad2ant2lr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B C \in ℝ$
30		remulcl	$⊢ (B \in ℝ \land D \in ℝ) \to B D \in ℝ$
31	30	ad2ant2l	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B D \in ℝ$
32		lelttr	$⊢ (A C \in ℝ \land B C \in ℝ \land B D \in ℝ) \to ((A C \leq B C \land B C < B D) \to A C < B D)$
33	27 29 31 32	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ((A C \leq B C \land B C < B D) \to A C < B D)$
34	33	adantr	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land ((0 \leq A \land A < B) \land (0 \leq C \land C < D))) \to ((A C \leq B C \land B C < B D) \to A C < B D)$
35	12 25 34	mp2and	$⊢ (((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \land ((0 \leq A \land A < B) \land (0 \leq C \land C < D))) \to A C < B D$
36	35	an4s	$⊢ (((A \in ℝ \land B \in ℝ) \land (0 \leq A \land A < B)) \land ((C \in ℝ \land D \in ℝ) \land (0 \leq C \land C < D))) \to A C < B D$

Metamath Proof Explorer

Theorem ltmul12a

Proof