Theorem renegcld 11581

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11043  -cneg 11382

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 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120

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 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-ltxr 11189  df-sub 11383  df-neg 11384

This theorem is referenced by:  ltord2  11683  leord2  11684  eqord2  11685  possumd  11779  recgt0  12004  riotaneg  12138  negiso  12139  nn0negleid  12470  difgtsumgt  12471  nnnegz  12508  neglt  12947  prodge0rd  13036  modsub12d  13869  monoord2  13974  discr1  14180  discr  14181  recj  15066  reneg  15067  imcj  15074  imneg  15075  abslt  15257  absle  15258  o1lo1  15479  o1lo12  15480  icco1  15482  rlimrege0  15521  lo1sub  15573  iseraltlem2  15625  infcvgaux1i  15799  absefib  16142  efieq1re  16143  moddvds  16209  bitscmp  16384  bitsinv1lem  16387  mulgnegnn  18998  cnsubrg  21369  xrhmeo  24877  pjthlem1  25370  ivth2  25389  ovolshft  25445  shftmbl  25472  volsup2  25539  volivth  25541  mbfmulc2lem  25581  mbfposr  25586  mbfposb  25587  ismbf3d  25588  mbfmulc2  25597  mbfinf  25599  mbfi1fseqlem4  25652  mbfi1fseqlem5  25653  mbfi1fseqlem6  25654  mbfi1flimlem  25656  itg2monolem1  25684  iblposlem  25726  iblre  25728  itgreval  25731  itgneg  25738  i1fibl  25742  itgitg1  25743  itgle  25744  ibladd  25755  itgaddlem2  25758  iblabslem  25762  itgmulc2lem2  25767  itgmulc2  25768  bddiblnc  25776  dvferm2lem  25923  dvferm2  25924  rolle  25927  dvivth  25948  lhop2  25953  dvfsumge  25961  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsum2  25974  coseq0negpitopi  26445  tanabsge  26448  tanord  26480  tanregt0  26481  abslogimle  26515  logcj  26548  argimgt0  26554  logdiv2  26559  logcnlem3  26586  logccv  26605  abscxpbnd  26696  logreclem  26705  asinlem3a  26813  asinneg  26829  atanlogsublem  26858  atantan  26866  atans2  26874  birthdaylem3  26896  cxplim  26915  amgmlem  26933  emcllem7  26945  zetacvg  26958  eldmgm  26965  lgamgulmlem2  26973  lgsneg  27265  lgsdilem  27268  lgseisenlem1  27319  pntpbnd1  27530  pntibndlem2  27535  padicabvcxp  27576  ostth3  27582  axsegconlem9  28905  nvabs  30651  pjhthlem1  31370  xlt2addrd  32732  expgt0b  32791  sgnmul  32810  oexpled  32822  ccfldextdgrr  33660  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  35714  poimirlem29  37636  itg2gt0cn  37662  ibladdnc  37664  itgaddnclem2  37666  iblabsnclem  37670  itgmulc2nclem2  37674  itgmulc2nc  37675  ftc1anclem5  37684  dvasin  37691  areacirclem1  37695  areacirclem4  37698  areacirclem5  37699  areacirc  37700  posbezout  42081  bcle2d  42160  aks6d1c7lem1  42161  oexpreposd  42303  3cubeslem4  42670  pellexlem6  42815  pell1234qrdich  42842  acongeq  42965  sqrtcval  43623  radcnvrat  44296  binomcxplemdvbinom  44335  binomcxplemnotnn0  44338  infnsuprnmpt  45237  fperiodmul  45295  supsubc  45342  ltmulneg  45381  rexabslelem  45407  supminfrnmpt  45434  leneg2d  45437  leneg3d  45446  supminfxr  45453  climliminflimsupd  45792  liminfreuzlem  45793  liminfltlem  45795  stoweidlem1  45992  stoweidlem7  45998  stoweidlem13  46004  stoweidlem23  46014  stoweidlem34  46025  stoweidlem42  46033  stoweidlem47  46038  stirlinglem6  46070  stirlinglem10  46074  fourierdlem24  46122  fourierdlem39  46137  fourierdlem40  46138  fourierdlem43  46141  fourierdlem44  46142  fourierdlem46  46143  fourierdlem48  46145  fourierdlem49  46146  fourierdlem58  46155  fourierdlem62  46159  fourierdlem72  46169  fourierdlem78  46175  fourierdlem83  46180  fourierdlem85  46182  fourierdlem88  46185  fourierdlem92  46189  fourierdlem97  46194  fourierdlem103  46200  fourierdlem104  46201  fourierdlem109  46206  fourierdlem111  46208  fourierdlem112  46209  sqwvfoura  46219  etransclem23  46248  etransclem46  46271  hoicvr  46539  hoicvrrex  46547  smfinflem  46808  smfliminflem  46821  finfdm  46837  smfinfdmmbllem  46839  sigaradd  46857  squeezedltsq  46880  sqrtnegnre  47301  proththd  47608  requad01  47615  requad1  47616  requad2  47617  dignn0flhalflem1  48597  eenglngeehlnmlem1  48719  eenglngeehlnmlem2  48720  line2ylem  48733  itscnhlc0yqe  48741  itsclquadb  48758  itscnhlinecirc02p  48767  amgmwlem  49784