Theorem renegcld 11605

Description: Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
renegcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
renegcld	⊢ (𝜑 → -𝐴 ∈ ℝ)

Proof of Theorem renegcld

Step	Hyp	Ref	Expression
1		renegcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		renegcl 11485	. 2 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
3	1, 2	syl 17	1 ⊢ (𝜑 → -𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11067  -cneg 11406

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213  df-sub 11407  df-neg 11408

This theorem is referenced by:  ltord2  11707  leord2  11708  eqord2  11709  possumd  11803  recgt0  12028  riotaneg  12162  negiso  12163  nn0negleid  12494  difgtsumgt  12495  nnnegz  12532  neglt  12971  prodge0rd  13060  modsub12d  13893  monoord2  13998  discr1  14204  discr  14205  recj  15090  reneg  15091  imcj  15098  imneg  15099  abslt  15281  absle  15282  o1lo1  15503  o1lo12  15504  icco1  15506  rlimrege0  15545  lo1sub  15597  iseraltlem2  15649  infcvgaux1i  15823  absefib  16166  efieq1re  16167  moddvds  16233  bitscmp  16408  bitsinv1lem  16411  mulgnegnn  19016  cnsubrg  21344  xrhmeo  24844  pjthlem1  25337  ivth2  25356  ovolshft  25412  shftmbl  25439  volsup2  25506  volivth  25508  mbfmulc2lem  25548  mbfposr  25553  mbfposb  25554  ismbf3d  25555  mbfmulc2  25564  mbfinf  25566  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  mbfi1flimlem  25623  itg2monolem1  25651  iblposlem  25693  iblre  25695  itgreval  25698  itgneg  25705  i1fibl  25709  itgitg1  25710  itgle  25711  ibladd  25722  itgaddlem2  25725  iblabslem  25729  itgmulc2lem2  25734  itgmulc2  25735  bddiblnc  25743  dvferm2lem  25890  dvferm2  25891  rolle  25894  dvivth  25915  lhop2  25920  dvfsumge  25928  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsum2  25941  coseq0negpitopi  26412  tanabsge  26415  tanord  26447  tanregt0  26448  abslogimle  26482  logcj  26515  argimgt0  26521  logdiv2  26526  logcnlem3  26553  logccv  26572  abscxpbnd  26663  logreclem  26672  asinlem3a  26780  asinneg  26796  atanlogsublem  26825  atantan  26833  atans2  26841  birthdaylem3  26863  cxplim  26882  amgmlem  26900  emcllem7  26912  zetacvg  26925  eldmgm  26932  lgamgulmlem2  26940  lgsneg  27232  lgsdilem  27235  lgseisenlem1  27286  pntpbnd1  27497  pntibndlem2  27502  padicabvcxp  27543  ostth3  27549  axsegconlem9  28852  nvabs  30601  pjhthlem1  31320  xlt2addrd  32682  expgt0b  32741  sgnmul  32760  oexpled  32772  ccfldextdgrr  33667  constrnegcl  33753  iconstr  33756  constrremulcl  33757  constrmulcl  33761  constrresqrtcl  33767  cos9thpiminplylem1  33772  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  dya2ub  34261  signsply0  34542  fdvneggt  34591  fdvnegge  34593  climlec3  35721  poimirlem29  37643  itg2gt0cn  37669  ibladdnc  37671  itgaddnclem2  37673  iblabsnclem  37677  itgmulc2nclem2  37681  itgmulc2nc  37682  ftc1anclem5  37691  dvasin  37698  areacirclem1  37702  areacirclem4  37705  areacirclem5  37706  areacirc  37707  posbezout  42088  bcle2d  42167  aks6d1c7lem1  42168  oexpreposd  42310  3cubeslem4  42677  pellexlem6  42822  pell1234qrdich  42849  acongeq  42972  sqrtcval  43630  radcnvrat  44303  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  infnsuprnmpt  45244  fperiodmul  45302  supsubc  45349  ltmulneg  45388  rexabslelem  45414  supminfrnmpt  45441  leneg2d  45444  leneg3d  45453  supminfxr  45460  climliminflimsupd  45799  liminfreuzlem  45800  liminfltlem  45802  stoweidlem1  45999  stoweidlem7  46005  stoweidlem13  46011  stoweidlem23  46021  stoweidlem34  46032  stoweidlem42  46040  stoweidlem47  46045  stirlinglem6  46077  stirlinglem10  46081  fourierdlem24  46129  fourierdlem39  46144  fourierdlem40  46145  fourierdlem43  46148  fourierdlem44  46149  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem58  46162  fourierdlem62  46166  fourierdlem72  46176  fourierdlem78  46182  fourierdlem83  46187  fourierdlem85  46189  fourierdlem88  46192  fourierdlem92  46196  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  fourierdlem109  46213  fourierdlem111  46215  fourierdlem112  46216  sqwvfoura  46226  etransclem23  46255  etransclem46  46278  hoicvr  46546  hoicvrrex  46554  smfinflem  46815  smfliminflem  46828  finfdm  46844  smfinfdmmbllem  46846  sigaradd  46864  squeezedltsq  46887  sqrtnegnre  47308  proththd  47615  requad01  47622  requad1  47623  requad2  47624  dignn0flhalflem1  48604  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  line2ylem  48740  itscnhlc0yqe  48748  itsclquadb  48765  itscnhlinecirc02p  48774  amgmwlem  49791