Metamath Proof Explorer


Theorem mulne0b

Description: The product of two nonzero numbers is nonzero. (Contributed by NM, 1-Aug-2004) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion mulne0b ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ( ๐ด โ‰  0 โˆง ๐ต โ‰  0 ) โ†” ( ๐ด ยท ๐ต ) โ‰  0 ) )

Proof

Step Hyp Ref Expression
1 neanior โŠข ( ( ๐ด โ‰  0 โˆง ๐ต โ‰  0 ) โ†” ยฌ ( ๐ด = 0 โˆจ ๐ต = 0 ) )
2 mul0or โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ( ๐ด ยท ๐ต ) = 0 โ†” ( ๐ด = 0 โˆจ ๐ต = 0 ) ) )
3 2 necon3abid โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ( ๐ด ยท ๐ต ) โ‰  0 โ†” ยฌ ( ๐ด = 0 โˆจ ๐ต = 0 ) ) )
4 1 3 bitr4id โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ( ๐ด โ‰  0 โˆง ๐ต โ‰  0 ) โ†” ( ๐ด ยท ๐ต ) โ‰  0 ) )