Metamath Proof Explorer


Theorem xdiv0

Description: Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016)

Ref Expression
Assertion xdiv0 A A 0 0 ÷ 𝑒 A = 0

Proof

Step Hyp Ref Expression
1 0re 0
2 rexdiv 0 A A 0 0 ÷ 𝑒 A = 0 A
3 1 2 mp3an1 A A 0 0 ÷ 𝑒 A = 0 A
4 recn A A
5 div0 A A 0 0 A = 0
6 4 5 sylan A A 0 0 A = 0
7 3 6 eqtrd A A 0 0 ÷ 𝑒 A = 0