Theorem lemuldiv3d

Description: 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	lemuldiv3d.1	|- ( ph -> ( B x. A ) <_ C )
	lemuldiv3d.2	|- ( ph -> 0 < A )
	lemuldiv3d.3	|- ( ph -> A e. RR )
	lemuldiv3d.4	|- ( ph -> B e. RR )
	lemuldiv3d.5	|- ( ph -> C e. RR )
Assertion	lemuldiv3d	|- ( ph -> B <_ ( C / A ) )

Proof

Step	Hyp	Ref	Expression
1		lemuldiv3d.1	|- ( ph -> ( B x. A ) <_ C )
2		lemuldiv3d.2	|- ( ph -> 0 < A )
3		lemuldiv3d.3	|- ( ph -> A e. RR )
4		lemuldiv3d.4	|- ( ph -> B e. RR )
5		lemuldiv3d.5	|- ( ph -> C e. RR )
6		lemuldiv	|- ( ( B e. RR /\ C e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( B x. A ) <_ C <-> B <_ ( C / A ) ) )
7	4 5 3 2 6	syl112anc	|- ( ph -> ( ( B x. A ) <_ C <-> B <_ ( C / A ) ) )
8	1 7	mpbid	|- ( ph -> B <_ ( C / A ) )