Metamath Proof Explorer


Theorem dividi

Description: A number divided by itself is one. (Contributed by NM, 9-Feb-1995)

Ref Expression
Hypotheses divclz.1 A
reccl.2 A0
Assertion dividi AA=1

Proof

Step Hyp Ref Expression
1 divclz.1 A
2 reccl.2 A0
3 divid AA0AA=1
4 1 2 3 mp2an AA=1