Metamath Proof Explorer


Theorem div0

Description: Division into zero is zero. (Contributed by NM, 14-Mar-2005) (Proof shortened by SN, 9-Jul-2025)

Ref Expression
Assertion div0 A A 0 0 A = 0

Proof

Step Hyp Ref Expression
1 0cn 0
2 eqid 0 = 0
3 diveq0 0 A A 0 0 A = 0 0 = 0
4 2 3 mpbiri 0 A A 0 0 A = 0
5 1 4 mp3an1 A A 0 0 A = 0