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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	divlt0gt0d.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	divlt0gt0d.3	⊢ ( 𝜑 → 𝐴 < 0 )
Assertion	divlt0gt0d	⊢ ( 𝜑 → ( 𝐴 / 𝐵 ) < 0 )

Proof

Step	Hyp	Ref	Expression
1		divlt0gt0d.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		divlt0gt0d.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
3		divlt0gt0d.3	⊢ ( 𝜑 → 𝐴 < 0 )
4		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
5	1 4	ltnled	⊢ ( 𝜑 → ( 𝐴 < 0 ↔ ¬ 0 ≤ 𝐴 ) )
6	3 5	mpbid	⊢ ( 𝜑 → ¬ 0 ≤ 𝐴 )
7	1 2	ge0divd	⊢ ( 𝜑 → ( 0 ≤ 𝐴 ↔ 0 ≤ ( 𝐴 / 𝐵 ) ) )
8	6 7	mtbid	⊢ ( 𝜑 → ¬ 0 ≤ ( 𝐴 / 𝐵 ) )
9	1 2	rerpdivcld	⊢ ( 𝜑 → ( 𝐴 / 𝐵 ) ∈ ℝ )
10	9 4	ltnled	⊢ ( 𝜑 → ( ( 𝐴 / 𝐵 ) < 0 ↔ ¬ 0 ≤ ( 𝐴 / 𝐵 ) ) )
11	8 10	mpbird	⊢ ( 𝜑 → ( 𝐴 / 𝐵 ) < 0 )