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-rnegex
Description: Existence of negative of real number. Axiom 15 of 22 for real and
complex numbers, justified by Theorem axrnegex . (Contributed by Eric
Schmidt , 21-May-2007)
Ref
Expression
Assertion
ax-rnegex ⊢ ( 𝐴 ∈ ℝ → ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cA ⊢ 𝐴
1
cr ⊢ ℝ
2
0 1
wcel ⊢ 𝐴 ∈ ℝ
3
vx ⊢ 𝑥
4
caddc ⊢ +
5
3
cv ⊢ 𝑥
6
0 5 4
co ⊢ ( 𝐴 + 𝑥 )
7
cc0 ⊢ 0
8
6 7
wceq ⊢ ( 𝐴 + 𝑥 ) = 0
9
8 3 1
wrex ⊢ ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0
10
2 9
wi ⊢ ( 𝐴 ∈ ℝ → ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 )