Theorem renegcli 11517

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

Hypothesis

Ref	Expression
renegcl.1	⊢ 𝐴 ∈ ℝ

Assertion

Ref	Expression
renegcli	⊢ -𝐴 ∈ ℝ

Proof of Theorem renegcli

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		renegcl.1	. 2 ⊢ 𝐴 ∈ ℝ
2		ax-rnegex 11177	. 2 ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
3		recn 11196	. . . . 5 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
4		df-neg 11443	. . . . . . 7 ⊢ -𝐴 = (0 − 𝐴)
5	4	eqeq1i 2737	. . . . . 6 ⊢ (-𝐴 = 𝑥 ↔ (0 − 𝐴) = 𝑥)
6		0cn 11202	. . . . . . 7 ⊢ 0 ∈ ℂ
7	1	recni 11224	. . . . . . 7 ⊢ 𝐴 ∈ ℂ
8		subadd 11459	. . . . . . 7 ⊢ ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
9	6, 7, 8	mp3an12 1451	. . . . . 6 ⊢ (𝑥 ∈ ℂ → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
10	5, 9	bitrid 282	. . . . 5 ⊢ (𝑥 ∈ ℂ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
11	3, 10	syl 17	. . . 4 ⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
12		eleq1a 2828	. . . 4 ⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 → -𝐴 ∈ ℝ))
13	11, 12	sylbird 259	. . 3 ⊢ (𝑥 ∈ ℝ → ((𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ))
14	13	rexlimiv 3148	. 2 ⊢ (∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ)
15	1, 2, 14	mp2b 10	1 ⊢ -𝐴 ∈ ℝ

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∃wrex 3070  (class class class)co 7405  ℂcc 11104  ℝcr 11105  0cc0 11106   + caddc 11109   − cmin 11440  -cneg 11441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11442  df-neg 11443

This theorem is referenced by:  resubcli  11518  renegcl  11519  recgt0ii  12116  inelr  12198  cju  12204  neg1rr  12323  sincos2sgn  16133  dvdslelem  16248  divalglem1  16333  divalglem6  16337  modsubi  17001  neghalfpire  25966  coseq0negpitopi  26004  pige3ALT  26020  negpitopissre  26040  eff1o  26049  ellogrn  26059  logimclad  26072  logneg  26087  logcj  26105  argregt0  26109  argrege0  26110  argimgt0  26111  argimlt0  26112  logimul  26113  logneg2  26114  logcnlem3  26143  dvloglem  26147  logf1o2  26149  efopnlem2  26156  cxpsqrtlem  26201  abscxpbnd  26250  logreclem  26256  ang180lem2  26304  asinneg  26380  asinsin  26386  asin1  26388  asinrecl  26396  atanlogaddlem  26407  atanlogsublem  26409  atanlogsub  26410  atantan  26417  atanbndlem  26419  birthday  26448  ppiub  26696  lgsdir2lem1  26817  ex-fl  29689  ex-ceil  29690  normlem2  30351  logdivsqrle  33650  logi  34692  bj-pinftyccb  36090  bj-minftyccb  36094  bj-pinftynminfty  36096  cos2h  36467  tan2h  36468  renegclALT  37821  fourierdlem5  44814  fourierdlem9  44818  fourierdlem18  44827  fourierdlem24  44833  fourierdlem38  44847  fourierdlem40  44849  fourierdlem43  44852  fourierdlem44  44853  fourierdlem46  44854  fourierdlem50  44858  fourierdlem62  44870  fourierdlem66  44874  fourierdlem74  44882  fourierdlem75  44883  fourierdlem76  44884  fourierdlem77  44885  fourierdlem78  44886  fourierdlem83  44891  fourierdlem85  44893  fourierdlem87  44895  fourierdlem88  44896  fourierdlem93  44901  fourierdlem94  44902  fourierdlem95  44903  fourierdlem101  44909  fourierdlem102  44910  fourierdlem103  44911  fourierdlem104  44912  fourierdlem111  44919  fourierdlem112  44920  fourierdlem113  44921  fourierdlem114  44922  sqwvfoura  44930  sqwvfourb  44931  fouriersw  44933  fouriercn  44934