Metamath Proof Explorer


Theorem lemul2d

Description: Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016)

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

Proof

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