xdivid

Description: A number divided by itself is one. (Contributed by Thierry Arnoux, 18-Dec-2016)

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

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

Metamath Proof Explorer