divgt0

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

		Ref	Expression
	Assertion	divgt0	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to 0 < \frac{A}{B}$

Step	Hyp	Ref	Expression
1		gt0div	$⊢ (A \in ℝ \land B \in ℝ \land 0 < B) \to (0 < A \leftrightarrow 0 < \frac{A}{B})$
2	1	biimpd	$⊢ (A \in ℝ \land B \in ℝ \land 0 < B) \to (0 < A \to 0 < \frac{A}{B})$
3	2	3exp	$⊢ A \in ℝ \to (B \in ℝ \to (0 < B \to (0 < A \to 0 < \frac{A}{B})))$
4	3	com34	$⊢ A \in ℝ \to (B \in ℝ \to (0 < A \to (0 < B \to 0 < \frac{A}{B})))$
5	4	com23	$⊢ A \in ℝ \to (0 < A \to (B \in ℝ \to (0 < B \to 0 < \frac{A}{B})))$
6	5	imp43	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to 0 < \frac{A}{B}$

Metamath Proof Explorer