Metamath Proof Explorer


Axiom 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 )