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 
|- ( ( A e. CC /\ B e. CC ) -> ( ( A =/= 0 /\ B =/= 0 ) <-> ( A x. B ) =/= 0 ) )

Proof

Step Hyp Ref Expression
1 neanior 
 |-  ( ( A =/= 0 /\ B =/= 0 ) <-> -. ( A = 0 \/ B = 0 ) )
2 mul0or 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) = 0 <-> ( A = 0 \/ B = 0 ) ) )
3 2 necon3abid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) =/= 0 <-> -. ( A = 0 \/ B = 0 ) ) )
4 1 3 bitr4id 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A =/= 0 /\ B =/= 0 ) <-> ( A x. B ) =/= 0 ) )