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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cr	⊢ ℝ
2	0 1	wcel	⊢ 𝐴 ∈ ℝ
3		cc0	⊢ 0
4	0 3	wne	⊢ 𝐴 ≠ 0
5	2 4	wa	⊢ ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 )
6		vx	⊢ 𝑥
7		cmul	⊢ ·
8	6	cv	⊢ 𝑥
9	0 8 7	co	⊢ ( 𝐴 · 𝑥 )
10		c1	⊢ 1
11	9 10	wceq	⊢ ( 𝐴 · 𝑥 ) = 1
12	11 6 1	wrex	⊢ ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1
13	5 12	wi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 )