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

Metamath Proof Explorer

Theorem lemul2i

Description: Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999)

	Ref	Expression
Hypotheses	ltplus1.1	$⊢ A \in ℝ$
	prodgt0.2	$⊢ B \in ℝ$
	ltmul1.3	$⊢ C \in ℝ$
Assertion	lemul2i	$⊢ 0 < C \to (A \leq B \leftrightarrow C A \leq C B)$

Step	Hyp	Ref	Expression
1		ltplus1.1	$⊢ A \in ℝ$
2		prodgt0.2	$⊢ B \in ℝ$
3		ltmul1.3	$⊢ C \in ℝ$
4		lemul2	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A \leq B \leftrightarrow C A \leq C B)$
5	1 2 4	mp3an12	$⊢ (C \in ℝ \land 0 < C) \to (A \leq B \leftrightarrow C A \leq C B)$
6	3 5	mpan	$⊢ 0 < C \to (A \leq B \leftrightarrow C A \leq C B)$