Theorem resubcld 10036

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

Hypotheses

Ref	Expression
renegcld.1	|- ( ph -> A e. RR )
resubcld.2	|- ( ph -> B e. RR )

Assertion

Ref	Expression
resubcld	|- ( ph -> ( A - B ) e. RR )

Proof of Theorem resubcld

Step	Hyp	Ref	Expression
1		renegcld.1	. 2 |- ( ph -> A e. RR )
2		resubcld.2	. 2 |- ( ph -> B e. RR )
3		resubcl 9927	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
4	1, 2, 3	syl2anc 665	1 |- ( ph -> ( A - B ) e. RR )

Syntax hints:   -> wi 4   e. wcel 1867  (class class class)co 6296   RRcr 9527   - cmin 9849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  df-po 4766  df-so 4767  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-er 7362  df-en 7569  df-dom 7570  df-sdom 7571  df-pnf 9666  df-mnf 9667  df-ltxr 9669  df-sub 9851  df-neg 9852

This theorem is referenced by:  ltsubadd  10073  lesubadd  10075  lesub1  10097  lesub2  10098  ltsub1  10099  ltsub2  10100  lt2sub  10101  le2sub  10102  ltmul1a  10443  supaddc  10563  cru  10590  qbtwnre  11481  lincmb01cmp  11762  iccf1o  11763  xov1plusxeqvd  11765  intfracq  12072  fldiv  12073  modlt  12093  modsubdir  12144  serle  12254  expmulnbnd  12390  discr  12395  fzsdom2  12584  cshwidxmod  12879  crre  13145  remullem  13159  sqrlem7  13280  absrdbnd  13372  fzomaxdiflem  13373  caubnd2  13388  amgm2  13400  mulcn2  13626  reccn2  13627  rlimo1  13647  climle  13670  climsqz  13671  climsqz2  13672  rlimle  13678  isercolllem1  13695  climsup  13700  caucvgrlem  13703  caucvgrlemOLD  13704  caucvgrlem2  13707  iseraltlem2  13716  iseraltlem3  13717  iseralt  13718  fsumle  13826  cvgcmp  13843  cvgcmpce  13845  bpoly4  14079  eflt  14138  resinhcl  14177  tanhlt1  14181  sin01bnd  14206  sin01gt0  14211  moddvds  14279  bitscmp  14375  bitsinv1lem  14378  smueqlem  14427  modprm0  14708  pcbc  14797  4sqlem15OLD  14855  4sqlem15  14861  blss2ps  21342  blss2  21343  blssps  21363  blss  21364  nm2dif  21562  nlmvscnlem2  21612  nrginvrcnlem  21617  iccntr  21743  icccmplem2  21745  metdstri  21772  cnllycmp  21873  evth  21876  lebnumii  21883  ipcnlem2  22101  cncmet  22176  rrxds  22238  rrxmval  22245  rrxmet  22248  rrxdstprj1  22249  minveclem3b  22256  minveclem4  22260  ivthlem2  22277  ivthlem3  22278  ovollb2lem  22315  ovoliunlem1  22329  ovolscalem1  22340  ovolicc1  22343  ovolicc2lem4OLD  22347  ovolicc2lem4  22348  ovolicc2  22350  ovolicc  22351  voliunlem2  22378  ovolioo  22395  ioorcl2  22398  uniioovol  22410  uniioombllem2  22414  uniioombllem2OLD  22415  uniioombllem3a  22416  uniioombllem3  22417  uniioombllem4  22418  uniioombllem6  22420  opnmbllem  22433  volcn  22438  vitalilem2  22441  ismbf3d  22484  mbfaddlem  22490  i1fadd  22527  itg1addlem4  22531  mbfi1fseqlem6  22552  itg2seq  22574  itg2split  22581  itg2cnlem2  22594  itg2cn  22595  itgrevallem1  22626  dvcjbr  22777  dvferm1lem  22810  dvferm2lem  22812  cmvth  22817  mvth  22818  dvlip  22819  dvlip2  22821  c1liplem1  22822  dvgt0  22830  dvlt0  22831  dvge0  22832  dvle  22833  dvivthlem1  22834  lhop1lem  22839  lhop  22842  dvcnvrelem1  22843  dvcnvrelem2  22844  dvcnvre  22845  dvcvx  22846  dvfsumle  22847  dvfsumge  22848  dvfsumrlimf  22851  dvfsumlem2  22853  dvfsumlem3  22854  dvfsumlem4  22855  dvfsum2  22860  ftc1a  22863  ftc1lem4  22865  coe1mul3  22922  ply1divex  22959  plydivex  23115  aalioulem2  23151  aalioulem3  23152  aalioulem4  23153  aalioulem5  23154  aalioulem6  23155  aaliou3lem7  23167  taylthlem2  23191  mtest  23221  pilem2  23269  pilem2OLD  23270  tangtx  23322  cosordlem  23342  efif1olem2  23354  logcnlem3  23451  logcnlem4  23452  isosctrlem2  23610  chordthmlem2  23621  chordthmlem4  23623  heron  23626  atanlogsublem  23703  atantan  23711  birthdaylem3  23741  logdifbnd  23781  emcllem1  23783  emcllem2  23784  emcllem5  23787  emcllem6  23788  harmonicbnd4  23798  fsumharmonic  23799  lgamgulmlem2  23817  lgamgulmlem3  23818  lgamucov  23825  relgamcl  23849  ftalem2  23860  ftalem5  23863  chpub  24008  logfaclbnd  24010  logfacbnd3  24011  logexprlim  24013  bposlem1  24072  bposlem9  24080  lgseisenlem1  24137  lgsquadlem1  24142  chtppilimlem1  24171  vmadivsum  24180  vmadivsumb  24181  rplogsumlem1  24182  rplogsumlem2  24183  rpvmasumlem  24185  dchrisumlem2  24188  dchrisum0re  24211  rplogsum  24225  mulogsumlem  24229  mulog2sumlem1  24232  vmalogdivsum2  24236  vmalogdivsum  24237  2vmadivsumlem  24238  log2sumbnd  24242  selbergb  24247  selberg2lem  24248  selberg2b  24250  chpdifbndlem1  24251  selberg3lem1  24255  selberg3lem2  24256  selberg3  24257  selberg4lem1  24258  selberg4  24259  pntrf  24261  pntrmax  24262  pntrsumo1  24263  selberg3r  24267  selberg4r  24268  selberg34r  24269  pntrlog2bndlem1  24275  pntrlog2bndlem2  24276  pntrlog2bndlem3  24277  pntrlog2bndlem4  24278  pntrlog2bndlem5  24279  pntrlog2bndlem6  24281  pntrlog2bnd  24282  pntpbnd1a  24283  pntpbnd2  24285  pntibndlem2  24289  pntlemg  24296  pntlemn  24298  pntlemj  24301  pntlemf  24303  pntlemo  24305  pntlem3  24307  pntleml  24309  ttgcontlem1  24758  eqeelen  24777  brbtwn2  24778  colinearalg  24783  axcgrid  24789  axsegconlem1  24790  axsegconlem3  24792  axsegconlem8  24797  axsegconlem9  24798  axsegconlem10  24799  ax5seglem3a  24803  ax5seg  24811  axpaschlem  24813  axcontlem8  24844  clwlkisclwwlklem2fv2  25353  clwlkisclwwlklem2a4  25354  clwlkisclwwlklem2a  25355  extwwlkfablem2  25648  nvabs  26144  dipcj  26195  minvecolem4  26364  lt2addrd  28166  xlt2addrd  28176  fzsplit3  28203  bcm1n  28204  bhmafibid1  28240  2sqmod  28244  submateqlem1  28469  cnre2csqlem  28552  tpr2rico  28554  dya2ub  28928  dya2icoseg  28935  ballotlemfcc  29149  ballotlemfrcn0  29185  sgnsub  29200  signslema  29236  subfacval3  29697  poimirlem29  31673  broucube  31678  opnmbllem0  31680  mblfinlem3  31683  mblfinlem4  31684  itg2addnclem  31697  itg2addnclem3  31699  itg2gt0cn  31701  ftc1cnnclem  31719  areacirclem1  31736  areacirclem2  31737  areacirclem4  31739  areacirclem5  31740  areacirc  31741  cntotbnd  31832  rrnmet  31865  rrndstprj1  31866  rrndstprj2  31867  icodiamlt  35374  irrapxlem2  35377  irrapxlem3  35378  irrapxlem4  35379  irrapxlem5  35380  pellexlem2  35384  pellexlem6  35388  pell1qrgaplem  35429  rmspecfund  35467  rmspecpos  35474  jm2.24nn  35519  jm2.17c  35522  fzmaxdif  35541  acongeq  35543  modabsdifz  35549  jm3.1lem2  35583  areaquad  35804  imo72b2lem0  36249  cvgdvgrat  36303  hashnzfzclim  36312  binomcxplemdvbinom  36343  oddfl  37100  lefldiveq  37119  fperiodmul  37135  fzdifsuc2  37143  suprltrp  37164  supxrgere  37169  supxrgelem  37173  suplesup  37175  iccshift  37208  iooshift  37212  fmul01lt1lem2  37239  climinf  37260  climinfOLD  37261  sumnnodd  37286  ltmod  37294  lptre2pt  37296  fperdvper  37366  dvbdfbdioolem1  37376  dvbdfbdioolem2  37377  dvbdfbdioo  37378  ioodvbdlimc1lem1  37379  ioodvbdlimc1lem2  37380  ioodvbdlimc2lem  37382  dvnmul  37391  iblspltprt  37423  itgspltprt  37429  itgiccshift  37430  itgperiod  37431  itgsbtaddcnst  37432  stoweidlem1  37434  stoweidlem11  37444  stoweidlem12  37445  stoweidlem13  37446  stoweidlem14  37447  stoweidlem23  37456  stoweidlem24  37457  stoweidlem25  37458  stoweidlem26  37459  stoweidlem34  37468  stoweidlem40  37474  stoweidlem41  37475  stoweidlem42  37476  stoweidlem45  37479  stoweidlem60  37494  stoweidlem62  37496  stoweidlem62OLD  37497  wallispilem3  37502  wallispilem4  37503  wallispi  37505  wallispi2lem1  37506  stirlinglem5  37513  stirlinglem11  37519  stirlinglem12  37520  dirkercncflem1  37538  fourierdlem4  37546  fourierdlem6  37548  fourierdlem7  37549  fourierdlem9  37551  fourierdlem13  37555  fourierdlem14  37556  fourierdlem15  37557  fourierdlem19  37561  fourierdlem26  37568  fourierdlem35  37577  fourierdlem39  37581  fourierdlem40  37582  fourierdlem41  37583  fourierdlem42  37584  fourierdlem48  37590  fourierdlem49  37591  fourierdlem50  37592  fourierdlem51  37593  fourierdlem56  37598  fourierdlem57  37599  fourierdlem59  37601  fourierdlem60  37602  fourierdlem61  37603  fourierdlem63  37605  fourierdlem64  37606  fourierdlem65  37607  fourierdlem66  37608  fourierdlem68  37610  fourierdlem71  37613  fourierdlem72  37614  fourierdlem73  37615  fourierdlem74  37616  fourierdlem75  37617  fourierdlem76  37618  fourierdlem78  37620  fourierdlem79  37621  fourierdlem81  37623  fourierdlem82  37624  fourierdlem83  37625  fourierdlem84  37626  fourierdlem88  37630  fourierdlem89  37631  fourierdlem90  37632  fourierdlem91  37633  fourierdlem92  37634  fourierdlem93  37635  fourierdlem95  37637  fourierdlem97  37639  fourierdlem101  37643  fourierdlem103  37645  fourierdlem104  37646  fourierdlem107  37649  fourierdlem109  37651  fourierdlem111  37653  fouriersw  37667  elaa2lem  37669  etransclem23  37693  iundjiun  37811  bgoldbtbndlem2  38304  bgoldbtbndlem3  38305  bgoldbtbndlem4  38306  bgoldbtbnd  38307  ltsubsubaddltsub  38410  2elfz2melfz  38420  ply1mulgsumlem2  38952  difmodm1lt  39099  nnpw2pmod  39168  dignn0flhalflem1  39200