This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Construction and axiomatization of real and complex numbers Real and complex number postulates restated as axioms 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 )