Theorem resubcld 10922

Description: Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
renegcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
resubcld.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
resubcld	⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

Proof of Theorem resubcld

Step	Hyp	Ref	Expression
1		renegcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		resubcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		resubcl 10804	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2083  (class class class)co 7023  ℝcr 10389   − cmin 10723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-po 5369  df-so 5370  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-er 8146  df-en 8365  df-dom 8366  df-sdom 8367  df-pnf 10530  df-mnf 10531  df-ltxr 10533  df-sub 10725  df-neg 10726

This theorem is referenced by:  ltsubadd  10964  lesubadd  10966  lesub1  10988  lesub2  10989  ltsub1  10990  ltsub2  10991  lt2sub  10992  le2sub  10993  ltmul1a  11343  supaddc  11462  cru  11484  qbtwnre  12446  lincmb01cmp  12735  iccf1o  12736  xov1plusxeqvd  12738  intfracq  13081  fldiv  13082  modlt  13102  modsubdir  13162  modsumfzodifsn  13166  serle  13279  expmulnbnd  13450  discr  13455  fzsdom2  13641  cshwidxmod  14005  crre  14311  remullem  14325  sqrlem7  14446  absrdbnd  14539  fzomaxdiflem  14540  caubnd2  14555  amgm2  14567  icodiamlt  14633  bhmafibid1  14663  mulcn2  14790  reccn2  14791  rlimo1  14811  climle  14834  climsqz  14835  climsqz2  14836  rlimle  14842  isercolllem1  14859  climsup  14864  caucvgrlem  14867  caucvgrlem2  14869  iseraltlem2  14877  iseraltlem3  14878  iseralt  14879  fsumle  14991  cvgcmp  15008  cvgcmpce  15010  bpoly4  15250  eflt  15307  resinhcl  15346  tanhlt1  15350  sin01bnd  15375  sin01gt0  15380  moddvds  15455  bitscmp  15624  bitsinv1lem  15627  smueqlem  15676  modprm0  15975  pcbc  16069  4sqlem15  16128  blss2ps  22700  blss2  22701  blssps  22721  blss  22722  nm2dif  22921  nlmvscnlem2  22981  nrginvrcnlem  22987  iccntr  23116  icccmplem2  23118  metdstri  23146  cnllycmp  23247  evth  23250  lebnumii  23257  ipcnlem2  23534  cncmet  23612  rrxds  23683  rrxmval  23695  rrxmet  23698  rrxdstprj1  23699  rrxdsfi  23701  ehl1eudis  23710  ehl2eudis  23712  minveclem3b  23718  minveclem4  23722  ivthlem2  23740  ivthlem3  23741  ovollb2lem  23776  ovoliunlem1  23790  ovolscalem1  23801  ovolicc1  23804  ovolicc2lem4  23808  ovolicc2  23810  ovolicc  23811  voliunlem2  23839  ovolioo  23856  ioorcl2  23860  uniioovol  23867  uniioombllem2  23871  uniioombllem3a  23872  uniioombllem3  23873  uniioombllem4  23874  uniioombllem6  23876  opnmbllem  23889  volcn  23894  vitalilem2  23897  ismbf3d  23942  mbfaddlem  23948  i1fadd  23983  itg1addlem4  23987  mbfi1fseqlem6  24008  itg2seq  24030  itg2split  24037  itg2cnlem2  24050  itg2cn  24051  itgrevallem1  24082  dvcjbr  24233  dvferm1lem  24268  dvferm2lem  24270  cmvth  24275  mvth  24276  dvlip  24277  dvlip2  24279  c1liplem1  24280  dvgt0  24288  dvlt0  24289  dvge0  24290  dvle  24291  dvivthlem1  24292  lhop1lem  24297  lhop  24300  dvcnvrelem1  24301  dvcnvrelem2  24302  dvcnvre  24303  dvcvx  24304  dvfsumle  24305  dvfsumge  24306  dvfsumrlimf  24309  dvfsumlem2  24311  dvfsumlem3  24312  dvfsumlem4  24313  dvfsum2  24318  ftc1a  24321  ftc1lem4  24323  coe1mul3  24380  ply1divex  24417  plydivex  24573  aalioulem2  24609  aalioulem3  24610  aalioulem4  24611  aalioulem5  24612  aalioulem6  24613  aaliou3lem7  24625  taylthlem2  24649  mtest  24679  pilem2  24727  tangtx  24778  cosordlem  24800  efif1olem2  24812  logcnlem3  24912  logcnlem4  24913  isosctrlem2  25082  chordthmlem2  25096  chordthmlem4  25098  heron  25101  atanlogsublem  25178  atantan  25186  birthdaylem3  25217  logdifbnd  25257  emcllem1  25259  emcllem2  25260  emcllem5  25263  emcllem6  25264  harmonicbnd4  25274  fsumharmonic  25275  lgamgulmlem2  25293  lgamgulmlem3  25294  lgamucov  25301  relgamcl  25325  ftalem2  25337  ftalem5  25340  chpub  25482  logfaclbnd  25484  logfacbnd3  25485  logexprlim  25487  bposlem1  25546  bposlem9  25554  gausslemma2dlem1a  25627  lgseisenlem1  25637  lgsquadlem1  25642  2sqmod  25698  chtppilimlem1  25735  vmadivsum  25744  vmadivsumb  25745  rplogsumlem1  25746  rplogsumlem2  25747  rpvmasumlem  25749  dchrisumlem2  25752  dchrisum0re  25775  rplogsum  25789  mulogsumlem  25793  mulog2sumlem1  25796  vmalogdivsum2  25800  vmalogdivsum  25801  2vmadivsumlem  25802  log2sumbnd  25806  selbergb  25811  selberg2lem  25812  selberg2b  25814  chpdifbndlem1  25815  selberg3lem1  25819  selberg3lem2  25820  selberg3  25821  selberg4lem1  25822  selberg4  25823  pntrf  25825  pntrmax  25826  pntrsumo1  25827  selberg3r  25831  selberg4r  25832  selberg34r  25833  pntrlog2bndlem1  25839  pntrlog2bndlem2  25840  pntrlog2bndlem3  25841  pntrlog2bndlem4  25842  pntrlog2bndlem5  25843  pntrlog2bndlem6  25845  pntrlog2bnd  25846  pntpbnd1a  25847  pntpbnd2  25849  pntibndlem2  25853  pntlemg  25860  pntlemn  25862  pntlemj  25865  pntlemf  25867  pntlemo  25869  pntlem3  25871  pntleml  25873  ttgcontlem1  26358  eqeelen  26377  brbtwn2  26378  colinearalg  26383  axcgrid  26389  axsegconlem1  26390  axsegconlem3  26392  axsegconlem8  26397  axsegconlem9  26398  axsegconlem10  26399  ax5seglem3a  26403  ax5seg  26411  axpaschlem  26413  axcontlem8  26444  nbusgrvtxm1  26848  crctcshwlkn0lem3  27276  crctcshwlkn0lem5  27278  crctcsh  27288  clwlkclwwlklem2fv2  27460  clwlkclwwlklem2a4  27461  clwlkclwwlklem2a  27462  nvabs  28136  dipcj  28178  minvecolem4  28344  lt2addrd  30159  xlt2addrd  30166  fzsplit3  30199  bcm1n  30200  submateqlem1  30683  cnre2csqlem  30766  tpr2rico  30768  dya2ub  31141  dya2icoseg  31148  ballotlemfcc  31364  ballotlemfrcn0  31400  sgnsub  31415  signslema  31445  ftc2re  31482  subfacval3  32046  dnibndlem8  33435  dnibndlem10  33437  dnibndlem11  33438  dnibndlem12  33439  dnicn  33442  knoppcnlem4  33446  unblimceq0  33457  unbdqndv2lem2  33460  knoppndvlem11  33472  knoppndvlem14  33475  knoppndvlem15  33476  knoppndvlem17  33478  knoppndvlem20  33481  poimirlem29  34473  broucube  34478  opnmbllem0  34480  mblfinlem3  34483  mblfinlem4  34484  itg2addnclem  34495  itg2addnclem3  34497  itg2gt0cn  34499  ftc1cnnclem  34517  areacirclem1  34534  areacirclem2  34535  areacirclem4  34537  areacirclem5  34538  areacirc  34539  cntotbnd  34627  rrnmet  34660  rrndstprj1  34661  rrndstprj2  34662  frlmvscadiccat  38693  fltnlta  38793  irrapxlem2  38926  irrapxlem3  38927  irrapxlem4  38928  irrapxlem5  38929  pellexlem2  38933  pellexlem6  38937  pell1qrgaplem  38976  rmspecsqrtnq  39009  rmspecfund  39012  rmspecpos  39019  jm2.24nn  39062  jm2.17c  39065  fzmaxdif  39084  acongeq  39086  modabsdifz  39089  jm3.1lem2  39121  areaquad  39329  imo72b2lem0  40022  cvgdvgrat  40204  hashnzfzclim  40213  binomcxplemdvbinom  40244  oddfl  41105  lefldiveq  41121  fperiodmul  41133  fzdifsuc2  41139  suprltrp  41158  supxrgere  41163  supxrgelem  41167  suplesup  41169  infleinflem2  41201  infleinf  41202  xrralrecnnge  41224  iccshift  41357  iooshift  41361  iooiinicc  41381  fmul01lt1lem2  41429  climinf  41450  sumnnodd  41474  ltmod  41482  lptre2pt  41484  climleltrp  41520  limsupgtlem  41621  liminflimsupclim  41651  fperdvper  41766  dvbdfbdioolem1  41776  dvbdfbdioolem2  41777  dvbdfbdioo  41778  ioodvbdlimc1lem1  41779  ioodvbdlimc1lem2  41780  ioodvbdlimc2lem  41782  dvnmul  41791  iblspltprt  41821  itgspltprt  41827  itgiccshift  41828  itgperiod  41829  itgsbtaddcnst  41830  sublevolico  41833  stoweidlem1  41850  stoweidlem11  41860  stoweidlem12  41861  stoweidlem13  41862  stoweidlem14  41863  stoweidlem23  41872  stoweidlem24  41873  stoweidlem25  41874  stoweidlem26  41875  stoweidlem34  41883  stoweidlem40  41889  stoweidlem41  41890  stoweidlem42  41891  stoweidlem45  41894  stoweidlem60  41909  stoweidlem62  41911  wallispilem3  41916  wallispilem4  41917  wallispi  41919  wallispi2lem1  41920  stirlinglem5  41927  stirlinglem11  41933  stirlinglem12  41934  dirkercncflem1  41952  fourierdlem4  41960  fourierdlem6  41962  fourierdlem7  41963  fourierdlem9  41965  fourierdlem13  41969  fourierdlem14  41970  fourierdlem15  41971  fourierdlem19  41975  fourierdlem26  41982  fourierdlem35  41991  fourierdlem39  41995  fourierdlem40  41996  fourierdlem41  41997  fourierdlem42  41998  fourierdlem48  42003  fourierdlem49  42004  fourierdlem50  42005  fourierdlem51  42006  fourierdlem56  42011  fourierdlem57  42012  fourierdlem59  42014  fourierdlem60  42015  fourierdlem61  42016  fourierdlem63  42018  fourierdlem64  42019  fourierdlem65  42020  fourierdlem66  42021  fourierdlem68  42023  fourierdlem71  42026  fourierdlem72  42027  fourierdlem73  42028  fourierdlem74  42029  fourierdlem75  42030  fourierdlem76  42031  fourierdlem78  42033  fourierdlem79  42034  fourierdlem81  42036  fourierdlem82  42037  fourierdlem83  42038  fourierdlem84  42039  fourierdlem88  42043  fourierdlem89  42044  fourierdlem90  42045  fourierdlem91  42046  fourierdlem92  42047  fourierdlem93  42048  fourierdlem95  42050  fourierdlem97  42052  fourierdlem101  42056  fourierdlem103  42058  fourierdlem104  42059  fourierdlem107  42062  fourierdlem109  42064  fourierdlem111  42066  fouriersw  42080  elaa2lem  42082  etransclem23  42106  rrxtopnfi  42136  rrndistlt  42139  ioorrnopnlem  42153  ioorrnopnxrlem  42155  sge0gtfsumgt  42289  iundjiun  42306  volicorecl  42392  hoiprodcl  42393  hoiprodcl3  42426  volicore  42427  hoidmvcl  42428  hoidmv1lelem2  42438  hoidmv1lelem3  42439  hoidmv1le  42440  hoidmvlelem1  42441  hoidmvlelem2  42442  hoiqssbllem1  42468  hoiqssbllem2  42469  hoiqssbllem3  42470  hspmbllem1  42472  ovolval5lem1  42498  ovolval5lem2  42499  iunhoiioolem  42521  iccvonmbllem  42524  vonicclem1  42529  preimageiingt  42562  salpreimagtge  42566  smfaddlem1  42603  smflimlem4  42614  smfmullem1  42630  smfmullem2  42631  smfmullem3  42632  ltsubsubaddltsub  43039  2elfz2melfz  43056  requad01  43290  requad1  43291  requad2  43292  bgoldbtbndlem2  43475  bgoldbtbndlem3  43476  bgoldbtbndlem4  43477  bgoldbtbnd  43478  ply1mulgsumlem2  43943  difmodm1lt  44085  nnpw2pmod  44146  dignn0flhalflem1  44178  affinecomb1  44192  rrxlinesc  44225  rrxlinec  44226  eenglngeehlnmlem1  44227  eenglngeehlnmlem2  44228  rrx2vlinest  44231  rrx2linest2  44234  2sphere  44239  line2  44242  itsclc0lem2  44247  itsclc0lem3  44248  itscnhlc0yqe  44249  itsclc0yqsollem2  44253  itsclc0yqsol  44254  itscnhlc0xyqsol  44255  itsclinecirc0  44263  itsclinecirc0b  44264  itsclinecirc0in  44265  itsclquadb  44266  2itscp  44271  itscnhlinecirc02plem1  44272  itscnhlinecirc02p  44275  inlinecirc02plem  44276  amgmwlem  44405