Theorem resubcld 10012

Description: Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
renegcld.1
resubcld.2

Assertion

Ref	Expression
resubcld

Proof of Theorem resubcld

Step	Hyp	Ref	Expression
1		renegcld.1	. 2
2		resubcld.2	. 2
3		resubcl 9906	. 2
4	1, 2, 3	syl2anc 661	1

Syntax hints:  ->wi 4  e.wcel 1818  (class class class)co 6296  cr 9512  cmin 9828

This theorem is referenced by:  ltsubadd  10047  lesubadd  10049  lesub1  10071  lesub2  10072  ltsub1  10073  ltsub2  10074  lt2sub  10075  le2sub  10076  ltmul1a  10416  cru  10553  qbtwnre  11427  lincmb01cmp  11692  iccf1o  11693  xov1plusxeqvd  11695  intfracq  11986  fldiv  11987  modlt  12006  modsubdir  12055  serle  12162  expmulnbnd  12298  discr  12303  fzsdom2  12486  cshwidxmod  12774  crre  12947  remullem  12961  sqrlem7  13082  absrdbnd  13174  fzomaxdiflem  13175  caubnd2  13190  amgm2  13202  mulcn2  13418  reccn2  13419  rlimo1  13439  climle  13462  climsqz  13463  climsqz2  13464  rlimle  13470  isercolllem1  13487  climsup  13492  caucvgrlem  13495  caucvgrlem2  13497  iseraltlem2  13505  iseraltlem3  13506  iseralt  13507  fsumle  13613  cvgcmp  13630  cvgcmpce  13632  eflt  13852  resinhcl  13891  tanhlt1  13895  sin01bnd  13920  sin01gt0  13925  moddvds  13993  bitscmp  14088  bitsinv1lem  14091  smueqlem  14140  modprm0  14330  pcbc  14419  4sqlem15  14477  blss2ps  20906  blss2  20907  blssps  20927  blss  20928  nm2dif  21144  nlmvscnlem2  21194  nrginvrcnlem  21199  iccntr  21326  icccmplem2  21328  metdstri  21355  cnllycmp  21456  evth  21459  lebnumii  21466  ipcnlem2  21684  cncmet  21761  rrxds  21825  rrxmval  21832  rrxmet  21835  rrxdstprj1  21836  minveclem3b  21843  minveclem4  21847  ivthlem2  21864  ivthlem3  21865  ovollb2lem  21899  ovoliunlem1  21913  ovolscalem1  21924  ovolicc1  21927  ovolicc2lem4  21931  ovolicc2  21933  ovolicc  21934  voliunlem2  21961  ovolioo  21978  ioorcl2  21981  uniioovol  21988  uniioombllem2  21992  uniioombllem3a  21993  uniioombllem3  21994  uniioombllem4  21995  uniioombllem6  21997  opnmbllem  22010  volcn  22015  vitalilem2  22018  ismbf3d  22061  mbfaddlem  22067  i1fadd  22102  itg1addlem4  22106  mbfi1fseqlem6  22127  itg2seq  22149  itg2split  22156  itg2cnlem2  22169  itg2cn  22170  itgrevallem1  22201  dvcjbr  22352  dvferm1lem  22385  dvferm2lem  22387  cmvth  22392  mvth  22393  dvlip  22394  dvlip2  22396  c1liplem1  22397  dvgt0  22405  dvlt0  22406  dvge0  22407  dvle  22408  dvivthlem1  22409  lhop1lem  22414  lhop  22417  dvcnvrelem1  22418  dvcnvrelem2  22419  dvcnvre  22420  dvcvx  22421  dvfsumle  22422  dvfsumge  22423  dvfsumrlimf  22426  dvfsumlem2  22428  dvfsumlem3  22429  dvfsumlem4  22430  dvfsum2  22435  ftc1a  22438  ftc1lem4  22440  coe1mul3  22500  ply1divex  22537  plydivex  22693  aalioulem2  22729  aalioulem3  22730  aalioulem4  22731  aalioulem5  22732  aalioulem6  22733  aaliou3lem7  22745  taylthlem2  22769  mtest  22799  pilem2  22847  tangtx  22898  cosordlem  22918  efif1olem2  22930  logcnlem3  23025  logcnlem4  23026  isosctrlem2  23153  chordthmlem2  23164  chordthmlem4  23166  heron  23169  atanlogsublem  23246  atantan  23254  birthdaylem3  23283  logdifbnd  23323  emcllem1  23325  emcllem2  23326  emcllem5  23329  emcllem6  23330  harmonicbnd4  23340  fsumharmonic  23341  ftalem2  23347  ftalem5  23350  chpub  23495  logfaclbnd  23497  logfacbnd3  23498  logexprlim  23500  bposlem1  23559  bposlem9  23567  lgseisenlem1  23624  lgsquadlem1  23629  chtppilimlem1  23658  vmadivsum  23667  vmadivsumb  23668  rplogsumlem1  23669  rplogsumlem2  23670  rpvmasumlem  23672  dchrisumlem2  23675  dchrisum0re  23698  rplogsum  23712  mulogsumlem  23716  mulog2sumlem1  23719  vmalogdivsum2  23723  vmalogdivsum  23724  2vmadivsumlem  23725  log2sumbnd  23729  selbergb  23734  selberg2lem  23735  selberg2b  23737  chpdifbndlem1  23738  selberg3lem1  23742  selberg3lem2  23743  selberg3  23744  selberg4lem1  23745  selberg4  23746  pntrf  23748  pntrmax  23749  pntrsumo1  23750  selberg3r  23754  selberg4r  23755  selberg34r  23756  pntrlog2bndlem1  23762  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntrlog2bndlem6  23768  pntrlog2bnd  23769  pntpbnd1a  23770  pntpbnd2  23772  pntibndlem2  23776  pntlemg  23783  pntlemn  23785  pntlemj  23788  pntlemf  23790  pntlemo  23792  pntlem3  23794  pntleml  23796  ttgcontlem1  24188  eqeelen  24207  brbtwn2  24208  colinearalg  24213  axcgrid  24219  axsegconlem1  24220  axsegconlem3  24222  axsegconlem8  24227  axsegconlem9  24228  axsegconlem10  24229  ax5seglem3a  24233  ax5seg  24241  axpaschlem  24243  axcontlem8  24274  clwlkisclwwlklem2fv2  24783  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  extwwlkfablem2  25078  nvabs  25576  dipcj  25627  minvecolem4  25796  lt2addrd  27563  xlt2addrd  27578  fzsplit3  27599  bcm1n  27600  bhmafibid1  27632  2sqmod  27636  cnre2csqlem  27892  tpr2rico  27894  dya2ub  28241  dya2icoseg  28248  ballotlemfcc  28432  ballotlemfrcn0  28468  sgnsub  28483  signslema  28519  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamucov  28580  relgamcl  28604  subfacval3  28633  bpoly4  29821  supaddc  30041  opnmbllem0  30050  mblfinlem3  30053  mblfinlem4  30054  itg2addnclem  30066  itg2addnclem3  30068  itg2gt0cn  30070  ftc1cnnclem  30088  areacirclem1  30107  areacirclem2  30108  areacirclem4  30110  areacirclem5  30111  areacirc  30112  cntotbnd  30292  rrnmet  30325  rrndstprj1  30326  rrndstprj2  30327  icodiamlt  30756  irrapxlem2  30759  irrapxlem3  30760  irrapxlem4  30761  irrapxlem5  30762  pellexlem2  30766  pellexlem6  30770  pell1qrgaplem  30809  rmspecfund  30845  rmspecpos  30852  jm2.24nn  30897  jm2.17c  30900  fzmaxdif  30919  acongeq  30921  modabsdifz  30927  jm3.1lem2  30960  areaquad  31184  cvgdvgrat  31194  hashnzfzclim  31227  binomcxplemdvbinom  31258  oddfl  31459  lefldiveq  31482  fperiodmul  31504  fzdifsuc2  31512  iccshift  31558  iooshift  31562  fmul01lt1lem2  31579  climinf  31612  sumnnodd  31636  ltmod  31644  lptre2pt  31646  fperdvper  31715  dvbdfbdioolem1  31725  dvbdfbdioolem2  31726  dvbdfbdioo  31727  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnmul  31740  iblspltprt  31772  itgspltprt  31778  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  stoweidlem1  31783  stoweidlem11  31793  stoweidlem12  31794  stoweidlem13  31795  stoweidlem14  31796  stoweidlem23  31805  stoweidlem24  31806  stoweidlem25  31807  stoweidlem26  31808  stoweidlem34  31816  stoweidlem40  31822  stoweidlem41  31823  stoweidlem42  31824  stoweidlem45  31827  stoweidlem60  31842  stoweidlem62  31844  wallispilem3  31849  wallispilem4  31850  wallispi  31852  wallispi2lem1  31853  stirlinglem5  31860  stirlinglem11  31866  stirlinglem12  31867  dirkercncflem1  31885  fourierdlem4  31893  fourierdlem6  31895  fourierdlem7  31896  fourierdlem9  31898  fourierdlem13  31902  fourierdlem14  31903  fourierdlem15  31904  fourierdlem19  31908  fourierdlem26  31915  fourierdlem35  31924  fourierdlem39  31928  fourierdlem40  31929  fourierdlem41  31930  fourierdlem42  31931  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem51  31940  fourierdlem56  31945  fourierdlem57  31946  fourierdlem59  31948  fourierdlem60  31949  fourierdlem61  31950  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem66  31955  fourierdlem68  31957  fourierdlem71  31960  fourierdlem72  31961  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem78  31967  fourierdlem79  31968  fourierdlem81  31970  fourierdlem82  31971  fourierdlem83  31972  fourierdlem84  31973  fourierdlem88  31977  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem92  31981  fourierdlem93  31982  fourierdlem95  31984  fourierdlem97  31986  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fourierdlem107  31996  fourierdlem109  31998  fourierdlem111  32000  fouriersw  32014  elaa2lem  32016  etransclem23  32040  ltsubsubaddltsub  32324  2elfz2melfz  32334  ply1mulgsumlem2  32987  imo72b2lem0  37982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-po 4805  df-so 4806  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-ltxr 9654  df-sub 9830  df-neg 9831