Theorem renegcli 11646

Description: Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 11648 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 11298	. 2 ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
3		recn 11317	. . . . 5 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
4		df-neg 11571	. . . . . . 7 ⊢ -𝐴 = (0 − 𝐴)
5	4	eqeq1i 2768	. . . . . 6 ⊢ ( -𝐴 = 𝑥 ↔ (0 − 𝐴) = 𝑥)
6		0cn 11325	. . . . . . 7 ⊢ 0 ∈ ℂ
7	1	recni 11350	. . . . . . 7 ⊢ 𝐴 ∈ ℂ
8		subadd 11587	. . . . . . 7 ⊢ ((0 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
9	6, 7, 8	mp3an12 1481	. . . . . 6 ⊢ (𝑥 ∈ ℂ → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0))
10	5, 9	bitrid 286	. . . . 5 ⊢ (𝑥 ∈ ℂ → ( -𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
11	3, 10	syl 18	. . . 4 ⊢ (𝑥 ∈ ℝ → ( -𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0))
12		eleq1a 2859	. . . 4 ⊢ (𝑥 ∈ ℝ → ( -𝐴 = 𝑥 → -𝐴 ∈ ℝ))
13	11, 12	sylbird 263	. . 3 ⊢ (𝑥 ∈ ℝ → ((𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ))
14	13	rexlimiv 3160	. 2 ⊢ (∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ)
15	1, 2, 14	mp2b 10	1 ⊢ -𝐴 ∈ ℝ

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2147  ∃wrex 3090  (class class class)co 7443  ℂcc 11225  ℝcr 11226  0cc0 11227   + caddc 11230   − cmin 11568   -cneg 11569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-ltxr 11375  df-sub 11570  df-neg 11571

This theorem is used by:  resubcli  11647  renegcl  11648  recgt0ii  12250  neg1rr  12333  cju  12343  sincos2sgn  16391  dvdslelem  16508  divalglem1  16593  divalglem6  16597  modsubi  17279  neghalfpire  26824  coseq0negpitopi  26862  pige3ALT  26878  negpitopissre  26898  eff1o  26907  ellogrn  26917  logimclad  26930  logi  26945  logneg  26946  logcj  26964  argregt0  26968  argrege0  26969  argimgt0  26970  argimlt0  26971  logimul  26972  logneg2  26973  logcnlem3  27002  dvloglem  27006  logf1o2  27008  efopnlem2  27015  cxpsqrtlem  27060  abscxpbnd  27111  logreclem  27120  ang180lem2  27168  asinneg  27244  asinsin  27250  asin1  27252  asinrecl  27260  atanlogaddlem  27271  atanlogsublem  27273  atanlogsub  27274  atantan  27281  atanbndlem  27283  birthday  27312  ppiub  27561  lgsdir2lem1  27682  ex-fl  31078  ex-ceil  31079  normlem2  31743  logdivsqrle  35349  bj-pinftyccb  38334  bj-minftyccb  38338  bj-pinftynminfty  38340  cos2h  38726  tan2h  38727  renegclALT  40212  fourierdlem5  47327  fourierdlem9  47331  fourierdlem18  47340  fourierdlem24  47346  fourierdlem38  47360  fourierdlem40  47362  fourierdlem43  47365  fourierdlem44  47366  fourierdlem46  47367  fourierdlem50  47371  fourierdlem62  47383  fourierdlem66  47387  fourierdlem74  47395  fourierdlem75  47396  fourierdlem76  47397  fourierdlem77  47398  fourierdlem78  47399  fourierdlem83  47404  fourierdlem85  47406  fourierdlem87  47408  fourierdlem88  47409  fourierdlem93  47414  fourierdlem94  47415  fourierdlem95  47416  fourierdlem101  47422  fourierdlem102  47423  fourierdlem103  47424  fourierdlem104  47425  fourierdlem111  47432  fourierdlem112  47433  fourierdlem113  47434  fourierdlem114  47435  sqwvfoura  47443  sqwvfourb  47444  fouriersw  47446  fouriercn  47447  goldratval  48141