Metamath Proof Explorer


Theorem divid

Description: A number divided by itself is one. (Contributed by NM, 1-Aug-2004) (Proof shortened by SN, 9-Jul-2025)

Ref Expression
Assertion divid A A 0 A A = 1

Proof

Step Hyp Ref Expression
1 eqid A = A
2 diveq1 A A A 0 A A = 1 A = A
3 1 2 mpbiri A A A 0 A A = 1
4 3 3anidm12 A A 0 A A = 1