Theorem renegcld 11673

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

Syntax hints:   → wi 4   ∈ wcel 2098  ℝcr 11139  -cneg 11477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-ltxr 11285  df-sub 11478  df-neg 11479

This theorem is referenced by:  ltord2  11775  leord2  11776  eqord2  11777  possumd  11871  recgt0  12093  riotaneg  12226  negiso  12227  nn0negleid  12557  difgtsumgt  12558  nnnegz  12594  prodge0rd  13116  modsub12d  13929  monoord2  14034  discr1  14237  discr  14238  recj  15107  reneg  15108  imcj  15115  imneg  15116  abslt  15297  absle  15298  o1lo1  15517  o1lo12  15518  icco1  15520  rlimrege0  15559  lo1sub  15611  iseraltlem2  15665  infcvgaux1i  15839  absefib  16178  efieq1re  16179  moddvds  16245  bitscmp  16416  bitsinv1lem  16419  mulgnegnn  19047  cnsubrg  21377  xrhmeo  24915  pjthlem1  25409  ivth2  25428  ovolshft  25484  shftmbl  25511  volsup2  25578  volivth  25580  mbfmulc2lem  25620  mbfposr  25625  mbfposb  25626  ismbf3d  25627  mbfmulc2  25636  mbfinf  25638  mbfi1fseqlem4  25692  mbfi1fseqlem5  25693  mbfi1fseqlem6  25694  mbfi1flimlem  25696  itg2monolem1  25724  iblposlem  25765  iblre  25767  itgreval  25770  itgneg  25777  i1fibl  25781  itgitg1  25782  itgle  25783  ibladd  25794  itgaddlem2  25797  iblabslem  25801  itgmulc2lem2  25806  itgmulc2  25807  bddiblnc  25815  dvferm2lem  25962  dvferm2  25963  rolle  25966  dvivth  25987  lhop2  25992  dvfsumge  26000  dvfsumlem2  26005  dvfsumlem2OLD  26006  dvfsum2  26013  coseq0negpitopi  26483  tanabsge  26486  tanord  26517  tanregt0  26518  abslogimle  26552  logcj  26585  argimgt0  26591  logdiv2  26596  logcnlem3  26623  logccv  26642  abscxpbnd  26733  logreclem  26739  asinlem3a  26847  asinneg  26863  atanlogsublem  26892  atantan  26900  atans2  26908  birthdaylem3  26930  cxplim  26949  amgmlem  26967  emcllem7  26979  zetacvg  26992  eldmgm  26999  lgamgulmlem2  27007  lgsneg  27299  lgsdilem  27302  lgseisenlem1  27353  pntpbnd1  27564  pntibndlem2  27569  padicabvcxp  27610  ostth3  27616  axsegconlem9  28808  nvabs  30554  pjhthlem1  31273  xlt2addrd  32610  ccfldextdgrr  33488  xrge0iifcnv  33662  xrge0iifiso  33664  xrge0iifhom  33666  dya2ub  34018  sgnmul  34290  signsply0  34311  fdvneggt  34360  fdvnegge  34362  climlec3  35456  poimirlem29  37250  itg2gt0cn  37276  ibladdnc  37278  itgaddnclem2  37280  iblabsnclem  37284  itgmulc2nclem2  37288  itgmulc2nc  37289  ftc1anclem5  37298  dvasin  37305  areacirclem1  37309  areacirclem4  37312  areacirclem5  37313  areacirc  37314  posbezout  41700  bcle2d  41779  aks6d1c7lem1  41780  oexpreposd  42013  3cubeslem4  42248  pellexlem6  42393  pell1234qrdich  42420  acongeq  42543  sqrtcval  43210  radcnvrat  43890  binomcxplemdvbinom  43929  binomcxplemnotnn0  43932  infnsuprnmpt  44761  neglt  44801  fperiodmul  44821  supsubc  44870  ltmulneg  44909  rexabslelem  44935  supminfrnmpt  44962  leneg2d  44965  leneg3d  44974  supminfxr  44981  climliminflimsupd  45324  liminfreuzlem  45325  liminfltlem  45327  stoweidlem1  45524  stoweidlem7  45530  stoweidlem13  45536  stoweidlem23  45546  stoweidlem34  45557  stoweidlem42  45565  stoweidlem47  45570  stirlinglem6  45602  stirlinglem10  45606  fourierdlem24  45654  fourierdlem39  45669  fourierdlem40  45670  fourierdlem43  45673  fourierdlem44  45674  fourierdlem46  45675  fourierdlem48  45677  fourierdlem49  45678  fourierdlem58  45687  fourierdlem62  45691  fourierdlem72  45701  fourierdlem78  45707  fourierdlem83  45712  fourierdlem85  45714  fourierdlem88  45717  fourierdlem92  45721  fourierdlem97  45726  fourierdlem103  45732  fourierdlem104  45733  fourierdlem109  45738  fourierdlem111  45740  fourierdlem112  45741  sqwvfoura  45751  etransclem23  45780  etransclem46  45803  hoicvr  46071  hoicvrrex  46079  smfinflem  46340  smfliminflem  46353  finfdm  46369  smfinfdmmbllem  46371  sigaradd  46389  sqrtnegnre  46822  proththd  47088  requad01  47095  requad1  47096  requad2  47097  dignn0flhalflem1  47871  eenglngeehlnmlem1  47993  eenglngeehlnmlem2  47994  line2ylem  48007  itscnhlc0yqe  48015  itsclquadb  48032  itscnhlinecirc02p  48041  amgmwlem  48418