Metamath Proof Explorer


Theorem ltdiv1i

Description: Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999)

Ref Expression
Hypotheses ltplus1.1
|- A e. RR
prodgt0.2
|- B e. RR
ltmul1.3
|- C e. RR
Assertion ltdiv1i
|- ( 0 < C -> ( A < B <-> ( A / C ) < ( B / 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 ltdiv1
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( A / C ) < ( B / C ) ) )
5 1 2 4 mp3an12
 |-  ( ( C e. RR /\ 0 < C ) -> ( A < B <-> ( A / C ) < ( B / C ) ) )
6 3 5 mpan
 |-  ( 0 < C -> ( A < B <-> ( A / C ) < ( B / C ) ) )