Metamath Proof Explorer


Theorem ltdiv2dd

Description: Division of a positive number by both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ltdiv2dd.a
|- ( ph -> A e. RR+ )
ltdiv2dd.b
|- ( ph -> B e. RR+ )
ltdiv2dd.c
|- ( ph -> C e. RR+ )
ltdiv2dd.altb
|- ( ph -> A < B )
Assertion ltdiv2dd
|- ( ph -> ( C / B ) < ( C / A ) )

Proof

Step Hyp Ref Expression
1 ltdiv2dd.a
 |-  ( ph -> A e. RR+ )
2 ltdiv2dd.b
 |-  ( ph -> B e. RR+ )
3 ltdiv2dd.c
 |-  ( ph -> C e. RR+ )
4 ltdiv2dd.altb
 |-  ( ph -> A < B )
5 1 2 3 ltdiv2d
 |-  ( ph -> ( A < B <-> ( C / B ) < ( C / A ) ) )
6 4 5 mpbid
 |-  ( ph -> ( C / B ) < ( C / A ) )