Metamath Proof Explorer


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 )