Theorem xdiv0

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

	Ref	Expression
Assertion	xdiv0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 0 /𝑒 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		rexdiv	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 0 /𝑒 𝐴 ) = ( 0 / 𝐴 ) )
3	1 2	mp3an1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 0 /𝑒 𝐴 ) = ( 0 / 𝐴 ) )
4		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
5		div0	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 0 / 𝐴 ) = 0 )
6	4 5	sylan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 0 / 𝐴 ) = 0 )
7	3 6	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 0 /𝑒 𝐴 ) = 0 )