Metamath Proof Explorer

Theorem ltmul1

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

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

Proof

Step	Hyp	Ref	Expression
1		ltmul1a	$⊢ ((A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \land A < B) \to A C < B C$
2	1	ex	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A < B \to A C < B C)$
3		oveq1	$⊢ A = B \to A C = B C$
4	3	a1i	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A = B \to A C = B C)$
5		ltmul1a	$⊢ ((B \in ℝ \land A \in ℝ \land (C \in ℝ \land 0 < C)) \land B < A) \to B C < A C$
6	5	ex	$⊢ (B \in ℝ \land A \in ℝ \land (C \in ℝ \land 0 < C)) \to (B < A \to B C < A C)$
7	6	3com12	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (B < A \to B C < A C)$
8	4 7	orim12d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to ((A = B \lor B < A) \to (A C = B C \lor B C < A C))$
9	8	con3d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (\neg (A C = B C \lor B C < A C) \to \neg (A = B \lor B < A))$
10		simp1	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to A \in ℝ$
11		simp3l	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to C \in ℝ$
12	10 11	remulcld	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to A C \in ℝ$
13		simp2	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to B \in ℝ$
14	13 11	remulcld	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to B C \in ℝ$
15	12 14	lttrid	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A C < B C \leftrightarrow \neg (A C = B C \lor B C < A C))$
16	10 13	lttrid	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A < B \leftrightarrow \neg (A = B \lor B < A))$
17	9 15 16	3imtr4d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A C < B C \to A < B)$
18	2 17	impbid	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A < B \leftrightarrow A C < B C)$