Theorem xrecex

Description: Existence of reciprocal of nonzero real number. (Contributed by Thierry Arnoux, 17-Dec-2016)

	Ref	Expression
Assertion	xrecex	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \exists x\in ℝA{\cdot }_{𝑒}x=1$$

Proof

Step	Hyp	Ref	Expression
1		ax-rrecex	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \exists x\in ℝAx=1$$
2		rexmul	$$⊢\left(A\in ℝ\wedge x\in ℝ\right)\to A{\cdot }_{𝑒}x=Ax$$
3	2	eqeq1d	$$⊢\left(A\in ℝ\wedge x\in ℝ\right)\to \left(A{\cdot }_{𝑒}x=1\leftrightarrow Ax=1\right)$$
4	3	ex	$$⊢A\in ℝ\to \left(x\in ℝ\to \left(A{\cdot }_{𝑒}x=1\leftrightarrow Ax=1\right)\right)$$
5	4	adantr	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(x\in ℝ\to \left(A{\cdot }_{𝑒}x=1\leftrightarrow Ax=1\right)\right)$$
6	5	pm5.32d	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(\left(x\in ℝ\wedge A{\cdot }_{𝑒}x=1\right)\leftrightarrow \left(x\in ℝ\wedge Ax=1\right)\right)$$
7	6	rexbidv2	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \left(\exists x\in ℝA{\cdot }_{𝑒}x=1\leftrightarrow \exists x\in ℝAx=1\right)$$
8	1 7	mpbird	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \exists x\in ℝA{\cdot }_{𝑒}x=1$$