Metamath Proof Explorer


Theorem ltdiv1dd

Description: Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses ltmul1d.1 φA
ltmul1d.2 φB
ltmul1d.3 φC+
ltdiv1dd.4 φA<B
Assertion ltdiv1dd φAC<BC

Proof

Step Hyp Ref Expression
1 ltmul1d.1 φA
2 ltmul1d.2 φB
3 ltmul1d.3 φC+
4 ltdiv1dd.4 φA<B
5 1 2 3 ltdiv1d φA<BAC<BC
6 4 5 mpbid φAC<BC