Theorem renegcld 11616

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

Syntax hints:   → wi 4   ∈ wcel 2144  ℝcr 11074  -cneg 11417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-po 5557  df-so 5558  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-ltxr 11223  df-sub 11418  df-neg 11419

This theorem is referenced by:  ltord2  11718  leord2  11719  eqord2  11720  possumd  11814  recgt0  12039  riotaneg  12173  negiso  12174  nn0negleid  12535  difgtsumgt  12536  nnnegz  12573  neglt  13015  prodge0rd  13104  modsub12d  13943  monoord2  14048  discr1  14254  discr  14255  sgnmul  15122  recj  15153  reneg  15154  imcj  15161  imneg  15162  abslt  15344  absle  15345  o1lo1  15566  o1lo12  15567  icco1  15569  rlimrege0  15608  lo1sub  15660  iseraltlem2  15712  infcvgaux1i  15889  absefib  16232  efieq1re  16233  moddvds  16299  bitscmp  16474  bitsinv1lem  16477  mulgnegnn  19128  cnsubrg  21481  xrhmeo  25010  pjthlem1  25501  ivth2  25519  ovolshft  25575  shftmbl  25602  volsup2  25669  volivth  25671  mbfmulc2lem  25711  mbfposr  25716  mbfposb  25717  ismbf3d  25718  mbfmulc2  25727  mbfinf  25729  mbfi1fseqlem4  25782  mbfi1fseqlem5  25783  mbfi1fseqlem6  25784  mbfi1flimlem  25786  itg2monolem1  25814  iblposlem  25856  iblre  25858  itgreval  25861  itgneg  25868  i1fibl  25872  itgitg1  25873  itgle  25874  ibladd  25885  itgaddlem2  25888  iblabslem  25892  itgmulc2lem2  25897  itgmulc2  25898  bddiblnc  25906  dvferm2lem  26050  dvferm2  26051  rolle  26054  dvivth  26074  lhop2  26079  dvfsumge  26086  dvfsumlem2  26091  dvfsum2  26098  coseq0negpitopi  26570  tanabsge  26573  tanord  26605  tanregt0  26606  abslogimle  26640  logcj  26673  argimgt0  26679  logdiv2  26684  logcnlem3  26711  logccv  26730  abscxpbnd  26820  logreclem  26829  asinlem3a  26937  asinneg  26953  atanlogsublem  26982  atantan  26990  atans2  26998  birthdaylem3  27020  cxplim  27038  amgmlem  27056  emcllem7  27068  zetacvg  27081  eldmgm  27088  lgamgulmlem2  27096  lgsneg  27387  lgsdilem  27390  lgseisenlem1  27441  pntpbnd1  27652  pntibndlem2  27657  padicabvcxp  27698  ostth3  27704  axsegconlem9  29128  nvabs  30877  pjhthlem1  31596  xlt2addrd  32963  expgt0b  33021  oexpled  33040  ccfldextdgrr  33971  constrnegcl  34062  iconstr  34065  constrremulcl  34066  constrmulcl  34070  constrresqrtcl  34076  cos9thpiminplylem1  34081  xrge0iifcnv  34232  xrge0iifiso  34234  xrge0iifhom  34236  dya2ub  34569  signsply0  34847  fdvneggt  34896  fdvnegge  34898  climlec3  36089  poimirlem29  38153  itg2gt0cn  38179  ibladdnc  38181  itgaddnclem2  38183  iblabsnclem  38187  itgmulc2nclem2  38191  itgmulc2nc  38192  ftc1anclem5  38201  dvasin  38208  areacirclem1  38212  areacirclem4  38215  areacirclem5  38216  areacirc  38217  posbezout  42722  bcle2d  42801  aks6d1c7lem1  42802  oexpreposd  42936  3cubeslem4  43275  pellexlem6  43416  pell1234qrdich  43443  acongeq  43565  sqrtcval  44222  radcnvrat  44895  binomcxplemdvbinom  44934  binomcxplemnotnn0  44937  infnsuprnmpt  45830  fperiodmul  45888  supsubc  45934  ltmulneg  45972  rexabslelem  45997  supminfrnmpt  46024  leneg2d  46027  leneg3d  46036  supminfxr  46043  climliminflimsupd  46380  liminfreuzlem  46381  liminfltlem  46383  stoweidlem1  46580  stoweidlem7  46586  stoweidlem13  46592  stoweidlem23  46602  stoweidlem34  46613  stoweidlem42  46621  stoweidlem47  46626  stirlinglem6  46658  stirlinglem10  46662  fourierdlem24  46710  fourierdlem39  46725  fourierdlem40  46726  fourierdlem43  46729  fourierdlem44  46730  fourierdlem46  46731  fourierdlem48  46733  fourierdlem49  46734  fourierdlem58  46743  fourierdlem62  46747  fourierdlem72  46757  fourierdlem78  46763  fourierdlem83  46768  fourierdlem85  46770  fourierdlem88  46773  fourierdlem92  46777  fourierdlem97  46782  fourierdlem103  46788  fourierdlem104  46789  fourierdlem109  46794  fourierdlem111  46796  fourierdlem112  46797  sqwvfoura  46807  etransclem23  46836  etransclem46  46859  hoicvr  47127  hoicvrrex  47135  smfinflem  47396  smfliminflem  47409  finfdm  47425  smfinfdmmbllem  47427  sigaradd  47445  squeezedltsq  47469  sqrtnegnre  47906  proththd  48228  requad01  48248  requad1  48249  requad2  48250  dignn0flhalflem1  49242  eenglngeehlnmlem1  49364  eenglngeehlnmlem2  49365  line2ylem  49378  itscnhlc0yqe  49386  itsclquadb  49403  itscnhlinecirc02p  49412  amgmwlem  50428