Theorem resubcld 9877

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

Syntax hints:   -> wi 4   e. wcel 1758  (class class class)co 6190   RRcr 9382   - cmin 9696

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-po 4739  df-so 4740  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-riota 6151  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-er 7201  df-en 7411  df-dom 7412  df-sdom 7413  df-pnf 9521  df-mnf 9522  df-ltxr 9524  df-sub 9698  df-neg 9699

This theorem is referenced by:  ltsubadd  9910  lesubadd  9912  lesub1  9934  lesub2  9935  ltsub1  9936  ltsub2  9937  lt2sub  9938  le2sub  9939  ltmul1a  10279  cru  10415  qbtwnre  11270  lincmb01cmp  11529  iccf1o  11530  xov1plusxeqvd  11532  intfracq  11799  fldiv  11800  modlt  11819  modsubdir  11868  serle  11962  expmulnbnd  12097  discr  12102  fzsdom2  12291  cshwidxmod  12542  crre  12705  remullem  12719  sqrlem7  12840  absrdbnd  12931  fzomaxdiflem  12932  caubnd2  12947  amgm2  12959  mulcn2  13175  reccn2  13176  rlimo1  13196  climle  13219  climsqz  13220  climsqz2  13221  rlimle  13227  isercolllem1  13244  climsup  13249  caucvgrlem  13252  caucvgrlem2  13254  iseraltlem2  13262  iseraltlem3  13263  iseralt  13264  fsumle  13364  cvgcmp  13381  cvgcmpce  13383  eflt  13503  resinhcl  13542  tanhlt1  13546  sin01bnd  13571  sin01gt0  13576  moddvds  13644  bitscmp  13736  bitsinv1lem  13739  smueqlem  13788  modprm0  13975  pcbc  14064  4sqlem15  14122  blss2ps  20094  blss2  20095  blssps  20115  blss  20116  nm2dif  20332  nlmvscnlem2  20382  nrginvrcnlem  20387  iccntr  20514  icccmplem2  20516  metdstri  20543  cnllycmp  20644  evth  20647  lebnumii  20654  ipcnlem2  20872  cncmet  20949  rrxds  21013  rrxmval  21020  rrxmet  21023  rrxdstprj1  21024  minveclem3b  21031  minveclem4  21035  ivthlem2  21052  ivthlem3  21053  ovollb2lem  21087  ovoliunlem1  21101  ovolscalem1  21112  ovolicc1  21115  ovolicc2lem4  21119  ovolicc2  21121  ovolicc  21122  voliunlem2  21148  ovolioo  21165  ioorcl2  21168  uniioovol  21175  uniioombllem2  21179  uniioombllem3a  21180  uniioombllem3  21181  uniioombllem4  21182  uniioombllem6  21184  opnmbllem  21197  volcn  21202  vitalilem2  21205  ismbf3d  21248  mbfaddlem  21254  i1fadd  21289  itg1addlem4  21293  mbfi1fseqlem6  21314  itg2seq  21336  itg2split  21343  itg2cnlem2  21356  itg2cn  21357  itgrevallem1  21388  dvcjbr  21539  dvferm1lem  21572  dvferm2lem  21574  cmvth  21579  mvth  21580  dvlip  21581  dvlip2  21583  c1liplem1  21584  dvgt0  21592  dvlt0  21593  dvge0  21594  dvle  21595  dvivthlem1  21596  lhop1lem  21601  lhop  21604  dvcnvrelem1  21605  dvcnvrelem2  21606  dvcnvre  21607  dvcvx  21608  dvfsumle  21609  dvfsumge  21610  dvfsumrlimf  21613  dvfsumlem2  21615  dvfsumlem3  21616  dvfsumlem4  21617  dvfsum2  21622  ftc1a  21625  ftc1lem4  21627  coe1mul3  21687  ply1divex  21724  plydivex  21879  aalioulem2  21915  aalioulem3  21916  aalioulem4  21917  aalioulem5  21918  aalioulem6  21919  aaliou3lem7  21931  taylthlem2  21955  mtest  21985  pilem2  22033  tangtx  22083  cosordlem  22103  efif1olem2  22115  logcnlem3  22205  logcnlem4  22206  isosctrlem2  22333  chordthmlem2  22344  chordthmlem4  22346  heron  22349  atanlogsublem  22426  atantan  22434  birthdaylem3  22463  logdifbnd  22503  emcllem1  22505  emcllem2  22506  emcllem5  22509  emcllem6  22510  harmonicbnd4  22520  fsumharmonic  22521  ftalem2  22527  ftalem5  22530  chpub  22675  logfaclbnd  22677  logfacbnd3  22678  logexprlim  22680  bposlem1  22739  bposlem9  22747  lgseisenlem1  22804  lgsquadlem1  22809  chtppilimlem1  22838  vmadivsum  22847  vmadivsumb  22848  rplogsumlem1  22849  rplogsumlem2  22850  rpvmasumlem  22852  dchrisumlem2  22855  dchrisum0re  22878  rplogsum  22892  mulogsumlem  22896  mulog2sumlem1  22899  vmalogdivsum2  22903  vmalogdivsum  22904  2vmadivsumlem  22905  log2sumbnd  22909  selbergb  22914  selberg2lem  22915  selberg2b  22917  chpdifbndlem1  22918  selberg3lem1  22922  selberg3lem2  22923  selberg3  22924  selberg4lem1  22925  selberg4  22926  pntrf  22928  pntrmax  22929  pntrsumo1  22930  selberg3r  22934  selberg4r  22935  selberg34r  22936  pntrlog2bndlem1  22942  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntrlog2bndlem6  22948  pntrlog2bnd  22949  pntpbnd1a  22950  pntpbnd2  22952  pntibndlem2  22956  pntlemg  22963  pntlemn  22965  pntlemj  22968  pntlemf  22970  pntlemo  22972  pntlem3  22974  pntleml  22976  ttgcontlem1  23266  eqeelen  23285  brbtwn2  23286  colinearalg  23291  axcgrid  23297  axsegconlem1  23298  axsegconlem3  23300  axsegconlem8  23305  axsegconlem9  23306  axsegconlem10  23307  ax5seglem3a  23311  ax5seg  23319  axpaschlem  23321  axcontlem8  23352  nvabs  24196  dipcj  24247  minvecolem4  24416  lt2addrd  26170  xlt2addrd  26185  fzsplit3  26212  bcm1n  26213  cnre2csqlem  26474  tpr2rico  26476  dya2ub  26819  dya2icoseg  26826  ballotlemfcc  27010  ballotlemfrcn0  27046  sgnsub  27061  signslema  27097  lgamgulmlem2  27150  lgamgulmlem3  27151  lgamucov  27158  relgamcl  27182  subfacval3  27211  bpoly4  28336  supaddc  28555  opnmbllem0  28565  mblfinlem3  28568  mblfinlem4  28569  itg2addnclem  28581  itg2addnclem3  28583  itg2gt0cn  28585  ftc1cnnclem  28603  areacirclem1  28622  areacirclem2  28623  areacirclem4  28625  areacirclem5  28626  areacirc  28627  cntotbnd  28833  rrnmet  28866  rrndstprj1  28867  rrndstprj2  28868  icodiamlt  29299  irrapxlem2  29302  irrapxlem3  29303  irrapxlem4  29304  irrapxlem5  29305  pellexlem2  29309  pellexlem6  29313  pell1qrgaplem  29352  rmspecfund  29388  rmspecpos  29395  jm2.24nn  29440  jm2.17c  29443  fzmaxdif  29462  acongeq  29464  modabsdifz  29472  jm3.1lem2  29505  areaquad  29730  fmul01lt1lem2  29904  climinf  29917  stoweidlem1  29934  stoweidlem11  29944  stoweidlem12  29945  stoweidlem13  29946  stoweidlem14  29947  stoweidlem23  29956  stoweidlem24  29957  stoweidlem25  29958  stoweidlem26  29959  stoweidlem34  29967  stoweidlem40  29973  stoweidlem41  29974  stoweidlem42  29975  stoweidlem45  29978  stoweidlem60  29993  stoweidlem62  29995  wallispilem3  30000  wallispilem4  30001  wallispi  30003  wallispi2lem1  30004  stirlinglem5  30011  stirlinglem11  30017  stirlinglem12  30018  2elfz2melfz  30340  clwlkisclwwlklem2fv2  30583  clwlkisclwwlklem2a4  30584  clwlkisclwwlklem2a  30585  ltsubsubaddltsub  30605  extwwlkfablem2  30809  ply1mulgsumlem2  30987