Metamath Proof Explorer


Theorem divcli

Description: Closure law for division. (Contributed by NM, 2-Feb-1995) (Revised by Mario Carneiro, 17-Feb-2014)

Ref Expression
Hypotheses divclz.1 A
divclz.2 B
divcl.3 B 0
Assertion divcli A B

Proof

Step Hyp Ref Expression
1 divclz.1 A
2 divclz.2 B
3 divcl.3 B 0
4 1 2 divclzi B 0 A B
5 3 4 ax-mp A B