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 11098	. 2 ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
3		recn 11117	. . . . 5 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
4		df-neg 11369	. . . . . . 7 ⊢ -𝐴 = (0 − 𝐴)
5	4	eqeq1i 2740	. . . . . 6 ⊢ (-𝐴 = 𝑥 ↔ (0 − 𝐴) = 𝑥)
6		0cn 11125	. . . . . . 7 ⊢ 0 ∈ ℂ
7	1	recni 11148	. . . . . . 7 ⊢ 𝐴 ∈ ℂ
8		subadd 11385	. . . . . . 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 2830	. . . 4 ⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 → -𝐴 ∈ ℝ))
13	11, 12	sylbird 260	. . 3 ⊢ (𝑥 ∈ ℝ → ((𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ))
14	13	rexlimiv 3129	. 2 ⊢ (∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ)
15	1, 2, 14	mp2b 10	1 ⊢ -𝐴 ∈ ℝ

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

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 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678  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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3060  df-reu 3341  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-po 5528  df-so 5529  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8632  df-en 8883  df-dom 8884  df-sdom 8885  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  12051  neg1rr  12134  cju  12144  sincos2sgn  16150  dvdslelem  16267  divalglem1  16352  divalglem6  16356  modsubi  17032  neghalfpire  26417  coseq0negpitopi  26455  pige3ALT  26472  negpitopissre  26492  eff1o  26501  ellogrn  26511  logimclad  26524  logi  26539  logneg  26540  logcj  26558  argregt0  26562  argrege0  26563  argimgt0  26564  argimlt0  26565  logimul  26566  logneg2  26567  logcnlem3  26596  dvloglem  26600  logf1o2  26602  efopnlem2  26609  cxpsqrtlem  26654  abscxpbnd  26705  logreclem  26714  ang180lem2  26762  asinneg  26838  asinsin  26844  asin1  26846  asinrecl  26854  atanlogaddlem  26865  atanlogsublem  26867  atanlogsub  26868  atantan  26875  atanbndlem  26877  birthday  26906  ppiub  27155  lgsdir2lem1  27276  ex-fl  30505  ex-ceil  30506  normlem2  31170  logdivsqrle  34782  bj-pinftyccb  37523  bj-minftyccb  37527  bj-pinftynminfty  37529  cos2h  37920  tan2h  37921  renegclALT  39397  fourierdlem5  46528  fourierdlem9  46532  fourierdlem18  46541  fourierdlem24  46547  fourierdlem38  46561  fourierdlem40  46563  fourierdlem43  46566  fourierdlem44  46567  fourierdlem46  46568  fourierdlem50  46572  fourierdlem62  46584  fourierdlem66  46588  fourierdlem74  46596  fourierdlem75  46597  fourierdlem76  46598  fourierdlem77  46599  fourierdlem78  46600  fourierdlem83  46605  fourierdlem85  46607  fourierdlem87  46609  fourierdlem88  46610  fourierdlem93  46615  fourierdlem94  46616  fourierdlem95  46617  fourierdlem101  46623  fourierdlem102  46624  fourierdlem103  46625  fourierdlem104  46626  fourierdlem111  46633  fourierdlem112  46634  fourierdlem113  46635  fourierdlem114  46636  sqwvfoura  46644  sqwvfourb  46645  fouriersw  46647  fouriercn  46648  nthrucw  47304