Theorem lemuldiv4d

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

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

Proof

Step	Hyp	Ref	Expression
1		lemuldiv4d.1	|- ( ph -> B <_ ( C / A ) )
2		lemuldiv4d.2	|- ( ph -> 0 < A )
3		lemuldiv4d.3	|- ( ph -> A e. RR )
4		lemuldiv4d.4	|- ( ph -> B e. RR )
5		lemuldiv4d.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	7	bicomd	|- ( ph -> ( B <_ ( C / A ) <-> ( B x. A ) <_ C ) )
9	1 8	mpbid	|- ( ph -> ( B x. A ) <_ C )