Theorem renegcli 11444

Description: Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 11446 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 11099	. 2 ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
3		recn 11118	. . . . 5 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
4		df-neg 11369	. . . . . . 7 ⊢ -𝐴 = (0 − 𝐴)
5	4	eqeq1i 2734	. . . . . 6 ⊢ (-𝐴 = 𝑥 ↔ (0 − 𝐴) = 𝑥)
6		0cn 11126	. . . . . . 7 ⊢ 0 ∈ ℂ
7	1	recni 11148	. . . . . . 7 ⊢ 𝐴 ∈ ℂ
8		subadd 11385	. . . . . . 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 2823	. . . 4 ⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 → -𝐴 ∈ ℝ))
13	11, 12	sylbird 260	. . 3 ⊢ (𝑥 ∈ ℝ → ((𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ))
14	13	rexlimiv 3123	. 2 ⊢ (∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ)
15	1, 2, 14	mp2b 10	1 ⊢ -𝐴 ∈ ℝ

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  (class class class)co 7353  ℂcc 11026  ℝcr 11027  0cc0 11028   + caddc 11031   − cmin 11366  -cneg 11367

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 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-ltxr 11173  df-sub 11368  df-neg 11369

This theorem is referenced by:  resubcli  11445  renegcl  11446  recgt0ii  12050  neg1rr  12133  cju  12143  sincos2sgn  16122  dvdslelem  16239  divalglem1  16324  divalglem6  16328  modsubi  17003  neghalfpire  26391  coseq0negpitopi  26429  pige3ALT  26446  negpitopissre  26466  eff1o  26475  ellogrn  26485  logimclad  26498  logi  26513  logneg  26514  logcj  26532  argregt0  26536  argrege0  26537  argimgt0  26538  argimlt0  26539  logimul  26540  logneg2  26541  logcnlem3  26570  dvloglem  26574  logf1o2  26576  efopnlem2  26583  cxpsqrtlem  26628  abscxpbnd  26680  logreclem  26689  ang180lem2  26737  asinneg  26813  asinsin  26819  asin1  26821  asinrecl  26829  atanlogaddlem  26840  atanlogsublem  26842  atanlogsub  26843  atantan  26850  atanbndlem  26852  birthday  26881  ppiub  27132  lgsdir2lem1  27253  ex-fl  30410  ex-ceil  30411  normlem2  31074  logdivsqrle  34637  bj-pinftyccb  37214  bj-minftyccb  37218  bj-pinftynminfty  37220  cos2h  37610  tan2h  37611  renegclALT  38961  fourierdlem5  46113  fourierdlem9  46117  fourierdlem18  46126  fourierdlem24  46132  fourierdlem38  46146  fourierdlem40  46148  fourierdlem43  46151  fourierdlem44  46152  fourierdlem46  46153  fourierdlem50  46157  fourierdlem62  46169  fourierdlem66  46173  fourierdlem74  46181  fourierdlem75  46182  fourierdlem76  46183  fourierdlem77  46184  fourierdlem78  46185  fourierdlem83  46190  fourierdlem85  46192  fourierdlem87  46194  fourierdlem88  46195  fourierdlem93  46200  fourierdlem94  46201  fourierdlem95  46202  fourierdlem101  46208  fourierdlem102  46209  fourierdlem103  46210  fourierdlem104  46211  fourierdlem111  46218  fourierdlem112  46219  fourierdlem113  46220  fourierdlem114  46221  sqwvfoura  46229  sqwvfourb  46230  fouriersw  46232  fouriercn  46233