Metamath Proof Explorer


Theorem dividd

Description: A number divided by itself is one. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses div1d.1 φA
reccld.2 φA0
Assertion dividd φAA=1

Proof

Step Hyp Ref Expression
1 div1d.1 φA
2 reccld.2 φA0
3 divid AA0AA=1
4 1 2 3 syl2anc φAA=1