Theorem renegcld 11646

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 11112  -cneg 11450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7728  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8706  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11255  df-mnf 11256  df-ltxr 11258  df-sub 11451  df-neg 11452

This theorem is referenced by:  ltord2  11748  leord2  11749  eqord2  11750  possumd  11844  recgt0  12065  riotaneg  12198  negiso  12199  nn0negleid  12529  difgtsumgt  12530  nnnegz  12566  prodge0rd  13086  modsub12d  13898  monoord2  14004  discr1  14207  discr  14208  recj  15076  reneg  15077  imcj  15084  imneg  15085  abslt  15266  absle  15267  o1lo1  15486  o1lo12  15487  icco1  15489  rlimrege0  15528  lo1sub  15580  iseraltlem2  15634  infcvgaux1i  15808  absefib  16146  efieq1re  16147  moddvds  16213  bitscmp  16384  bitsinv1lem  16387  mulgnegnn  19001  cnsubrg  21206  xrhmeo  24692  pjthlem1  25186  ivth2  25205  ovolshft  25261  shftmbl  25288  volsup2  25355  volivth  25357  mbfmulc2lem  25397  mbfposr  25402  mbfposb  25403  ismbf3d  25404  mbfmulc2  25413  mbfinf  25415  mbfi1fseqlem4  25469  mbfi1fseqlem5  25470  mbfi1fseqlem6  25471  mbfi1flimlem  25473  itg2monolem1  25501  iblposlem  25542  iblre  25544  itgreval  25547  itgneg  25554  i1fibl  25558  itgitg1  25559  itgle  25560  ibladd  25571  itgaddlem2  25574  iblabslem  25578  itgmulc2lem2  25583  itgmulc2  25584  bddiblnc  25592  dvferm2lem  25739  dvferm2  25740  rolle  25743  dvivth  25763  lhop2  25768  dvfsumge  25775  dvfsumlem2  25780  dvfsum2  25787  coseq0negpitopi  26250  tanabsge  26253  tanord  26284  tanregt0  26285  abslogimle  26319  logcj  26351  argimgt0  26357  logdiv2  26362  logcnlem3  26389  logccv  26408  abscxpbnd  26498  logreclem  26504  asinlem3a  26612  asinneg  26628  atanlogsublem  26657  atantan  26665  atans2  26673  birthdaylem3  26695  cxplim  26713  amgmlem  26731  emcllem7  26743  zetacvg  26756  eldmgm  26763  lgamgulmlem2  26771  lgsneg  27061  lgsdilem  27064  lgseisenlem1  27115  pntpbnd1  27326  pntibndlem2  27331  padicabvcxp  27372  ostth3  27378  axsegconlem9  28451  nvabs  30193  pjhthlem1  30912  xlt2addrd  32239  ccfldextdgrr  33036  xrge0iifcnv  33212  xrge0iifiso  33214  xrge0iifhom  33216  dya2ub  33568  sgnmul  33840  signsply0  33861  fdvneggt  33911  fdvnegge  33913  climlec3  35008  gg-dvfsumlem2  35470  poimirlem29  36821  itg2gt0cn  36847  ibladdnc  36849  itgaddnclem2  36851  iblabsnclem  36855  itgmulc2nclem2  36859  itgmulc2nc  36860  ftc1anclem5  36869  dvasin  36876  areacirclem1  36880  areacirclem4  36883  areacirclem5  36884  areacirc  36885  oexpreposd  41515  3cubeslem4  41730  pellexlem6  41875  pell1234qrdich  41902  acongeq  42025  sqrtcval  42695  radcnvrat  43376  binomcxplemdvbinom  43415  binomcxplemnotnn0  43418  infnsuprnmpt  44253  neglt  44293  fperiodmul  44313  supsubc  44362  ltmulneg  44401  rexabslelem  44427  supminfrnmpt  44454  leneg2d  44457  leneg3d  44466  supminfxr  44473  climliminflimsupd  44816  liminfreuzlem  44817  liminfltlem  44819  stoweidlem1  45016  stoweidlem7  45022  stoweidlem13  45028  stoweidlem23  45038  stoweidlem34  45049  stoweidlem42  45057  stoweidlem47  45062  stirlinglem6  45094  stirlinglem10  45098  fourierdlem24  45146  fourierdlem39  45161  fourierdlem40  45162  fourierdlem43  45165  fourierdlem44  45166  fourierdlem46  45167  fourierdlem48  45169  fourierdlem49  45170  fourierdlem58  45179  fourierdlem62  45183  fourierdlem72  45193  fourierdlem78  45199  fourierdlem83  45204  fourierdlem85  45206  fourierdlem88  45209  fourierdlem92  45213  fourierdlem97  45218  fourierdlem103  45224  fourierdlem104  45225  fourierdlem109  45230  fourierdlem111  45232  fourierdlem112  45233  sqwvfoura  45243  etransclem23  45272  etransclem46  45295  hoicvr  45563  hoicvrrex  45571  smfinflem  45832  smfliminflem  45845  finfdm  45861  smfinfdmmbllem  45863  sigaradd  45881  sqrtnegnre  46314  proththd  46581  requad01  46588  requad1  46589  requad2  46590  dignn0flhalflem1  47389  eenglngeehlnmlem1  47511  eenglngeehlnmlem2  47512  line2ylem  47525  itscnhlc0yqe  47533  itsclquadb  47550  itscnhlinecirc02p  47559  amgmwlem  47937