lt2mul2divd

Description: The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016)

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

Step	Hyp	Ref	Expression
1		lt2mul2divd.1	$⊢ φ \to A \in ℝ$
2		lt2mul2divd.2	$⊢ φ \to B \in ℝ^{+}$
3		lt2mul2divd.3	$⊢ φ \to C \in ℝ$
4		lt2mul2divd.4	$⊢ φ \to D \in ℝ^{+}$
5	2	rpregt0d	$⊢ φ \to (B \in ℝ \land 0 < B)$
6	4	rpregt0d	$⊢ φ \to (D \in ℝ \land 0 < D)$
7		lt2mul2div	$⊢ ((A \in ℝ \land (B \in ℝ \land 0 < B)) \land (C \in ℝ \land (D \in ℝ \land 0 < D))) \to (A B < C D \leftrightarrow \frac{A}{D} < \frac{C}{B})$
8	1 5 3 6 7	syl22anc	$⊢ φ \to (A B < C D \leftrightarrow \frac{A}{D} < \frac{C}{B})$

Metamath Proof Explorer