Theorem renegcld 11547

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 11427	. 2 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
3	1, 2	syl 17	1 ⊢ (𝜑 → -𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11008  -cneg 11348

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 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085

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 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-ltxr 11154  df-sub 11349  df-neg 11350

This theorem is referenced by:  ltord2  11649  leord2  11650  eqord2  11651  possumd  11745  recgt0  11970  riotaneg  12104  negiso  12105  nn0negleid  12436  difgtsumgt  12437  nnnegz  12474  neglt  12913  prodge0rd  13002  modsub12d  13835  monoord2  13940  discr1  14146  discr  14147  recj  15031  reneg  15032  imcj  15039  imneg  15040  abslt  15222  absle  15223  o1lo1  15444  o1lo12  15445  icco1  15447  rlimrege0  15486  lo1sub  15538  iseraltlem2  15590  infcvgaux1i  15764  absefib  16107  efieq1re  16108  moddvds  16174  bitscmp  16349  bitsinv1lem  16352  mulgnegnn  18963  cnsubrg  21334  xrhmeo  24842  pjthlem1  25335  ivth2  25354  ovolshft  25410  shftmbl  25437  volsup2  25504  volivth  25506  mbfmulc2lem  25546  mbfposr  25551  mbfposb  25552  ismbf3d  25553  mbfmulc2  25562  mbfinf  25564  mbfi1fseqlem4  25617  mbfi1fseqlem5  25618  mbfi1fseqlem6  25619  mbfi1flimlem  25621  itg2monolem1  25649  iblposlem  25691  iblre  25693  itgreval  25696  itgneg  25703  i1fibl  25707  itgitg1  25708  itgle  25709  ibladd  25720  itgaddlem2  25723  iblabslem  25727  itgmulc2lem2  25732  itgmulc2  25733  bddiblnc  25741  dvferm2lem  25888  dvferm2  25889  rolle  25892  dvivth  25913  lhop2  25918  dvfsumge  25926  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsum2  25939  coseq0negpitopi  26410  tanabsge  26413  tanord  26445  tanregt0  26446  abslogimle  26480  logcj  26513  argimgt0  26519  logdiv2  26524  logcnlem3  26551  logccv  26570  abscxpbnd  26661  logreclem  26670  asinlem3a  26778  asinneg  26794  atanlogsublem  26823  atantan  26831  atans2  26839  birthdaylem3  26861  cxplim  26880  amgmlem  26898  emcllem7  26910  zetacvg  26923  eldmgm  26930  lgamgulmlem2  26938  lgsneg  27230  lgsdilem  27233  lgseisenlem1  27284  pntpbnd1  27495  pntibndlem2  27500  padicabvcxp  27541  ostth3  27547  axsegconlem9  28874  nvabs  30620  pjhthlem1  31339  xlt2addrd  32711  expgt0b  32770  sgnmul  32789  oexpled  32801  ccfldextdgrr  33655  constrnegcl  33746  iconstr  33749  constrremulcl  33750  constrmulcl  33754  constrresqrtcl  33760  cos9thpiminplylem1  33765  xrge0iifcnv  33916  xrge0iifiso  33918  xrge0iifhom  33920  dya2ub  34254  signsply0  34535  fdvneggt  34584  fdvnegge  34586  climlec3  35727  poimirlem29  37649  itg2gt0cn  37675  ibladdnc  37677  itgaddnclem2  37679  iblabsnclem  37683  itgmulc2nclem2  37687  itgmulc2nc  37688  ftc1anclem5  37697  dvasin  37704  areacirclem1  37708  areacirclem4  37711  areacirclem5  37712  areacirc  37713  posbezout  42093  bcle2d  42172  aks6d1c7lem1  42173  oexpreposd  42315  3cubeslem4  42682  pellexlem6  42827  pell1234qrdich  42854  acongeq  42976  sqrtcval  43634  radcnvrat  44307  binomcxplemdvbinom  44346  binomcxplemnotnn0  44349  infnsuprnmpt  45248  fperiodmul  45306  supsubc  45353  ltmulneg  45391  rexabslelem  45417  supminfrnmpt  45444  leneg2d  45447  leneg3d  45456  supminfxr  45463  climliminflimsupd  45802  liminfreuzlem  45803  liminfltlem  45805  stoweidlem1  46002  stoweidlem7  46008  stoweidlem13  46014  stoweidlem23  46024  stoweidlem34  46035  stoweidlem42  46043  stoweidlem47  46048  stirlinglem6  46080  stirlinglem10  46084  fourierdlem24  46132  fourierdlem39  46147  fourierdlem40  46148  fourierdlem43  46151  fourierdlem44  46152  fourierdlem46  46153  fourierdlem48  46155  fourierdlem49  46156  fourierdlem58  46165  fourierdlem62  46169  fourierdlem72  46179  fourierdlem78  46185  fourierdlem83  46190  fourierdlem85  46192  fourierdlem88  46195  fourierdlem92  46199  fourierdlem97  46204  fourierdlem103  46210  fourierdlem104  46211  fourierdlem109  46216  fourierdlem111  46218  fourierdlem112  46219  sqwvfoura  46229  etransclem23  46258  etransclem46  46281  hoicvr  46549  hoicvrrex  46557  smfinflem  46818  smfliminflem  46831  finfdm  46847  smfinfdmmbllem  46849  sigaradd  46867  squeezedltsq  46890  sqrtnegnre  47311  proththd  47618  requad01  47625  requad1  47626  requad2  47627  dignn0flhalflem1  48620  eenglngeehlnmlem1  48742  eenglngeehlnmlem2  48743  line2ylem  48756  itscnhlc0yqe  48764  itsclquadb  48781  itscnhlinecirc02p  48790  amgmwlem  49807