Metamath Proof Explorer


Theorem divne0b

Description: The ratio of nonzero numbers is nonzero. (Contributed by NM, 2-Aug-2004) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion divne0b
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A =/= 0 <-> ( A / B ) =/= 0 ) )

Proof

Step Hyp Ref Expression
1 diveq0
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = 0 <-> A = 0 ) )
2 1 bicomd
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A = 0 <-> ( A / B ) = 0 ) )
3 2 necon3bid
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A =/= 0 <-> ( A / B ) =/= 0 ) )