Theorem resubcld 9983

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 9874	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
4	1, 2, 3	syl2anc 659	1 |- ( ph -> ( A - B ) e. RR )

Syntax hints:   -> wi 4   e. wcel 1823  (class class class)co 6270   RRcr 9480   - cmin 9796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-po 4789  df-so 4790  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-ltxr 9622  df-sub 9798  df-neg 9799

This theorem is referenced by:  ltsubadd  10018  lesubadd  10020  lesub1  10042  lesub2  10043  ltsub1  10044  ltsub2  10045  lt2sub  10046  le2sub  10047  ltmul1a  10387  cru  10523  qbtwnre  11401  lincmb01cmp  11666  iccf1o  11667  xov1plusxeqvd  11669  intfracq  11968  fldiv  11969  modlt  11988  modsubdir  12037  serle  12144  expmulnbnd  12280  discr  12285  fzsdom2  12470  cshwidxmod  12765  crre  13029  remullem  13043  sqrlem7  13164  absrdbnd  13256  fzomaxdiflem  13257  caubnd2  13272  amgm2  13284  mulcn2  13500  reccn2  13501  rlimo1  13521  climle  13544  climsqz  13545  climsqz2  13546  rlimle  13552  isercolllem1  13569  climsup  13574  caucvgrlem  13577  caucvgrlem2  13579  iseraltlem2  13587  iseraltlem3  13588  iseralt  13589  fsumle  13695  cvgcmp  13712  cvgcmpce  13714  eflt  13934  resinhcl  13973  tanhlt1  13977  sin01bnd  14002  sin01gt0  14007  moddvds  14077  bitscmp  14172  bitsinv1lem  14175  smueqlem  14224  modprm0  14414  pcbc  14503  4sqlem15  14561  blss2ps  21072  blss2  21073  blssps  21093  blss  21094  nm2dif  21310  nlmvscnlem2  21360  nrginvrcnlem  21365  iccntr  21492  icccmplem2  21494  metdstri  21521  cnllycmp  21622  evth  21625  lebnumii  21632  ipcnlem2  21850  cncmet  21927  rrxds  21991  rrxmval  21998  rrxmet  22001  rrxdstprj1  22002  minveclem3b  22009  minveclem4  22013  ivthlem2  22030  ivthlem3  22031  ovollb2lem  22065  ovoliunlem1  22079  ovolscalem1  22090  ovolicc1  22093  ovolicc2lem4  22097  ovolicc2  22099  ovolicc  22100  voliunlem2  22127  ovolioo  22144  ioorcl2  22147  uniioovol  22154  uniioombllem2  22158  uniioombllem3a  22159  uniioombllem3  22160  uniioombllem4  22161  uniioombllem6  22163  opnmbllem  22176  volcn  22181  vitalilem2  22184  ismbf3d  22227  mbfaddlem  22233  i1fadd  22268  itg1addlem4  22272  mbfi1fseqlem6  22293  itg2seq  22315  itg2split  22322  itg2cnlem2  22335  itg2cn  22336  itgrevallem1  22367  dvcjbr  22518  dvferm1lem  22551  dvferm2lem  22553  cmvth  22558  mvth  22559  dvlip  22560  dvlip2  22562  c1liplem1  22563  dvgt0  22571  dvlt0  22572  dvge0  22573  dvle  22574  dvivthlem1  22575  lhop1lem  22580  lhop  22583  dvcnvrelem1  22584  dvcnvrelem2  22585  dvcnvre  22586  dvcvx  22587  dvfsumle  22588  dvfsumge  22589  dvfsumrlimf  22592  dvfsumlem2  22594  dvfsumlem3  22595  dvfsumlem4  22596  dvfsum2  22601  ftc1a  22604  ftc1lem4  22606  coe1mul3  22666  ply1divex  22703  plydivex  22859  aalioulem2  22895  aalioulem3  22896  aalioulem4  22897  aalioulem5  22898  aalioulem6  22899  aaliou3lem7  22911  taylthlem2  22935  mtest  22965  pilem2  23013  tangtx  23064  cosordlem  23084  efif1olem2  23096  logcnlem3  23193  logcnlem4  23194  isosctrlem2  23350  chordthmlem2  23361  chordthmlem4  23363  heron  23366  atanlogsublem  23443  atantan  23451  birthdaylem3  23481  logdifbnd  23521  emcllem1  23523  emcllem2  23524  emcllem5  23527  emcllem6  23528  harmonicbnd4  23538  fsumharmonic  23539  ftalem2  23545  ftalem5  23548  chpub  23693  logfaclbnd  23695  logfacbnd3  23696  logexprlim  23698  bposlem1  23757  bposlem9  23765  lgseisenlem1  23822  lgsquadlem1  23827  chtppilimlem1  23856  vmadivsum  23865  vmadivsumb  23866  rplogsumlem1  23867  rplogsumlem2  23868  rpvmasumlem  23870  dchrisumlem2  23873  dchrisum0re  23896  rplogsum  23910  mulogsumlem  23914  mulog2sumlem1  23917  vmalogdivsum2  23921  vmalogdivsum  23922  2vmadivsumlem  23923  log2sumbnd  23927  selbergb  23932  selberg2lem  23933  selberg2b  23935  chpdifbndlem1  23936  selberg3lem1  23940  selberg3lem2  23941  selberg3  23942  selberg4lem1  23943  selberg4  23944  pntrf  23946  pntrmax  23947  pntrsumo1  23948  selberg3r  23952  selberg4r  23953  selberg34r  23954  pntrlog2bndlem1  23960  pntrlog2bndlem2  23961  pntrlog2bndlem3  23962  pntrlog2bndlem4  23963  pntrlog2bndlem5  23964  pntrlog2bndlem6  23966  pntrlog2bnd  23967  pntpbnd1a  23968  pntpbnd2  23970  pntibndlem2  23974  pntlemg  23981  pntlemn  23983  pntlemj  23986  pntlemf  23988  pntlemo  23990  pntlem3  23992  pntleml  23994  ttgcontlem1  24390  eqeelen  24409  brbtwn2  24410  colinearalg  24415  axcgrid  24421  axsegconlem1  24422  axsegconlem3  24424  axsegconlem8  24429  axsegconlem9  24430  axsegconlem10  24431  ax5seglem3a  24435  ax5seg  24443  axpaschlem  24445  axcontlem8  24476  clwlkisclwwlklem2fv2  24985  clwlkisclwwlklem2a4  24986  clwlkisclwwlklem2a  24987  extwwlkfablem2  25280  nvabs  25774  dipcj  25825  minvecolem4  25994  lt2addrd  27794  xlt2addrd  27809  fzsplit3  27833  bcm1n  27834  bhmafibid1  27866  2sqmod  27870  cnre2csqlem  28127  tpr2rico  28129  dya2ub  28478  dya2icoseg  28485  ballotlemfcc  28696  ballotlemfrcn0  28732  sgnsub  28747  signslema  28783  lgamgulmlem2  28836  lgamgulmlem3  28837  lgamucov  28844  relgamcl  28868  subfacval3  28897  bpoly4  30049  supaddc  30281  opnmbllem0  30290  mblfinlem3  30293  mblfinlem4  30294  itg2addnclem  30306  itg2addnclem3  30308  itg2gt0cn  30310  ftc1cnnclem  30328  areacirclem1  30347  areacirclem2  30348  areacirclem4  30350  areacirclem5  30351  areacirc  30352  cntotbnd  30532  rrnmet  30565  rrndstprj1  30566  rrndstprj2  30567  icodiamlt  30995  irrapxlem2  30998  irrapxlem3  30999  irrapxlem4  31000  irrapxlem5  31001  pellexlem2  31005  pellexlem6  31009  pell1qrgaplem  31048  rmspecfund  31084  rmspecpos  31091  jm2.24nn  31136  jm2.17c  31139  fzmaxdif  31158  acongeq  31160  modabsdifz  31166  jm3.1lem2  31199  areaquad  31425  cvgdvgrat  31435  hashnzfzclim  31468  binomcxplemdvbinom  31499  oddfl  31699  lefldiveq  31722  fperiodmul  31743  fzdifsuc2  31751  iccshift  31797  iooshift  31801  fmul01lt1lem2  31818  climinf  31851  sumnnodd  31875  ltmod  31883  lptre2pt  31885  fperdvper  31954  dvbdfbdioolem1  31964  dvbdfbdioolem2  31965  dvbdfbdioo  31966  ioodvbdlimc1lem1  31967  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvnmul  31979  iblspltprt  32011  itgspltprt  32017  itgiccshift  32018  itgperiod  32019  itgsbtaddcnst  32020  stoweidlem1  32022  stoweidlem11  32032  stoweidlem12  32033  stoweidlem13  32034  stoweidlem14  32035  stoweidlem23  32044  stoweidlem24  32045  stoweidlem25  32046  stoweidlem26  32047  stoweidlem34  32055  stoweidlem40  32061  stoweidlem41  32062  stoweidlem42  32063  stoweidlem45  32066  stoweidlem60  32081  stoweidlem62  32083  wallispilem3  32088  wallispilem4  32089  wallispi  32091  wallispi2lem1  32092  stirlinglem5  32099  stirlinglem11  32105  stirlinglem12  32106  dirkercncflem1  32124  fourierdlem4  32132  fourierdlem6  32134  fourierdlem7  32135  fourierdlem9  32137  fourierdlem13  32141  fourierdlem14  32142  fourierdlem15  32143  fourierdlem19  32147  fourierdlem26  32154  fourierdlem35  32163  fourierdlem39  32167  fourierdlem40  32168  fourierdlem41  32169  fourierdlem42  32170  fourierdlem48  32176  fourierdlem49  32177  fourierdlem50  32178  fourierdlem51  32179  fourierdlem56  32184  fourierdlem57  32185  fourierdlem59  32187  fourierdlem60  32188  fourierdlem61  32189  fourierdlem63  32191  fourierdlem64  32192  fourierdlem65  32193  fourierdlem66  32194  fourierdlem68  32196  fourierdlem71  32199  fourierdlem72  32200  fourierdlem73  32201  fourierdlem74  32202  fourierdlem75  32203  fourierdlem76  32204  fourierdlem78  32206  fourierdlem79  32207  fourierdlem81  32209  fourierdlem82  32210  fourierdlem83  32211  fourierdlem84  32212  fourierdlem88  32216  fourierdlem89  32217  fourierdlem90  32218  fourierdlem91  32219  fourierdlem92  32220  fourierdlem93  32221  fourierdlem95  32223  fourierdlem97  32225  fourierdlem101  32229  fourierdlem103  32231  fourierdlem104  32232  fourierdlem107  32235  fourierdlem109  32237  fourierdlem111  32239  fouriersw  32253  elaa2lem  32255  etransclem23  32279  ltsubsubaddltsub  32698  2elfz2melfz  32708  ply1mulgsumlem2  33241  difmodm1lt  33389  nnpw2pmod  33458  dignn0flhalflem1  33490  imo72b2lem0  38434