Metamath Proof Explorer


Theorem lemul12bd

Description: Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016)

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

Proof

Step Hyp Ref Expression
1 ltp1d.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„ )
2 divgt0d.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
3 lemul1ad.3 โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„ )
4 ltmul12ad.3 โŠข ( ๐œ‘ โ†’ ๐ท โˆˆ โ„ )
5 lemul12bd.4 โŠข ( ๐œ‘ โ†’ 0 โ‰ค ๐ด )
6 lemul12bd.5 โŠข ( ๐œ‘ โ†’ 0 โ‰ค ๐ท )
7 lemul12bd.6 โŠข ( ๐œ‘ โ†’ ๐ด โ‰ค ๐ต )
8 lemul12bd.7 โŠข ( ๐œ‘ โ†’ ๐ถ โ‰ค ๐ท )
9 1 5 jca โŠข ( ๐œ‘ โ†’ ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) )
10 4 6 jca โŠข ( ๐œ‘ โ†’ ( ๐ท โˆˆ โ„ โˆง 0 โ‰ค ๐ท ) )
11 lemul12b โŠข ( ( ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โˆง ๐ต โˆˆ โ„ ) โˆง ( ๐ถ โˆˆ โ„ โˆง ( ๐ท โˆˆ โ„ โˆง 0 โ‰ค ๐ท ) ) ) โ†’ ( ( ๐ด โ‰ค ๐ต โˆง ๐ถ โ‰ค ๐ท ) โ†’ ( ๐ด ยท ๐ถ ) โ‰ค ( ๐ต ยท ๐ท ) ) )
12 9 2 3 10 11 syl22anc โŠข ( ๐œ‘ โ†’ ( ( ๐ด โ‰ค ๐ต โˆง ๐ถ โ‰ค ๐ท ) โ†’ ( ๐ด ยท ๐ถ ) โ‰ค ( ๐ต ยท ๐ท ) ) )
13 7 8 12 mp2and โŠข ( ๐œ‘ โ†’ ( ๐ด ยท ๐ถ ) โ‰ค ( ๐ต ยท ๐ท ) )