Theorem renegcld 11572

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11032  -cneg 11373

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 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109

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 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5521  df-po 5534  df-so 5535  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7319  df-ov 7365  df-oprab 7366  df-mpo 7367  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-pnf 11176  df-mnf 11177  df-ltxr 11179  df-sub 11374  df-neg 11375

This theorem is referenced by:  ltord2  11674  leord2  11675  eqord2  11676  possumd  11770  recgt0  11996  riotaneg  12130  negiso  12131  nn0negleid  12484  difgtsumgt  12485  nnnegz  12522  neglt  12957  prodge0rd  13046  modsub12d  13885  monoord2  13990  discr1  14196  discr  14197  recj  15081  reneg  15082  imcj  15089  imneg  15090  abslt  15272  absle  15273  o1lo1  15494  o1lo12  15495  icco1  15497  rlimrege0  15536  lo1sub  15588  iseraltlem2  15640  infcvgaux1i  15817  absefib  16160  efieq1re  16161  moddvds  16227  bitscmp  16402  bitsinv1lem  16405  mulgnegnn  19055  cnsubrg  21421  xrhmeo  24927  pjthlem1  25418  ivth2  25436  ovolshft  25492  shftmbl  25519  volsup2  25586  volivth  25588  mbfmulc2lem  25628  mbfposr  25633  mbfposb  25634  ismbf3d  25635  mbfmulc2  25644  mbfinf  25646  mbfi1fseqlem4  25699  mbfi1fseqlem5  25700  mbfi1fseqlem6  25701  mbfi1flimlem  25703  itg2monolem1  25731  iblposlem  25773  iblre  25775  itgreval  25778  itgneg  25785  i1fibl  25789  itgitg1  25790  itgle  25791  ibladd  25802  itgaddlem2  25805  iblabslem  25809  itgmulc2lem2  25814  itgmulc2  25815  bddiblnc  25823  dvferm2lem  25967  dvferm2  25968  rolle  25971  dvivth  25991  lhop2  25996  dvfsumge  26003  dvfsumlem2  26008  dvfsum2  26015  coseq0negpitopi  26484  tanabsge  26487  tanord  26519  tanregt0  26520  abslogimle  26554  logcj  26587  argimgt0  26593  logdiv2  26598  logcnlem3  26625  logccv  26644  abscxpbnd  26734  logreclem  26743  asinlem3a  26851  asinneg  26867  atanlogsublem  26896  atantan  26904  atans2  26912  birthdaylem3  26934  cxplim  26953  amgmlem  26971  emcllem7  26983  zetacvg  26996  eldmgm  27003  lgamgulmlem2  27011  lgsneg  27302  lgsdilem  27305  lgseisenlem1  27356  pntpbnd1  27567  pntibndlem2  27572  padicabvcxp  27613  ostth3  27619  axsegconlem9  29012  nvabs  30762  pjhthlem1  31481  xlt2addrd  32851  expgt0b  32909  sgnmul  32927  oexpled  32939  ccfldextdgrr  33836  constrnegcl  33927  iconstr  33930  constrremulcl  33931  constrmulcl  33935  constrresqrtcl  33941  cos9thpiminplylem1  33946  xrge0iifcnv  34097  xrge0iifiso  34099  xrge0iifhom  34101  dya2ub  34434  signsply0  34715  fdvneggt  34764  fdvnegge  34766  climlec3  35936  poimirlem29  37990  itg2gt0cn  38016  ibladdnc  38018  itgaddnclem2  38020  iblabsnclem  38024  itgmulc2nclem2  38028  itgmulc2nc  38029  ftc1anclem5  38038  dvasin  38045  areacirclem1  38049  areacirclem4  38052  areacirclem5  38053  areacirc  38054  posbezout  42559  bcle2d  42638  aks6d1c7lem1  42639  oexpreposd  42774  3cubeslem4  43141  pellexlem6  43286  pell1234qrdich  43313  acongeq  43435  sqrtcval  44092  radcnvrat  44765  binomcxplemdvbinom  44804  binomcxplemnotnn0  44807  infnsuprnmpt  45703  fperiodmul  45761  supsubc  45807  ltmulneg  45845  rexabslelem  45870  supminfrnmpt  45897  leneg2d  45900  leneg3d  45909  supminfxr  45916  climliminflimsupd  46253  liminfreuzlem  46254  liminfltlem  46256  stoweidlem1  46453  stoweidlem7  46459  stoweidlem13  46465  stoweidlem23  46475  stoweidlem34  46486  stoweidlem42  46494  stoweidlem47  46499  stirlinglem6  46531  stirlinglem10  46535  fourierdlem24  46583  fourierdlem39  46598  fourierdlem40  46599  fourierdlem43  46602  fourierdlem44  46603  fourierdlem46  46604  fourierdlem48  46606  fourierdlem49  46607  fourierdlem58  46616  fourierdlem62  46620  fourierdlem72  46630  fourierdlem78  46636  fourierdlem83  46641  fourierdlem85  46643  fourierdlem88  46646  fourierdlem92  46650  fourierdlem97  46655  fourierdlem103  46661  fourierdlem104  46662  fourierdlem109  46667  fourierdlem111  46669  fourierdlem112  46670  sqwvfoura  46680  etransclem23  46709  etransclem46  46732  hoicvr  47000  hoicvrrex  47008  smfinflem  47269  smfliminflem  47282  finfdm  47298  smfinfdmmbllem  47300  sigaradd  47318  squeezedltsq  47340  sqrtnegnre  47773  proththd  48095  requad01  48115  requad1  48116  requad2  48117  dignn0flhalflem1  49109  eenglngeehlnmlem1  49231  eenglngeehlnmlem2  49232  line2ylem  49245  itscnhlc0yqe  49253  itsclquadb  49270  itscnhlinecirc02p  49279  amgmwlem  50295