Metamath Proof Explorer


Theorem lemul2i

Description: Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999)

Ref Expression
Hypotheses ltplus1.1
|- A e. RR
prodgt0.2
|- B e. RR
ltmul1.3
|- C e. RR
Assertion lemul2i
|- ( 0 < C -> ( A <_ B <-> ( C x. A ) <_ ( C x. B ) ) )

Proof

Step Hyp Ref Expression
1 ltplus1.1
 |-  A e. RR
2 prodgt0.2
 |-  B e. RR
3 ltmul1.3
 |-  C e. RR
4 lemul2
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( C x. A ) <_ ( C x. B ) ) )
5 1 2 4 mp3an12
 |-  ( ( C e. RR /\ 0 < C ) -> ( A <_ B <-> ( C x. A ) <_ ( C x. B ) ) )
6 3 5 mpan
 |-  ( 0 < C -> ( A <_ B <-> ( C x. A ) <_ ( C x. B ) ) )