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
|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 cr
 |-  RR
2 0 1 wcel
 |-  A e. RR
3 vx
 |-  x
4 caddc
 |-  +
5 3 cv
 |-  x
6 0 5 4 co
 |-  ( A + x )
7 cc0
 |-  0
8 6 7 wceq
 |-  ( A + x ) = 0
9 8 3 1 wrex
 |-  E. x e. RR ( A + x ) = 0
10 2 9 wi
 |-  ( A e. RR -> E. x e. RR ( A + x ) = 0 )