Metamath Proof Explorer

Theorem diveq0

Description: A ratio is zero iff the numerator is zero. (Contributed by NM, 20-Apr-2006) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> A e. CC )
2 0cnd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> 0 e. CC )
3 3simpc 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B e. CC /\ B =/= 0 ) )
4 divmul2 
 |-  ( ( A e. CC /\ 0 e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) = 0 <-> A = ( B x. 0 ) ) )
5 1 2 3 4 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = 0 <-> A = ( B x. 0 ) ) )
6 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> B e. CC )
7 6 mul01d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B x. 0 ) = 0 )
8 7 eqeq2d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A = ( B x. 0 ) <-> A = 0 ) )
9 5 8 bitrd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) = 0 <-> A = 0 ) )