Theorem resubcld 10047

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

Syntax hints:   -> wi 4   e. wcel 1887  (class class class)co 6290   RRcr 9538   - cmin 9860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-po 4755  df-so 4756  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-er 7363  df-en 7570  df-dom 7571  df-sdom 7572  df-pnf 9677  df-mnf 9678  df-ltxr 9680  df-sub 9862  df-neg 9863

This theorem is referenced by:  ltsubadd  10084  lesubadd  10086  lesub1  10108  lesub2  10109  ltsub1  10110  ltsub2  10111  lt2sub  10112  le2sub  10113  ltmul1a  10454  supaddc  10574  cru  10601  qbtwnre  11492  lincmb01cmp  11775  iccf1o  11776  xov1plusxeqvd  11778  intfracq  12086  fldiv  12087  modlt  12107  modsubdir  12158  serle  12268  expmulnbnd  12404  discr  12409  fzsdom2  12600  cshwidxmod  12905  crre  13177  remullem  13191  sqrlem7  13312  absrdbnd  13404  fzomaxdiflem  13405  caubnd2  13420  amgm2  13432  icodiamlt  13497  mulcn2  13659  reccn2  13660  rlimo1  13680  climle  13703  climsqz  13704  climsqz2  13705  rlimle  13711  isercolllem1  13728  climsup  13733  caucvgrlem  13736  caucvgrlemOLD  13737  caucvgrlem2  13740  iseraltlem2  13749  iseraltlem3  13750  iseralt  13751  fsumle  13859  cvgcmp  13876  cvgcmpce  13878  bpoly4  14112  eflt  14171  resinhcl  14210  tanhlt1  14214  sin01bnd  14239  sin01gt0  14244  moddvds  14312  bitscmp  14412  bitsinv1lem  14415  smueqlem  14464  modprm0  14756  pcbc  14845  4sqlem15OLD  14903  4sqlem15  14909  blss2ps  21418  blss2  21419  blssps  21439  blss  21440  nm2dif  21638  nlmvscnlem2  21688  nrginvrcnlem  21693  iccntr  21839  icccmplem2  21841  metdstri  21868  metdstriOLD  21883  cnllycmp  21984  evth  21987  lebnumii  21997  ipcnlem2  22215  cncmet  22290  rrxds  22352  rrxmval  22359  rrxmet  22362  rrxdstprj1  22363  minveclem3b  22370  minveclem4  22374  minveclem3bOLD  22382  minveclem4OLD  22386  ivthlem2  22403  ivthlem3  22404  ovollb2lem  22441  ovoliunlem1  22455  ovolscalem1  22466  ovolicc1  22469  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  ovolicc2  22476  ovolicc  22477  voliunlem2  22504  ovolioo  22521  ioorcl2  22524  uniioovol  22536  uniioombllem2  22540  uniioombllem2OLD  22541  uniioombllem3a  22542  uniioombllem3  22543  uniioombllem4  22544  uniioombllem6  22546  opnmbllem  22559  volcn  22564  vitalilem2  22567  ismbf3d  22610  mbfaddlem  22616  i1fadd  22653  itg1addlem4  22657  mbfi1fseqlem6  22678  itg2seq  22700  itg2split  22707  itg2cnlem2  22720  itg2cn  22721  itgrevallem1  22752  dvcjbr  22903  dvferm1lem  22936  dvferm2lem  22938  cmvth  22943  mvth  22944  dvlip  22945  dvlip2  22947  c1liplem1  22948  dvgt0  22956  dvlt0  22957  dvge0  22958  dvle  22959  dvivthlem1  22960  lhop1lem  22965  lhop  22968  dvcnvrelem1  22969  dvcnvrelem2  22970  dvcnvre  22971  dvcvx  22972  dvfsumle  22973  dvfsumge  22974  dvfsumrlimf  22977  dvfsumlem2  22979  dvfsumlem3  22980  dvfsumlem4  22981  dvfsum2  22986  ftc1a  22989  ftc1lem4  22991  coe1mul3  23048  ply1divex  23087  plydivex  23250  aalioulem2  23289  aalioulem3  23290  aalioulem4  23291  aalioulem5  23292  aalioulem6  23293  aaliou3lem7  23305  taylthlem2  23329  mtest  23359  pilem2  23407  pilem2OLD  23408  tangtx  23460  cosordlem  23480  efif1olem2  23492  logcnlem3  23589  logcnlem4  23590  isosctrlem2  23748  chordthmlem2  23759  chordthmlem4  23761  heron  23764  atanlogsublem  23841  atantan  23849  birthdaylem3  23879  logdifbnd  23919  emcllem1  23921  emcllem2  23922  emcllem5  23925  emcllem6  23926  harmonicbnd4  23936  fsumharmonic  23937  lgamgulmlem2  23955  lgamgulmlem3  23956  lgamucov  23963  relgamcl  23987  ftalem2  23998  ftalem5  24001  ftalem5OLD  24003  chpub  24148  logfaclbnd  24150  logfacbnd3  24151  logexprlim  24153  bposlem1  24212  bposlem9  24220  lgseisenlem1  24277  lgsquadlem1  24282  chtppilimlem1  24311  vmadivsum  24320  vmadivsumb  24321  rplogsumlem1  24322  rplogsumlem2  24323  rpvmasumlem  24325  dchrisumlem2  24328  dchrisum0re  24351  rplogsum  24365  mulogsumlem  24369  mulog2sumlem1  24372  vmalogdivsum2  24376  vmalogdivsum  24377  2vmadivsumlem  24378  log2sumbnd  24382  selbergb  24387  selberg2lem  24388  selberg2b  24390  chpdifbndlem1  24391  selberg3lem1  24395  selberg3lem2  24396  selberg3  24397  selberg4lem1  24398  selberg4  24399  pntrf  24401  pntrmax  24402  pntrsumo1  24403  selberg3r  24407  selberg4r  24408  selberg34r  24409  pntrlog2bndlem1  24415  pntrlog2bndlem2  24416  pntrlog2bndlem3  24417  pntrlog2bndlem4  24418  pntrlog2bndlem5  24419  pntrlog2bndlem6  24421  pntrlog2bnd  24422  pntpbnd1a  24423  pntpbnd2  24425  pntibndlem2  24429  pntlemg  24436  pntlemn  24438  pntlemj  24441  pntlemf  24443  pntlemo  24445  pntlem3  24447  pntleml  24449  ttgcontlem1  24915  eqeelen  24934  brbtwn2  24935  colinearalg  24940  axcgrid  24946  axsegconlem1  24947  axsegconlem3  24949  axsegconlem8  24954  axsegconlem9  24955  axsegconlem10  24956  ax5seglem3a  24960  ax5seg  24968  axpaschlem  24970  axcontlem8  25001  clwlkisclwwlklem2fv2  25511  clwlkisclwwlklem2a4  25512  clwlkisclwwlklem2a  25513  extwwlkfablem2  25806  nvabs  26302  dipcj  26353  minvecolem4  26522  minvecolem4OLD  26532  lt2addrd  28326  xlt2addrd  28338  fzsplit3  28370  bcm1n  28371  bhmafibid1  28405  2sqmod  28409  submateqlem1  28633  cnre2csqlem  28716  tpr2rico  28718  dya2ub  29092  dya2icoseg  29099  ballotlemfcc  29326  ballotlemfrcn0  29362  ballotlemfrcn0OLD  29400  sgnsub  29415  signslema  29451  subfacval3  29912  poimirlem29  31969  broucube  31974  opnmbllem0  31976  mblfinlem3  31979  mblfinlem4  31980  itg2addnclem  31993  itg2addnclem3  31995  itg2gt0cn  31997  ftc1cnnclem  32015  areacirclem1  32032  areacirclem2  32033  areacirclem4  32035  areacirclem5  32036  areacirc  32037  cntotbnd  32128  rrnmet  32161  rrndstprj1  32162  rrndstprj2  32163  irrapxlem2  35667  irrapxlem3  35668  irrapxlem4  35669  irrapxlem5  35670  pellexlem2  35674  pellexlem6  35678  pell1qrgaplem  35719  rmspecfund  35757  rmspecpos  35764  jm2.24nn  35809  jm2.17c  35812  fzmaxdif  35831  acongeq  35833  modabsdifz  35839  jm3.1lem2  35873  areaquad  36101  imo72b2lem0  36608  cvgdvgrat  36662  hashnzfzclim  36671  binomcxplemdvbinom  36702  oddfl  37487  lefldiveq  37506  fperiodmul  37522  fzdifsuc2  37530  suprltrp  37551  supxrgere  37556  supxrgelem  37560  suplesup  37562  iccshift  37619  iooshift  37623  fmul01lt1lem2  37663  climinf  37684  climinfOLD  37685  sumnnodd  37710  ltmod  37718  lptre2pt  37720  fperdvper  37790  dvbdfbdioolem1  37800  dvbdfbdioolem2  37801  dvbdfbdioo  37802  ioodvbdlimc1lem1  37803  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem1OLD  37805  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  dvnmul  37818  iblspltprt  37850  itgspltprt  37856  itgiccshift  37857  itgperiod  37858  itgsbtaddcnst  37859  stoweidlem1  37861  stoweidlem11  37871  stoweidlem12  37872  stoweidlem13  37873  stoweidlem14  37874  stoweidlem23  37883  stoweidlem24  37884  stoweidlem25  37885  stoweidlem26  37886  stoweidlem34  37895  stoweidlem40  37901  stoweidlem41  37902  stoweidlem42  37903  stoweidlem45  37906  stoweidlem60  37921  stoweidlem62  37923  stoweidlem62OLD  37924  wallispilem3  37929  wallispilem4  37930  wallispi  37932  wallispi2lem1  37933  stirlinglem5  37940  stirlinglem11  37946  stirlinglem12  37947  dirkercncflem1  37965  fourierdlem4  37973  fourierdlem6  37975  fourierdlem7  37976  fourierdlem9  37978  fourierdlem13  37982  fourierdlem14  37983  fourierdlem15  37984  fourierdlem19  37988  fourierdlem26  37995  fourierdlem35  38005  fourierdlem39  38009  fourierdlem40  38010  fourierdlem41  38011  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem48  38018  fourierdlem49  38019  fourierdlem50  38020  fourierdlem51  38021  fourierdlem56  38026  fourierdlem57  38027  fourierdlem59  38029  fourierdlem60  38030  fourierdlem61  38031  fourierdlem63  38033  fourierdlem64  38034  fourierdlem65  38035  fourierdlem66  38036  fourierdlem68  38038  fourierdlem71  38041  fourierdlem72  38042  fourierdlem73  38043  fourierdlem74  38044  fourierdlem75  38045  fourierdlem76  38046  fourierdlem78  38048  fourierdlem79  38049  fourierdlem81  38051  fourierdlem82  38052  fourierdlem83  38053  fourierdlem84  38054  fourierdlem88  38058  fourierdlem89  38059  fourierdlem90  38060  fourierdlem91  38061  fourierdlem92  38062  fourierdlem93  38063  fourierdlem95  38065  fourierdlem97  38067  fourierdlem101  38071  fourierdlem103  38073  fourierdlem104  38074  fourierdlem107  38077  fourierdlem109  38079  fourierdlem111  38081  fouriersw  38095  elaa2lem  38097  elaa2lemOLD  38098  etransclem23  38122  rrxdsfi  38154  rrxtopnfi  38155  rrndistlt  38159  sge0gtfsumgt  38285  iundjiun  38298  volicorecl  38368  hoiprodcl  38369  hoiprodcl3  38402  volicore  38403  hoidmvcl  38404  hoidmv1lelem2  38414  hoidmv1lelem3  38415  hoidmv1le  38416  hoidmvlelem1  38417  hoidmvlelem2  38418  hoiqssbllem1  38444  hoiqssbllem2  38445  hoiqssbllem3  38446  hspmbllem1  38448  bgoldbtbndlem2  38901  bgoldbtbndlem3  38902  bgoldbtbndlem4  38903  bgoldbtbnd  38904  ltsubsubaddltsub  39048  2elfz2melfz  39058  nbusgrvtxm1  39453  ply1mulgsumlem2  40232  difmodm1lt  40378  nnpw2pmod  40447  dignn0flhalflem1  40479