Metamath Proof Explorer


Theorem lemul2ad

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

Ref Expression
Hypotheses ltp1d.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
divgt0d.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
lemul1ad.3 โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„ )
lemul1ad.4 โŠข ( ๐œ‘ โ†’ 0 โ‰ค ๐ถ )
lemul1ad.5 โŠข ( ๐œ‘ โ†’ ๐ด โ‰ค ๐ต )
Assertion lemul2ad ( ๐œ‘ โ†’ ( ๐ถ ยท ๐ด ) โ‰ค ( ๐ถ ยท ๐ต ) )

Proof

Step Hyp Ref Expression
1 ltp1d.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
2 divgt0d.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
3 lemul1ad.3 โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„ )
4 lemul1ad.4 โŠข ( ๐œ‘ โ†’ 0 โ‰ค ๐ถ )
5 lemul1ad.5 โŠข ( ๐œ‘ โ†’ ๐ด โ‰ค ๐ต )
6 3 4 jca โŠข ( ๐œ‘ โ†’ ( ๐ถ โˆˆ โ„ โˆง 0 โ‰ค ๐ถ ) )
7 lemul2a โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ( ๐ถ โˆˆ โ„ โˆง 0 โ‰ค ๐ถ ) ) โˆง ๐ด โ‰ค ๐ต ) โ†’ ( ๐ถ ยท ๐ด ) โ‰ค ( ๐ถ ยท ๐ต ) )
8 1 2 6 5 7 syl31anc โŠข ( ๐œ‘ โ†’ ( ๐ถ ยท ๐ด ) โ‰ค ( ๐ถ ยท ๐ต ) )