Theorem ledivmul

Description: 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005)

	Ref	Expression
Assertion	ledivmul	|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) <_ B <-> A <_ ( C x. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		remulcl	|- ( ( C e. RR /\ B e. RR ) -> ( C x. B ) e. RR )
2	1	ancoms	|- ( ( B e. RR /\ C e. RR ) -> ( C x. B ) e. RR )
3	2	adantrr	|- ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( C x. B ) e. RR )
4	3	3adant1	|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( C x. B ) e. RR )
5		lediv1	|- ( ( A e. RR /\ ( C x. B ) e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ ( C x. B ) <-> ( A / C ) <_ ( ( C x. B ) / C ) ) )
6	4 5	syld3an2	|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ ( C x. B ) <-> ( A / C ) <_ ( ( C x. B ) / C ) ) )
7		recn	|- ( B e. RR -> B e. CC )
8	7	adantr	|- ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> B e. CC )
9		recn	|- ( C e. RR -> C e. CC )
10	9	ad2antrl	|- ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C e. CC )
11		gt0ne0	|- ( ( C e. RR /\ 0 < C ) -> C =/= 0 )
12	11	adantl	|- ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C =/= 0 )
13	8 10 12	divcan3d	|- ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( C x. B ) / C ) = B )
14	13	3adant1	|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( C x. B ) / C ) = B )
15	14	breq2d	|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) <_ ( ( C x. B ) / C ) <-> ( A / C ) <_ B ) )
16	6 15	bitr2d	|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) <_ B <-> A <_ ( C x. B ) ) )