![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mulne0d | Structured version Visualization version GIF version |
Description: The product of two nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
msq0d.1 | โข (๐ โ ๐ด โ โ) |
mul0ord.2 | โข (๐ โ ๐ต โ โ) |
mulne0d.3 | โข (๐ โ ๐ด โ 0) |
mulne0d.4 | โข (๐ โ ๐ต โ 0) |
Ref | Expression |
---|---|
mulne0d | โข (๐ โ (๐ด ยท ๐ต) โ 0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mulne0d.3 | . 2 โข (๐ โ ๐ด โ 0) | |
2 | mulne0d.4 | . 2 โข (๐ โ ๐ต โ 0) | |
3 | msq0d.1 | . . 3 โข (๐ โ ๐ด โ โ) | |
4 | mul0ord.2 | . . 3 โข (๐ โ ๐ต โ โ) | |
5 | 3, 4 | mulne0bd 11865 | . 2 โข (๐ โ ((๐ด โ 0 โง ๐ต โ 0) โ (๐ด ยท ๐ต) โ 0)) |
6 | 1, 2, 5 | mpbi2and 711 | 1 โข (๐ โ (๐ด ยท ๐ต) โ 0) |
Copyright terms: Public domain | W3C validator |