Theorem divlt0gt0d

Description: The ratio of a negative numerator and a positive denominator is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	divlt0gt0d.1	$$⊢\phi \to A\in ℝ$$
	divlt0gt0d.2	$$⊢\phi \to B\in {ℝ}^{+}$$
	divlt0gt0d.3	$$⊢\phi \to A<0$$
Assertion	divlt0gt0d	$$⊢\phi \to \frac{A}{B}<0$$

Proof

Step	Hyp	Ref	Expression
1		divlt0gt0d.1	$$⊢\phi \to A\in ℝ$$
2		divlt0gt0d.2	$$⊢\phi \to B\in {ℝ}^{+}$$
3		divlt0gt0d.3	$$⊢\phi \to A<0$$
4		0red	$$⊢\phi \to 0\in ℝ$$
5	1 4	ltnled	$$⊢\phi \to \left(A<0\leftrightarrow \neg 0\le A\right)$$
6	3 5	mpbid	$$⊢\phi \to \neg 0\le A$$
7	1 2	ge0divd	$$⊢\phi \to \left(0\le A\leftrightarrow 0\le \frac{A}{B}\right)$$
8	6 7	mtbid	$$⊢\phi \to \neg 0\le \frac{A}{B}$$
9	1 2	rerpdivcld	$$⊢\phi \to \frac{A}{B}\in ℝ$$
10	9 4	ltnled	$$⊢\phi \to \left(\frac{A}{B}<0\leftrightarrow \neg 0\le \frac{A}{B}\right)$$
11	8 10	mpbird	$$⊢\phi \to \frac{A}{B}<0$$