xdiv0

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

		Ref	Expression
	Assertion	xdiv0	$⊢ (A \in ℝ \land A \neq 0) \to 0 \div_{𝑒} A = 0$

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		rexdiv	$⊢ (0 \in ℝ \land A \in ℝ \land A \neq 0) \to 0 \div_{𝑒} A = \frac{0}{A}$
3	1 2	mp3an1	$⊢ (A \in ℝ \land A \neq 0) \to 0 \div_{𝑒} A = \frac{0}{A}$
4		recn	$⊢ A \in ℝ \to A \in ℂ$
5		div0	$⊢ (A \in ℂ \land A \neq 0) \to \frac{0}{A} = 0$
6	4 5	sylan	$⊢ (A \in ℝ \land A \neq 0) \to \frac{0}{A} = 0$
7	3 6	eqtrd	$⊢ (A \in ℝ \land A \neq 0) \to 0 \div_{𝑒} A = 0$

Metamath Proof Explorer