Axiom ax-rrecex

Description: Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, justified by Theorem axrrecex . (Contributed by Eric Schmidt, 11-Apr-2007)

	Ref	Expression
Assertion	ax-rrecex	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to \exists x\in ℝAx=1$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cr	$$classℝ$$
2	0 1	wcel	$$wffA\in ℝ$$
3		cc0	$$class0$$
4	0 3	wne	$$wffA\ne 0$$
5	2 4	wa	$$wff\left(A\in ℝ\wedge A\ne 0\right)$$
6		vx	$$setvarx$$
7		cmul	$$class\times$$
8	6	cv	$$setvarx$$
9	0 8 7	co	$$classAx$$
10		c1	$$class1$$
11	9 10	wceq	$$wffAx=1$$
12	11 6 1	wrex	$$wff\exists x\in ℝAx=1$$
13	5 12	wi	$$wff\left(\left(A\in ℝ\wedge A\ne 0\right)\to \exists x\in ℝAx=1\right)$$