Metamath Proof Explorer

Theorem ltmul1a

Description: Lemma for ltmul1 . Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of Apostol p. 20. (Contributed by NM, 15-May-1999) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		simpl2	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to B \in ℝ$
2		simpl1	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to A \in ℝ$
3	1 2	resubcld	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to B - A \in ℝ$
4		simpl3l	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to C \in ℝ$
5		simpr	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to A < B$
6	2 1	posdifd	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to (A < B \leftrightarrow 0 < B - A)$
7	5 6	mpbid	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to 0 < B - A$
8		simpl3r	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to 0 < C$
9	3 4 7 8	mulgt0d	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to 0 < (B - A) C$
10	1	recnd	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to B \in ℂ$
11	2	recnd	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to A \in ℂ$
12	4	recnd	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to C \in ℂ$
13	10 11 12	subdird	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to (B - A) C = B C - A C$
14	9 13	breqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to 0 < B C - A C$
15	2 4	remulcld	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to A C \in ℝ$
16	1 4	remulcld	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to B C \in ℝ$
17	15 16	posdifd	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to (A C < B C \leftrightarrow 0 < B C - A C)$
18	14 17	mpbird	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to A C < B C$