Theorem ltdivmul

Description: 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004)

	Ref	Expression
Assertion	ltdivmul	|- ( ( 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		ltdiv1	|- ( ( 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 ) ) )