Theorem xdiv0rp

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

	Ref	Expression
Assertion	xdiv0rp	$$⊢A\in {ℝ}^{+}\to 0{÷}_{𝑒}A=0$$

Proof

Step	Hyp	Ref	Expression
1		rprene0	$$⊢A\in {ℝ}^{+}\to \left(A\in ℝ\wedge A\ne 0\right)$$
2		xdiv0	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to 0{÷}_{𝑒}A=0$$
3	1 2	syl	$$⊢A\in {ℝ}^{+}\to 0{÷}_{𝑒}A=0$$