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

Metamath Proof Explorer

Theorem ltdiv1ii

Description: Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999)

	Ref	Expression
Hypotheses	ltplus1.1	$⊢ A \in ℝ$
	prodgt0.2	$⊢ B \in ℝ$
	ltmul1.3	$⊢ C \in ℝ$
	ltmul1i.4	$⊢ 0 < C$
Assertion	ltdiv1ii	$⊢ A < B \leftrightarrow \frac{A}{C} < \frac{B}{C}$

Step	Hyp	Ref	Expression
1		ltplus1.1	$⊢ A \in ℝ$
2		prodgt0.2	$⊢ B \in ℝ$
3		ltmul1.3	$⊢ C \in ℝ$
4		ltmul1i.4	$⊢ 0 < C$
5	1 2 3	ltdiv1i	$⊢ 0 < C \to (A < B \leftrightarrow \frac{A}{C} < \frac{B}{C})$
6	4 5	ax-mp	$⊢ A < B \leftrightarrow \frac{A}{C} < \frac{B}{C}$