Metamath Proof Explorer

Theorem renegcli

Description: Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl is deprecated, but is retained for its demonstration value.) (Contributed by NM, 17-Jan-1997) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Hypothesis renegcl.1 ${⊢}{A}\in ℝ$
Assertion renegcli ${⊢}-{A}\in ℝ$

Proof

Step Hyp Ref Expression
1 renegcl.1 ${⊢}{A}\in ℝ$
2 ax-rnegex ${⊢}{A}\in ℝ\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{A}+{x}=0$
3 recn ${⊢}{x}\in ℝ\to {x}\in ℂ$
4 df-neg ${⊢}-{A}=0-{A}$
5 4 eqeq1i ${⊢}-{A}={x}↔0-{A}={x}$
6 0cn ${⊢}0\in ℂ$
7 1 recni ${⊢}{A}\in ℂ$
8 subadd ${⊢}\left(0\in ℂ\wedge {A}\in ℂ\wedge {x}\in ℂ\right)\to \left(0-{A}={x}↔{A}+{x}=0\right)$
9 6 7 8 mp3an12 ${⊢}{x}\in ℂ\to \left(0-{A}={x}↔{A}+{x}=0\right)$
10 5 9 syl5bb ${⊢}{x}\in ℂ\to \left(-{A}={x}↔{A}+{x}=0\right)$
11 3 10 syl ${⊢}{x}\in ℝ\to \left(-{A}={x}↔{A}+{x}=0\right)$
12 eleq1a ${⊢}{x}\in ℝ\to \left(-{A}={x}\to -{A}\in ℝ\right)$
13 11 12 sylbird ${⊢}{x}\in ℝ\to \left({A}+{x}=0\to -{A}\in ℝ\right)$
14 13 rexlimiv ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}{A}+{x}=0\to -{A}\in ℝ$
15 1 2 14 mp2b ${⊢}-{A}\in ℝ$