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

Metamath Proof Explorer

Theorem divgt0i

Description: The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999)

Step	Hyp	Ref	Expression
1		ltplus1.1	$⊢ A \in ℝ$
2		prodgt0.2	$⊢ B \in ℝ$
3		divgt0	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to 0 < \frac{A}{B}$
4	2 3	mpanr1	$⊢ ((A \in ℝ \land 0 < A) \land 0 < B) \to 0 < \frac{A}{B}$
5	1 4	mpanl1	$⊢ (0 < A \land 0 < B) \to 0 < \frac{A}{B}$