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 B B 0 A B = 0 A = 0

Proof

Step Hyp Ref Expression
1 0cn 0
2 divmul2 A 0 B B 0 A B = 0 A = B 0
3 1 2 mp3an2 A B B 0 A B = 0 A = B 0
4 3 3impb A B B 0 A B = 0 A = B 0
5 simp2 A B B 0 B
6 5 mul01d A B B 0 B 0 = 0
7 6 eqeq2d A B B 0 A = B 0 A = 0
8 4 7 bitrd A B B 0 A B = 0 A = 0