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 2121  ℝcr 11032  -cneg 11373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  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 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  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  21406  xrhmeo  24935  pjthlem1  25426  ivth2  25444  ovolshft  25500  shftmbl  25527  volsup2  25594  volivth  25596  mbfmulc2lem  25636  mbfposr  25641  mbfposb  25642  ismbf3d  25643  mbfmulc2  25652  mbfinf  25654  mbfi1fseqlem4  25707  mbfi1fseqlem5  25708  mbfi1fseqlem6  25709  mbfi1flimlem  25711  itg2monolem1  25739  iblposlem  25781  iblre  25783  itgreval  25786  itgneg  25793  i1fibl  25797  itgitg1  25798  itgle  25799  ibladd  25810  itgaddlem2  25813  iblabslem  25817  itgmulc2lem2  25822  itgmulc2  25823  bddiblnc  25831  dvferm2lem  25975  dvferm2  25976  rolle  25979  dvivth  25999  lhop2  26004  dvfsumge  26011  dvfsumlem2  26016  dvfsum2  26023  coseq0negpitopi  26489  tanabsge  26492  tanord  26524  tanregt0  26525  abslogimle  26559  logcj  26592  argimgt0  26598  logdiv2  26603  logcnlem3  26630  logccv  26649  abscxpbnd  26739  logreclem  26748  asinlem3a  26856  asinneg  26872  atanlogsublem  26901  atantan  26909  atans2  26917  birthdaylem3  26939  cxplim  26957  amgmlem  26975  emcllem7  26987  zetacvg  27000  eldmgm  27007  lgamgulmlem2  27015  lgsneg  27306  lgsdilem  27309  lgseisenlem1  27360  pntpbnd1  27571  pntibndlem2  27576  padicabvcxp  27617  ostth3  27623  axsegconlem9  29016  nvabs  30765  pjhthlem1  31484  xlt2addrd  32855  expgt0b  32913  sgnmul  32931  oexpled  32943  ccfldextdgrr  33868  constrnegcl  33959  iconstr  33962  constrremulcl  33963  constrmulcl  33967  constrresqrtcl  33973  cos9thpiminplylem1  33978  xrge0iifcnv  34129  xrge0iifiso  34131  xrge0iifhom  34133  dya2ub  34466  signsply0  34747  fdvneggt  34796  fdvnegge  34798  climlec3  35977  poimirlem29  38031  itg2gt0cn  38057  ibladdnc  38059  itgaddnclem2  38061  iblabsnclem  38065  itgmulc2nclem2  38069  itgmulc2nc  38070  ftc1anclem5  38079  dvasin  38086  areacirclem1  38090  areacirclem4  38093  areacirclem5  38094  areacirc  38095  posbezout  42600  bcle2d  42679  aks6d1c7lem1  42680  oexpreposd  42814  3cubeslem4  43153  pellexlem6  43294  pell1234qrdich  43321  acongeq  43443  sqrtcval  44100  radcnvrat  44773  binomcxplemdvbinom  44812  binomcxplemnotnn0  44815  infnsuprnmpt  45708  fperiodmul  45766  supsubc  45812  ltmulneg  45850  rexabslelem  45875  supminfrnmpt  45902  leneg2d  45905  leneg3d  45914  supminfxr  45921  climliminflimsupd  46258  liminfreuzlem  46259  liminfltlem  46261  stoweidlem1  46458  stoweidlem7  46464  stoweidlem13  46470  stoweidlem23  46480  stoweidlem34  46491  stoweidlem42  46499  stoweidlem47  46504  stirlinglem6  46536  stirlinglem10  46540  fourierdlem24  46588  fourierdlem39  46603  fourierdlem40  46604  fourierdlem43  46607  fourierdlem44  46608  fourierdlem46  46609  fourierdlem48  46611  fourierdlem49  46612  fourierdlem58  46621  fourierdlem62  46625  fourierdlem72  46635  fourierdlem78  46641  fourierdlem83  46646  fourierdlem85  46648  fourierdlem88  46651  fourierdlem92  46655  fourierdlem97  46660  fourierdlem103  46666  fourierdlem104  46667  fourierdlem109  46672  fourierdlem111  46674  fourierdlem112  46675  sqwvfoura  46685  etransclem23  46714  etransclem46  46737  hoicvr  47005  hoicvrrex  47013  smfinflem  47274  smfliminflem  47287  finfdm  47303  smfinfdmmbllem  47305  sigaradd  47323  squeezedltsq  47347  sqrtnegnre  47784  proththd  48106  requad01  48126  requad1  48127  requad2  48128  dignn0flhalflem1  49120  eenglngeehlnmlem1  49242  eenglngeehlnmlem2  49243  line2ylem  49256  itscnhlc0yqe  49264  itsclquadb  49281  itscnhlinecirc02p  49290  amgmwlem  50306