Theorem renegcli 11551

Description: Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 11553 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 11209	. 2 ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
3		recn 11228	. . . . 5 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
4		df-neg 11477	. . . . . . 7 ⊢ -𝐴 = (0 − 𝐴)
5	4	eqeq1i 2730	. . . . . 6 ⊢ (-𝐴 = 𝑥 ↔ (0 − 𝐴) = 𝑥)
6		0cn 11236	. . . . . . 7 ⊢ 0 ∈ ℂ
7	1	recni 11258	. . . . . . 7 ⊢ 𝐴 ∈ ℂ
8		subadd 11493	. . . . . . 7 ⊢ ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
9	6, 7, 8	mp3an12 1447	. . . . . 6 ⊢ (𝑥 ∈ ℂ → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
10	5, 9	bitrid 282	. . . . 5 ⊢ (𝑥 ∈ ℂ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
11	3, 10	syl 17	. . . 4 ⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
12		eleq1a 2820	. . . 4 ⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 → -𝐴 ∈ ℝ))
13	11, 12	sylbird 259	. . 3 ⊢ (𝑥 ∈ ℝ → ((𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ))
14	13	rexlimiv 3138	. 2 ⊢ (∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ)
15	1, 2, 14	mp2b 10	1 ⊢ -𝐴 ∈ ℝ

Syntax hints:   ↔ wb 205   = wceq 1533   ∈ wcel 2098  ∃wrex 3060  (class class class)co 7417  ℂcc 11136  ℝcr 11137  0cc0 11138   + caddc 11141   − cmin 11474  -cneg 11475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428  ax-un 7739  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-riota 7373  df-ov 7420  df-oprab 7421  df-mpo 7422  df-er 8723  df-en 8963  df-dom 8964  df-sdom 8965  df-pnf 11280  df-mnf 11281  df-ltxr 11283  df-sub 11476  df-neg 11477

This theorem is referenced by:  resubcli  11552  renegcl  11553  recgt0ii  12150  inelr  12232  cju  12238  neg1rr  12357  sincos2sgn  16170  dvdslelem  16285  divalglem1  16370  divalglem6  16374  modsubi  17040  neghalfpire  26430  coseq0negpitopi  26468  pige3ALT  26484  negpitopissre  26504  eff1o  26513  ellogrn  26523  logimclad  26536  logi  26551  logneg  26552  logcj  26570  argregt0  26574  argrege0  26575  argimgt0  26576  argimlt0  26577  logimul  26578  logneg2  26579  logcnlem3  26608  dvloglem  26612  logf1o2  26614  efopnlem2  26621  cxpsqrtlem  26666  abscxpbnd  26718  logreclem  26724  ang180lem2  26772  asinneg  26848  asinsin  26854  asin1  26856  asinrecl  26864  atanlogaddlem  26875  atanlogsublem  26877  atanlogsub  26878  atantan  26885  atanbndlem  26887  birthday  26916  ppiub  27167  lgsdir2lem1  27288  ex-fl  30313  ex-ceil  30314  normlem2  30977  logdivsqrle  34352  bj-pinftyccb  36770  bj-minftyccb  36774  bj-pinftynminfty  36776  cos2h  37154  tan2h  37155  renegclALT  38504  fourierdlem5  45563  fourierdlem9  45567  fourierdlem18  45576  fourierdlem24  45582  fourierdlem38  45596  fourierdlem40  45598  fourierdlem43  45601  fourierdlem44  45602  fourierdlem46  45603  fourierdlem50  45607  fourierdlem62  45619  fourierdlem66  45623  fourierdlem74  45631  fourierdlem75  45632  fourierdlem76  45633  fourierdlem77  45634  fourierdlem78  45635  fourierdlem83  45640  fourierdlem85  45642  fourierdlem87  45644  fourierdlem88  45645  fourierdlem93  45650  fourierdlem94  45651  fourierdlem95  45652  fourierdlem101  45658  fourierdlem102  45659  fourierdlem103  45660  fourierdlem104  45661  fourierdlem111  45668  fourierdlem112  45669  fourierdlem113  45670  fourierdlem114  45671  sqwvfoura  45679  sqwvfourb  45680  fouriersw  45682  fouriercn  45683