Theorem xdiv0rp

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

	Ref	Expression
Assertion	xdiv0rp	⊢ ( 𝐴 ∈ ℝ+ → ( 0 /𝑒 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		rprene0	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) )
2		xdiv0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 0 /𝑒 𝐴 ) = 0 )
3	1 2	syl	⊢ ( 𝐴 ∈ ℝ+ → ( 0 /𝑒 𝐴 ) = 0 )