Theorem renegcli 11443

Description: Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 11445 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 11098	. 2 ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
3		recn 11117	. . . . 5 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
4		df-neg 11368	. . . . . . 7 ⊢ -𝐴 = (0 − 𝐴)
5	4	eqeq1i 2742	. . . . . 6 ⊢ (-𝐴 = 𝑥 ↔ (0 − 𝐴) = 𝑥)
6		0cn 11125	. . . . . . 7 ⊢ 0 ∈ ℂ
7	1	recni 11147	. . . . . . 7 ⊢ 𝐴 ∈ ℂ
8		subadd 11384	. . . . . . 7 ⊢ ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
9	6, 7, 8	mp3an12 1454	. . . . . 6 ⊢ (𝑥 ∈ ℂ → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
10	5, 9	bitrid 283	. . . . 5 ⊢ (𝑥 ∈ ℂ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
11	3, 10	syl 17	. . . 4 ⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
12		eleq1a 2832	. . . 4 ⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 → -𝐴 ∈ ℝ))
13	11, 12	sylbird 260	. . 3 ⊢ (𝑥 ∈ ℝ → ((𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ))
14	13	rexlimiv 3132	. 2 ⊢ (∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ)
15	1, 2, 14	mp2b 10	1 ⊢ -𝐴 ∈ ℝ

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  (class class class)co 7358  ℂcc 11025  ℝcr 11026  0cc0 11027   + caddc 11030   − cmin 11365  -cneg 11366

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11169  df-mnf 11170  df-ltxr 11172  df-sub 11367  df-neg 11368

This theorem is referenced by:  resubcli  11444  renegcl  11445  recgt0ii  12049  neg1rr  12132  cju  12142  sincos2sgn  16120  dvdslelem  16237  divalglem1  16322  divalglem6  16326  modsubi  17001  neghalfpire  26414  coseq0negpitopi  26452  pige3ALT  26469  negpitopissre  26489  eff1o  26498  ellogrn  26508  logimclad  26521  logi  26536  logneg  26537  logcj  26555  argregt0  26559  argrege0  26560  argimgt0  26561  argimlt0  26562  logimul  26563  logneg2  26564  logcnlem3  26593  dvloglem  26597  logf1o2  26599  efopnlem2  26606  cxpsqrtlem  26651  abscxpbnd  26703  logreclem  26712  ang180lem2  26760  asinneg  26836  asinsin  26842  asin1  26844  asinrecl  26852  atanlogaddlem  26863  atanlogsublem  26865  atanlogsub  26866  atantan  26873  atanbndlem  26875  birthday  26904  ppiub  27155  lgsdir2lem1  27276  ex-fl  30506  ex-ceil  30507  normlem2  31171  logdivsqrle  34800  bj-pinftyccb  37533  bj-minftyccb  37537  bj-pinftynminfty  37539  cos2h  37923  tan2h  37924  renegclALT  39400  fourierdlem5  46544  fourierdlem9  46548  fourierdlem18  46557  fourierdlem24  46563  fourierdlem38  46577  fourierdlem40  46579  fourierdlem43  46582  fourierdlem44  46583  fourierdlem46  46584  fourierdlem50  46588  fourierdlem62  46600  fourierdlem66  46604  fourierdlem74  46612  fourierdlem75  46613  fourierdlem76  46614  fourierdlem77  46615  fourierdlem78  46616  fourierdlem83  46621  fourierdlem85  46623  fourierdlem87  46625  fourierdlem88  46626  fourierdlem93  46631  fourierdlem94  46632  fourierdlem95  46633  fourierdlem101  46639  fourierdlem102  46640  fourierdlem103  46641  fourierdlem104  46642  fourierdlem111  46649  fourierdlem112  46650  fourierdlem113  46651  fourierdlem114  46652  sqwvfoura  46660  sqwvfourb  46661  fouriersw  46663  fouriercn  46664  nthrucw  47318