Metamath Proof Explorer


Theorem ltdivmuld

Description: 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses ltmul1d.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
ltmul1d.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
ltmul1d.3 โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„+ )
Assertion ltdivmuld ( ๐œ‘ โ†’ ( ( ๐ด / ๐ถ ) < ๐ต โ†” ๐ด < ( ๐ถ ยท ๐ต ) ) )

Proof

Step Hyp Ref Expression
1 ltmul1d.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
2 ltmul1d.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
3 ltmul1d.3 โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„+ )
4 3 rpregt0d โŠข ( ๐œ‘ โ†’ ( ๐ถ โˆˆ โ„ โˆง 0 < ๐ถ ) )
5 ltdivmul โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ( ๐ถ โˆˆ โ„ โˆง 0 < ๐ถ ) ) โ†’ ( ( ๐ด / ๐ถ ) < ๐ต โ†” ๐ด < ( ๐ถ ยท ๐ต ) ) )
6 1 2 4 5 syl3anc โŠข ( ๐œ‘ โ†’ ( ( ๐ด / ๐ถ ) < ๐ต โ†” ๐ด < ( ๐ถ ยท ๐ต ) ) )