Metamath Proof Explorer


Theorem lemul1i

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

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

Proof

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