Theorem renegcld 11578

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11039  -cneg 11379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-po 5542  df-so 5543  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-ltxr 11185  df-sub 11380  df-neg 11381

This theorem is referenced by:  ltord2  11680  leord2  11681  eqord2  11682  possumd  11776  recgt0  12001  riotaneg  12135  negiso  12136  nn0negleid  12467  difgtsumgt  12468  nnnegz  12505  neglt  12939  prodge0rd  13028  modsub12d  13865  monoord2  13970  discr1  14176  discr  14177  recj  15061  reneg  15062  imcj  15069  imneg  15070  abslt  15252  absle  15253  o1lo1  15474  o1lo12  15475  icco1  15477  rlimrege0  15516  lo1sub  15568  iseraltlem2  15620  infcvgaux1i  15794  absefib  16137  efieq1re  16138  moddvds  16204  bitscmp  16379  bitsinv1lem  16382  mulgnegnn  19031  cnsubrg  21399  xrhmeo  24917  pjthlem1  25410  ivth2  25429  ovolshft  25485  shftmbl  25512  volsup2  25579  volivth  25581  mbfmulc2lem  25621  mbfposr  25626  mbfposb  25627  ismbf3d  25628  mbfmulc2  25637  mbfinf  25639  mbfi1fseqlem4  25692  mbfi1fseqlem5  25693  mbfi1fseqlem6  25694  mbfi1flimlem  25696  itg2monolem1  25724  iblposlem  25766  iblre  25768  itgreval  25771  itgneg  25778  i1fibl  25782  itgitg1  25783  itgle  25784  ibladd  25795  itgaddlem2  25798  iblabslem  25802  itgmulc2lem2  25807  itgmulc2  25808  bddiblnc  25816  dvferm2lem  25963  dvferm2  25964  rolle  25967  dvivth  25988  lhop2  25993  dvfsumge  26001  dvfsumlem2  26006  dvfsumlem2OLD  26007  dvfsum2  26014  coseq0negpitopi  26485  tanabsge  26488  tanord  26520  tanregt0  26521  abslogimle  26555  logcj  26588  argimgt0  26594  logdiv2  26599  logcnlem3  26626  logccv  26645  abscxpbnd  26736  logreclem  26745  asinlem3a  26853  asinneg  26869  atanlogsublem  26898  atantan  26906  atans2  26914  birthdaylem3  26936  cxplim  26955  amgmlem  26973  emcllem7  26985  zetacvg  26998  eldmgm  27005  lgamgulmlem2  27013  lgsneg  27305  lgsdilem  27308  lgseisenlem1  27359  pntpbnd1  27570  pntibndlem2  27575  padicabvcxp  27616  ostth3  27622  axsegconlem9  29016  nvabs  30766  pjhthlem1  31485  xlt2addrd  32856  expgt0b  32914  sgnmul  32933  oexpled  32945  ccfldextdgrr  33856  constrnegcl  33947  iconstr  33950  constrremulcl  33951  constrmulcl  33955  constrresqrtcl  33961  cos9thpiminplylem1  33966  xrge0iifcnv  34117  xrge0iifiso  34119  xrge0iifhom  34121  dya2ub  34454  signsply0  34735  fdvneggt  34784  fdvnegge  34786  climlec3  35956  poimirlem29  37929  itg2gt0cn  37955  ibladdnc  37957  itgaddnclem2  37959  iblabsnclem  37963  itgmulc2nclem2  37967  itgmulc2nc  37968  ftc1anclem5  37977  dvasin  37984  areacirclem1  37988  areacirclem4  37991  areacirclem5  37992  areacirc  37993  posbezout  42499  bcle2d  42578  aks6d1c7lem1  42579  oexpreposd  42721  3cubeslem4  43075  pellexlem6  43220  pell1234qrdich  43247  acongeq  43369  sqrtcval  44026  radcnvrat  44699  binomcxplemdvbinom  44738  binomcxplemnotnn0  44741  infnsuprnmpt  45637  fperiodmul  45695  supsubc  45741  ltmulneg  45779  rexabslelem  45805  supminfrnmpt  45832  leneg2d  45835  leneg3d  45844  supminfxr  45851  climliminflimsupd  46188  liminfreuzlem  46189  liminfltlem  46191  stoweidlem1  46388  stoweidlem7  46394  stoweidlem13  46400  stoweidlem23  46410  stoweidlem34  46421  stoweidlem42  46429  stoweidlem47  46434  stirlinglem6  46466  stirlinglem10  46470  fourierdlem24  46518  fourierdlem39  46533  fourierdlem40  46534  fourierdlem43  46537  fourierdlem44  46538  fourierdlem46  46539  fourierdlem48  46541  fourierdlem49  46542  fourierdlem58  46551  fourierdlem62  46555  fourierdlem72  46565  fourierdlem78  46571  fourierdlem83  46576  fourierdlem85  46578  fourierdlem88  46581  fourierdlem92  46585  fourierdlem97  46590  fourierdlem103  46596  fourierdlem104  46597  fourierdlem109  46602  fourierdlem111  46604  fourierdlem112  46605  sqwvfoura  46615  etransclem23  46644  etransclem46  46667  hoicvr  46935  hoicvrrex  46943  smfinflem  47204  smfliminflem  47217  finfdm  47233  smfinfdmmbllem  47235  sigaradd  47253  squeezedltsq  47275  sqrtnegnre  47696  proththd  48003  requad01  48010  requad1  48011  requad2  48012  dignn0flhalflem1  49004  eenglngeehlnmlem1  49126  eenglngeehlnmlem2  49127  line2ylem  49140  itscnhlc0yqe  49148  itsclquadb  49165  itscnhlinecirc02p  49174  amgmwlem  50190