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