Theorem resubcld 9421

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

Syntax hints:   -> wi 4   e. wcel 1721  (class class class)co 6040   RRcr 8945   - cmin 9247

This theorem is referenced by:  ltsubadd  9454  lesubadd  9456  lesub1  9478  lesub2  9479  ltsub1  9480  ltsub2  9481  lt2sub  9482  le2sub  9483  ltmul1a  9815  cru  9948  qbtwnre  10741  lincmb01cmp  10994  iccf1o  10995  xov1plusxeqvd  10997  intfracq  11195  fldiv  11196  modlt  11213  modsubdir  11240  serle  11333  expmulnbnd  11466  discr  11471  fzsdom2  11648  crre  11874  remullem  11888  sqrlem7  12009  absrdbnd  12100  fzomaxdiflem  12101  caubnd2  12116  amgm2  12128  mulcn2  12344  reccn2  12345  rlimo1  12365  climle  12388  climsqz  12389  climsqz2  12390  rlimle  12396  isercolllem1  12413  climsup  12418  caucvgrlem  12421  caucvgrlem2  12423  iseraltlem2  12431  iseraltlem3  12432  iseralt  12433  fsumle  12533  cvgcmp  12550  cvgcmpce  12552  eflt  12673  resinhcl  12712  tanhlt1  12716  sin01bnd  12741  sin01gt0  12746  moddvds  12814  bitscmp  12905  bitsinv1lem  12908  smueqlem  12957  pcbc  13224  4sqlem15  13282  blss2ps  18386  blss2  18387  blssps  18407  blss  18408  nm2dif  18624  nlmvscnlem2  18674  nrginvrcnlem  18679  iccntr  18805  icccmplem2  18807  metdstri  18834  cnllycmp  18934  evth  18937  lebnumii  18944  ipcnlem2  19151  cncmet  19228  minveclem3b  19282  minveclem4  19286  ivthlem2  19302  ivthlem3  19303  ovollb2lem  19337  ovoliunlem1  19351  ovolscalem1  19362  ovolicc1  19365  ovolicc2lem4  19369  ovolicc2  19371  ovolicc  19372  voliunlem2  19398  ovolioo  19415  ioorcl2  19417  uniioovol  19424  uniioombllem2  19428  uniioombllem3a  19429  uniioombllem3  19430  uniioombllem4  19431  uniioombllem6  19433  opnmbllem  19446  volcn  19451  vitalilem2  19454  ismbf3d  19499  mbfaddlem  19505  i1fadd  19540  itg1addlem4  19544  mbfi1fseqlem6  19565  itg2seq  19587  itg2split  19594  itg2cnlem2  19607  itg2cn  19608  itgrevallem1  19639  dvcjbr  19788  dvferm1lem  19821  dvferm2lem  19823  cmvth  19828  mvth  19829  dvlip  19830  dvlip2  19832  c1liplem1  19833  dvgt0  19841  dvlt0  19842  dvge0  19843  dvle  19844  dvivthlem1  19845  lhop1lem  19850  lhop  19853  dvcnvrelem1  19854  dvcnvrelem2  19855  dvcnvre  19856  dvcvx  19857  dvfsumle  19858  dvfsumge  19859  dvfsumrlimf  19862  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumlem4  19866  dvfsum2  19871  ftc1a  19874  ftc1lem4  19876  coe1mul3  19975  ply1divex  20012  plydivex  20167  aalioulem2  20203  aalioulem3  20204  aalioulem4  20205  aalioulem5  20206  aalioulem6  20207  aaliou3lem7  20219  taylthlem2  20243  mtest  20273  pilem2  20321  tangtx  20366  cosordlem  20386  efif1olem2  20398  logcnlem3  20488  logcnlem4  20489  isosctrlem2  20616  chordthmlem2  20627  chordthmlem4  20629  atanlogsublem  20708  atantan  20716  birthdaylem3  20745  logdifbnd  20785  emcllem1  20787  emcllem2  20788  emcllem5  20791  emcllem6  20792  harmonicbnd4  20802  fsumharmonic  20803  ftalem2  20809  ftalem5  20812  chpub  20957  logfaclbnd  20959  logfacbnd3  20960  logexprlim  20962  bposlem1  21021  bposlem9  21029  lgseisenlem1  21086  lgsquadlem1  21091  chtppilimlem1  21120  vmadivsum  21129  vmadivsumb  21130  rplogsumlem1  21131  rplogsumlem2  21132  rpvmasumlem  21134  dchrisumlem2  21137  dchrisum0re  21160  rplogsum  21174  mulogsumlem  21178  mulog2sumlem1  21181  vmalogdivsum2  21185  vmalogdivsum  21186  2vmadivsumlem  21187  log2sumbnd  21191  selbergb  21196  selberg2lem  21197  selberg2b  21199  chpdifbndlem1  21200  selberg3lem1  21204  selberg3lem2  21205  selberg3  21206  selberg4lem1  21207  selberg4  21208  pntrf  21210  pntrmax  21211  pntrsumo1  21212  selberg3r  21216  selberg4r  21217  selberg34r  21218  pntrlog2bndlem1  21224  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntrlog2bnd  21231  pntpbnd1a  21232  pntpbnd2  21234  pntibndlem2  21238  pntlemg  21245  pntlemn  21247  pntlemj  21250  pntlemf  21252  pntlemo  21254  pntlem3  21256  pntleml  21258  nvabs  22115  dipcj  22166  minvecolem4  22335  lt2addrd  24068  xlt2addrd  24077  fzsplit3  24103  bcm1n  24104  cnre2csqlem  24261  tpr2rico  24263  dya2ub  24573  dya2icoseg  24580  ballotlemfcc  24704  ballotlemfrcn0  24740  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamucov  24775  relgamcl  24799  subfacval3  24828  eqeelen  25747  brbtwn2  25748  colinearalg  25753  axcgrid  25759  axsegconlem1  25760  axsegconlem3  25762  axsegconlem8  25767  axsegconlem9  25768  axsegconlem10  25769  ax5seglem3a  25773  ax5seg  25781  axpaschlem  25783  axcontlem8  25814  bpoly4  26009  supaddc  26137  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  itg2addnclem  26155  itg2addnclem3  26157  itg2gt0cn  26159  ftc1cnnclem  26177  dvreasin  26179  areacirclem2  26181  areacirclem3  26182  areacirclem4  26183  areacirclem5  26185  areacirclem6  26186  areacirc  26187  cntotbnd  26395  rrnmet  26428  rrndstprj1  26429  rrndstprj2  26430  icodiamlt  26773  irrapxlem2  26776  irrapxlem3  26777  irrapxlem4  26778  irrapxlem5  26779  pellexlem2  26783  pellexlem6  26787  pell1qrgaplem  26826  rmspecfund  26862  rmspecpos  26869  jm2.24nn  26914  jm2.17c  26917  fzmaxdif  26936  acongeq  26938  modabsdifz  26946  jm3.1lem2  26979  fmul01lt1lem2  27582  climinf  27599  stoweidlem1  27617  stoweidlem11  27627  stoweidlem12  27628  stoweidlem13  27629  stoweidlem14  27630  stoweidlem23  27639  stoweidlem24  27640  stoweidlem25  27641  stoweidlem26  27642  stoweidlem34  27650  stoweidlem40  27656  stoweidlem41  27657  stoweidlem42  27658  stoweidlem45  27661  stoweidlem60  27676  stoweidlem62  27678  wallispilem3  27683  wallispilem4  27684  wallispi  27686  wallispi2lem1  27687  stirlinglem5  27694  stirlinglem11  27700  stirlinglem12  27701

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-po 4463  df-so 4464  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-riota 6508  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-pnf 9078  df-mnf 9079  df-ltxr 9081  df-sub 9249  df-neg 9250