Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ax-rnegex | Structured version Visualization version GIF version |
Description: Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, justified by theorem axrnegex 10573. (Contributed by Eric Schmidt, 21-May-2007.) |
Ref | Expression |
---|---|
ax-rnegex | ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cr 10525 | . . 3 class ℝ | |
3 | 1, 2 | wcel 2105 | . 2 wff 𝐴 ∈ ℝ |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1527 | . . . . 5 class 𝑥 |
6 | caddc 10529 | . . . . 5 class + | |
7 | 1, 5, 6 | co 7145 | . . . 4 class (𝐴 + 𝑥) |
8 | cc0 10526 | . . . 4 class 0 | |
9 | 7, 8 | wceq 1528 | . . 3 wff (𝐴 + 𝑥) = 0 |
10 | 9, 4, 2 | wrex 3139 | . 2 wff ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 |
11 | 3, 10 | wi 4 | 1 wff (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) |
Colors of variables: wff setvar class |
This axiom is referenced by: 0re 10632 00id 10804 addid1 10809 cnegex 10810 0cnALT 10863 renegcli 10936 elre0re 39034 renegeu 39080 |
Copyright terms: Public domain | W3C validator |