Theorem renegcli 11489

Description: Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 11491 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 11145	. 2 ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
3		recn 11164	. . . . 5 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
4		df-neg 11414	. . . . . . 7 ⊢ -𝐴 = (0 − 𝐴)
5	4	eqeq1i 2735	. . . . . 6 ⊢ (-𝐴 = 𝑥 ↔ (0 − 𝐴) = 𝑥)
6		0cn 11172	. . . . . . 7 ⊢ 0 ∈ ℂ
7	1	recni 11194	. . . . . . 7 ⊢ 𝐴 ∈ ℂ
8		subadd 11430	. . . . . . 7 ⊢ ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
9	6, 7, 8	mp3an12 1453	. . . . . 6 ⊢ (𝑥 ∈ ℂ → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
10	5, 9	bitrid 283	. . . . 5 ⊢ (𝑥 ∈ ℂ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
11	3, 10	syl 17	. . . 4 ⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
12		eleq1a 2824	. . . 4 ⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 → -𝐴 ∈ ℝ))
13	11, 12	sylbird 260	. . 3 ⊢ (𝑥 ∈ ℝ → ((𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ))
14	13	rexlimiv 3128	. 2 ⊢ (∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ)
15	1, 2, 14	mp2b 10	1 ⊢ -𝐴 ∈ ℝ

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3054  (class class class)co 7389  ℂcc 11072  ℝcr 11073  0cc0 11074   + caddc 11077   − cmin 11411  -cneg 11412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-po 5548  df-so 5549  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-riota 7346  df-ov 7392  df-oprab 7393  df-mpo 7394  df-er 8673  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11216  df-mnf 11217  df-ltxr 11219  df-sub 11413  df-neg 11414

This theorem is referenced by:  resubcli  11490  renegcl  11491  recgt0ii  12095  inelr  12177  cju  12183  neg1rr  12302  sincos2sgn  16168  dvdslelem  16285  divalglem1  16370  divalglem6  16374  modsubi  17049  neghalfpire  26380  coseq0negpitopi  26418  pige3ALT  26435  negpitopissre  26455  eff1o  26464  ellogrn  26474  logimclad  26487  logi  26502  logneg  26503  logcj  26521  argregt0  26525  argrege0  26526  argimgt0  26527  argimlt0  26528  logimul  26529  logneg2  26530  logcnlem3  26559  dvloglem  26563  logf1o2  26565  efopnlem2  26572  cxpsqrtlem  26617  abscxpbnd  26669  logreclem  26678  ang180lem2  26726  asinneg  26802  asinsin  26808  asin1  26810  asinrecl  26818  atanlogaddlem  26829  atanlogsublem  26831  atanlogsub  26832  atantan  26839  atanbndlem  26841  birthday  26870  ppiub  27121  lgsdir2lem1  27242  ex-fl  30382  ex-ceil  30383  normlem2  31046  logdivsqrle  34647  bj-pinftyccb  37204  bj-minftyccb  37208  bj-pinftynminfty  37210  cos2h  37600  tan2h  37601  renegclALT  38951  fourierdlem5  46103  fourierdlem9  46107  fourierdlem18  46116  fourierdlem24  46122  fourierdlem38  46136  fourierdlem40  46138  fourierdlem43  46141  fourierdlem44  46142  fourierdlem46  46143  fourierdlem50  46147  fourierdlem62  46159  fourierdlem66  46163  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem77  46174  fourierdlem78  46175  fourierdlem83  46180  fourierdlem85  46182  fourierdlem87  46184  fourierdlem88  46185  fourierdlem93  46190  fourierdlem94  46191  fourierdlem95  46192  fourierdlem101  46198  fourierdlem102  46199  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  fourierdlem112  46209  fourierdlem113  46210  fourierdlem114  46211  sqwvfoura  46219  sqwvfourb  46220  fouriersw  46222  fouriercn  46223