Theorem lt2mul2divd

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

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

Proof

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