Metamath Proof Explorer


Theorem divne0i

Description: The ratio of nonzero numbers is nonzero. (Contributed by NM, 9-Feb-1995)

Ref Expression
Hypotheses divclz.1 A
divclz.2 B
divneq0.3 A 0
divneq0.4 B 0
Assertion divne0i A B 0

Proof

Step Hyp Ref Expression
1 divclz.1 A
2 divclz.2 B
3 divneq0.3 A 0
4 divneq0.4 B 0
5 divne0 A A 0 B B 0 A B 0
6 1 3 2 4 5 mp4an A B 0