This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltmul2d

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

	Ref	Expression
Hypotheses	ltmul1d.1	$⊢ φ \to A \in ℝ$
	ltmul1d.2	$⊢ φ \to B \in ℝ$
	ltmul1d.3	$⊢ φ \to C \in ℝ^{+}$
Assertion	ltmul2d	$⊢ φ \to (A < B \leftrightarrow C A < C B)$

Proof

Step	Hyp	Ref	Expression
1		ltmul1d.1	$⊢ φ \to A \in ℝ$
2		ltmul1d.2	$⊢ φ \to B \in ℝ$
3		ltmul1d.3	$⊢ φ \to C \in ℝ^{+}$
4	3	rpregt0d	$⊢ φ \to (C \in ℝ \land 0 < C)$
5		ltmul2	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A < B \leftrightarrow C A < C B)$
6	1 2 4 5	syl3anc	$⊢ φ \to (A < B \leftrightarrow C A < C B)$