Theorem lemul1

Description: Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 21-Feb-2005)

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

Proof

Step	Hyp	Ref	Expression
1		ltmul1	|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( A x. C ) < ( B x. C ) ) )
2		recn	|- ( A e. RR -> A e. CC )
3		recn	|- ( B e. RR -> B e. CC )
4		recn	|- ( C e. RR -> C e. CC )
5	4	adantr	|- ( ( C e. RR /\ 0 < C ) -> C e. CC )
6		gt0ne0	|- ( ( C e. RR /\ 0 < C ) -> C =/= 0 )
7	5 6	jca	|- ( ( C e. RR /\ 0 < C ) -> ( C e. CC /\ C =/= 0 ) )
8		mulcan2	|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A x. C ) = ( B x. C ) <-> A = B ) )
9	2 3 7 8	syl3an	|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) = ( B x. C ) <-> A = B ) )
10	9	bicomd	|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A = B <-> ( A x. C ) = ( B x. C ) ) )
11	1 10	orbi12d	|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A < B \/ A = B ) <-> ( ( A x. C ) < ( B x. C ) \/ ( A x. C ) = ( B x. C ) ) ) )
12		leloe	|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
13	12	3adant3	|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
14		remulcl	|- ( ( A e. RR /\ C e. RR ) -> ( A x. C ) e. RR )
15	14	3adant2	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. C ) e. RR )
16		remulcl	|- ( ( B e. RR /\ C e. RR ) -> ( B x. C ) e. RR )
17	16	3adant1	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B x. C ) e. RR )
18	15 17	leloed	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <_ ( B x. C ) <-> ( ( A x. C ) < ( B x. C ) \/ ( A x. C ) = ( B x. C ) ) ) )
19	18	3adant3r	|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) <_ ( B x. C ) <-> ( ( A x. C ) < ( B x. C ) \/ ( A x. C ) = ( B x. C ) ) ) )
20	11 13 19	3bitr4d	|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( A x. C ) <_ ( B x. C ) ) )