Theorem resubcld 9768

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 9665	. 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 1756  (class class class)co 6086   RRcr 9273   - cmin 9587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-po 4636  df-so 4637  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-ltxr 9415  df-sub 9589  df-neg 9590

This theorem is referenced by:  ltsubadd  9801  lesubadd  9803  lesub1  9825  lesub2  9826  ltsub1  9827  ltsub2  9828  lt2sub  9829  le2sub  9830  ltmul1a  10170  cru  10306  qbtwnre  11161  lincmb01cmp  11420  iccf1o  11421  xov1plusxeqvd  11423  intfracq  11690  fldiv  11691  modlt  11710  modsubdir  11759  serle  11853  expmulnbnd  11988  discr  11993  fzsdom2  12181  cshwidxmod  12432  crre  12595  remullem  12609  sqrlem7  12730  absrdbnd  12821  fzomaxdiflem  12822  caubnd2  12837  amgm2  12849  mulcn2  13065  reccn2  13066  rlimo1  13086  climle  13109  climsqz  13110  climsqz2  13111  rlimle  13117  isercolllem1  13134  climsup  13139  caucvgrlem  13142  caucvgrlem2  13144  iseraltlem2  13152  iseraltlem3  13153  iseralt  13154  fsumle  13254  cvgcmp  13271  cvgcmpce  13273  eflt  13393  resinhcl  13432  tanhlt1  13436  sin01bnd  13461  sin01gt0  13466  moddvds  13534  bitscmp  13626  bitsinv1lem  13629  smueqlem  13678  modprm0  13865  pcbc  13954  4sqlem15  14012  blss2ps  19958  blss2  19959  blssps  19979  blss  19980  nm2dif  20196  nlmvscnlem2  20246  nrginvrcnlem  20251  iccntr  20378  icccmplem2  20380  metdstri  20407  cnllycmp  20508  evth  20511  lebnumii  20518  ipcnlem2  20736  cncmet  20813  rrxds  20877  rrxmval  20884  rrxmet  20887  rrxdstprj1  20888  minveclem3b  20895  minveclem4  20899  ivthlem2  20916  ivthlem3  20917  ovollb2lem  20951  ovoliunlem1  20965  ovolscalem1  20976  ovolicc1  20979  ovolicc2lem4  20983  ovolicc2  20985  ovolicc  20986  voliunlem2  21012  ovolioo  21029  ioorcl2  21032  uniioovol  21039  uniioombllem2  21043  uniioombllem3a  21044  uniioombllem3  21045  uniioombllem4  21046  uniioombllem6  21048  opnmbllem  21061  volcn  21066  vitalilem2  21069  ismbf3d  21112  mbfaddlem  21118  i1fadd  21153  itg1addlem4  21157  mbfi1fseqlem6  21178  itg2seq  21200  itg2split  21207  itg2cnlem2  21220  itg2cn  21221  itgrevallem1  21252  dvcjbr  21403  dvferm1lem  21436  dvferm2lem  21438  cmvth  21443  mvth  21444  dvlip  21445  dvlip2  21447  c1liplem1  21448  dvgt0  21456  dvlt0  21457  dvge0  21458  dvle  21459  dvivthlem1  21460  lhop1lem  21465  lhop  21468  dvcnvrelem1  21469  dvcnvrelem2  21470  dvcnvre  21471  dvcvx  21472  dvfsumle  21473  dvfsumge  21474  dvfsumrlimf  21477  dvfsumlem2  21479  dvfsumlem3  21480  dvfsumlem4  21481  dvfsum2  21486  ftc1a  21489  ftc1lem4  21491  coe1mul3  21551  ply1divex  21588  plydivex  21743  aalioulem2  21779  aalioulem3  21780  aalioulem4  21781  aalioulem5  21782  aalioulem6  21783  aaliou3lem7  21795  taylthlem2  21819  mtest  21849  pilem2  21897  tangtx  21947  cosordlem  21967  efif1olem2  21979  logcnlem3  22069  logcnlem4  22070  isosctrlem2  22197  chordthmlem2  22208  chordthmlem4  22210  heron  22213  atanlogsublem  22290  atantan  22298  birthdaylem3  22327  logdifbnd  22367  emcllem1  22369  emcllem2  22370  emcllem5  22373  emcllem6  22374  harmonicbnd4  22384  fsumharmonic  22385  ftalem2  22391  ftalem5  22394  chpub  22539  logfaclbnd  22541  logfacbnd3  22542  logexprlim  22544  bposlem1  22603  bposlem9  22611  lgseisenlem1  22668  lgsquadlem1  22673  chtppilimlem1  22702  vmadivsum  22711  vmadivsumb  22712  rplogsumlem1  22713  rplogsumlem2  22714  rpvmasumlem  22716  dchrisumlem2  22719  dchrisum0re  22742  rplogsum  22756  mulogsumlem  22760  mulog2sumlem1  22763  vmalogdivsum2  22767  vmalogdivsum  22768  2vmadivsumlem  22769  log2sumbnd  22773  selbergb  22778  selberg2lem  22779  selberg2b  22781  chpdifbndlem1  22782  selberg3lem1  22786  selberg3lem2  22787  selberg3  22788  selberg4lem1  22789  selberg4  22790  pntrf  22792  pntrmax  22793  pntrsumo1  22794  selberg3r  22798  selberg4r  22799  selberg34r  22800  pntrlog2bndlem1  22806  pntrlog2bndlem2  22807  pntrlog2bndlem3  22808  pntrlog2bndlem4  22809  pntrlog2bndlem5  22810  pntrlog2bndlem6  22812  pntrlog2bnd  22813  pntpbnd1a  22814  pntpbnd2  22816  pntibndlem2  22820  pntlemg  22827  pntlemn  22829  pntlemj  22832  pntlemf  22834  pntlemo  22836  pntlem3  22838  pntleml  22840  ttgcontlem1  23099  eqeelen  23118  brbtwn2  23119  colinearalg  23124  axcgrid  23130  axsegconlem1  23131  axsegconlem3  23133  axsegconlem8  23138  axsegconlem9  23139  axsegconlem10  23140  ax5seglem3a  23144  ax5seg  23152  axpaschlem  23154  axcontlem8  23185  nvabs  24029  dipcj  24080  minvecolem4  24249  lt2addrd  26004  xlt2addrd  26019  fzsplit3  26046  bcm1n  26047  cnre2csqlem  26309  tpr2rico  26311  dya2ub  26654  dya2icoseg  26661  ballotlemfcc  26845  ballotlemfrcn0  26881  sgnsub  26896  signslema  26932  lgamgulmlem2  26985  lgamgulmlem3  26986  lgamucov  26993  relgamcl  27017  subfacval3  27046  bpoly4  28171  supaddc  28388  opnmbllem0  28398  mblfinlem3  28401  mblfinlem4  28402  itg2addnclem  28414  itg2addnclem3  28416  itg2gt0cn  28418  ftc1cnnclem  28436  areacirclem1  28455  areacirclem2  28456  areacirclem4  28458  areacirclem5  28459  areacirc  28460  cntotbnd  28666  rrnmet  28699  rrndstprj1  28700  rrndstprj2  28701  icodiamlt  29132  irrapxlem2  29135  irrapxlem3  29136  irrapxlem4  29137  irrapxlem5  29138  pellexlem2  29142  pellexlem6  29146  pell1qrgaplem  29185  rmspecfund  29221  rmspecpos  29228  jm2.24nn  29273  jm2.17c  29276  fzmaxdif  29295  acongeq  29297  modabsdifz  29305  jm3.1lem2  29338  areaquad  29563  fmul01lt1lem2  29737  climinf  29750  stoweidlem1  29767  stoweidlem11  29777  stoweidlem12  29778  stoweidlem13  29779  stoweidlem14  29780  stoweidlem23  29789  stoweidlem24  29790  stoweidlem25  29791  stoweidlem26  29792  stoweidlem34  29800  stoweidlem40  29806  stoweidlem41  29807  stoweidlem42  29808  stoweidlem45  29811  stoweidlem60  29826  stoweidlem62  29828  wallispilem3  29833  wallispilem4  29834  wallispi  29836  wallispi2lem1  29837  stirlinglem5  29844  stirlinglem11  29850  stirlinglem12  29851  2elfz2melfz  30173  clwlkisclwwlklem2fv2  30416  clwlkisclwwlklem2a4  30417  clwlkisclwwlklem2a  30418  ltsubsubaddltsub  30438  extwwlkfablem2  30642