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	|- ( ph -> A e. RR )
	divlt0gt0d.2	|- ( ph -> B e. RR+ )
	divlt0gt0d.3	|- ( ph -> A < 0 )
Assertion	divlt0gt0d	|- ( ph -> ( A / B ) < 0 )

Proof

Step	Hyp	Ref	Expression
1		divlt0gt0d.1	|- ( ph -> A e. RR )
2		divlt0gt0d.2	|- ( ph -> B e. RR+ )
3		divlt0gt0d.3	|- ( ph -> A < 0 )
4		0red	|- ( ph -> 0 e. RR )
5	1 4	ltnled	|- ( ph -> ( A < 0 <-> -. 0 <_ A ) )
6	3 5	mpbid	|- ( ph -> -. 0 <_ A )
7	1 2	ge0divd	|- ( ph -> ( 0 <_ A <-> 0 <_ ( A / B ) ) )
8	6 7	mtbid	|- ( ph -> -. 0 <_ ( A / B ) )
9	1 2	rerpdivcld	|- ( ph -> ( A / B ) e. RR )
10	9 4	ltnled	|- ( ph -> ( ( A / B ) < 0 <-> -. 0 <_ ( A / B ) ) )
11	8 10	mpbird	|- ( ph -> ( A / B ) < 0 )