![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mulge0d | Structured version Visualization version GIF version |
Description: The product of two nonnegative numbers is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
leidd.1 | โข (๐ โ ๐ด โ โ) |
ltnegd.2 | โข (๐ โ ๐ต โ โ) |
addge0d.3 | โข (๐ โ 0 โค ๐ด) |
addge0d.4 | โข (๐ โ 0 โค ๐ต) |
Ref | Expression |
---|---|
mulge0d | โข (๐ โ 0 โค (๐ด ยท ๐ต)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | leidd.1 | . 2 โข (๐ โ ๐ด โ โ) | |
2 | addge0d.3 | . 2 โข (๐ โ 0 โค ๐ด) | |
3 | ltnegd.2 | . 2 โข (๐ โ ๐ต โ โ) | |
4 | addge0d.4 | . 2 โข (๐ โ 0 โค ๐ต) | |
5 | mulge0 11674 | . 2 โข (((๐ด โ โ โง 0 โค ๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (๐ด ยท ๐ต)) | |
6 | 1, 2, 3, 4, 5 | syl22anc 838 | 1 โข (๐ โ 0 โค (๐ด ยท ๐ต)) |
Copyright terms: Public domain | W3C validator |