Theorem resubcld 11688

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 11570	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2105  (class class class)co 7430  ℝcr 11151   − cmin 11489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297  df-sub 11491  df-neg 11492

This theorem is referenced by:  ltsubadd  11730  lesubadd  11732  lesub1  11754  lesub2  11755  ltsub1  11756  ltsub2  11757  lt2sub  11758  le2sub  11759  ltmul1a  12113  supaddc  12232  cru  12255  ge2halflem1  13147  qbtwnre  13237  lincmb01cmp  13531  iccf1o  13532  xov1plusxeqvd  13534  intfracq  13895  fldiv  13896  modlt  13916  modsubdir  13977  modsumfzodifsn  13981  serle  14094  expmulnbnd  14270  discr  14275  fzsdom2  14463  cshwidxmod  14837  crre  15149  remullem  15163  01sqrexlem7  15283  absrdbnd  15376  fzomaxdiflem  15377  caubnd2  15392  amgm2  15404  icodiamlt  15470  bhmafibid1  15500  mulcn2  15628  reccn2  15629  rlimo1  15649  climle  15672  climsqz  15673  climsqz2  15674  rlimle  15680  isercolllem1  15697  climsup  15702  caucvgrlem  15705  caucvgrlem2  15707  iseraltlem2  15715  iseraltlem3  15716  iseralt  15717  fsumle  15831  cvgcmp  15848  cvgcmpce  15850  bpoly4  16091  eflt  16149  resinhcl  16188  tanhlt1  16192  sin01bnd  16217  sin01gt0  16222  moddvds  16297  bitscmp  16471  bitsinv1lem  16474  smueqlem  16523  modprm0  16838  pcbc  16933  4sqlem15  16992  blss2ps  24428  blss2  24429  blssps  24449  blss  24450  nm2dif  24653  nlmvscnlem2  24721  nrginvrcnlem  24727  iccntr  24856  icccmplem2  24858  metdstri  24886  cnllycmp  25001  evth  25004  lebnumii  25011  ipcnlem2  25291  cncmet  25369  rrxds  25440  rrxmval  25452  rrxmet  25455  rrxdstprj1  25456  rrxdsfi  25458  ehl1eudis  25467  ehl2eudis  25469  minveclem3b  25475  minveclem4  25479  ivthlem2  25500  ivthlem3  25501  ovollb2lem  25536  ovoliunlem1  25550  ovolscalem1  25561  ovolicc1  25564  ovolicc2lem4  25568  ovolicc2  25570  ovolicc  25571  voliunlem2  25599  ovolioo  25616  ioorcl2  25620  uniioovol  25627  uniioombllem2  25631  uniioombllem3a  25632  uniioombllem3  25633  uniioombllem4  25634  uniioombllem6  25636  opnmbllem  25649  volcn  25654  vitalilem2  25657  ismbf3d  25702  mbfaddlem  25708  i1fadd  25743  itg1addlem4  25747  itg1addlem4OLD  25748  mbfi1fseqlem6  25769  itg2seq  25791  itg2split  25798  itg2cnlem2  25811  itg2cn  25812  itgrevallem1  25844  dvcjbr  26001  dvferm1lem  26036  dvferm2lem  26038  cmvth  26043  cmvthOLD  26044  mvth  26045  dvlip  26046  dvlip2  26048  c1liplem1  26049  dvgt0  26057  dvlt0  26058  dvge0  26059  dvle  26060  dvivthlem1  26061  lhop1lem  26066  lhop  26069  dvcnvrelem1  26070  dvcnvrelem2  26071  dvcnvre  26072  dvcvx  26073  dvfsumle  26074  dvfsumleOLD  26075  dvfsumge  26076  dvfsumrlimf  26079  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumlem4  26084  dvfsum2  26089  ftc1a  26092  ftc1lem4  26094  coe1mul3  26152  ply1divex  26190  plydivex  26353  aalioulem2  26389  aalioulem3  26390  aalioulem4  26391  aalioulem5  26392  aalioulem6  26393  aaliou3lem7  26405  taylthlem2  26430  taylthlem2OLD  26431  mtest  26461  pilem2  26510  tangtx  26561  cosordlem  26586  efif1olem2  26599  logcnlem3  26700  logcnlem4  26701  isosctrlem2  26876  chordthmlem2  26890  chordthmlem4  26892  heron  26895  atanlogsublem  26972  atantan  26980  birthdaylem3  27010  logdifbnd  27051  emcllem1  27053  emcllem2  27054  emcllem5  27057  emcllem6  27058  harmonicbnd4  27068  fsumharmonic  27069  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamucov  27095  relgamcl  27119  ftalem2  27131  ftalem5  27134  chpub  27278  logfaclbnd  27280  logfacbnd3  27281  logexprlim  27283  bposlem1  27342  bposlem9  27350  gausslemma2dlem1a  27423  lgseisenlem1  27433  lgsquadlem1  27438  2sqmod  27494  chtppilimlem1  27531  vmadivsum  27540  vmadivsumb  27541  rplogsumlem1  27542  rplogsumlem2  27543  rpvmasumlem  27545  dchrisumlem2  27548  dchrisum0re  27571  rplogsum  27585  mulogsumlem  27589  mulog2sumlem1  27592  vmalogdivsum2  27596  vmalogdivsum  27597  2vmadivsumlem  27598  log2sumbnd  27602  selbergb  27607  selberg2lem  27608  selberg2b  27610  chpdifbndlem1  27611  selberg3lem1  27615  selberg3lem2  27616  selberg3  27617  selberg4lem1  27618  selberg4  27619  pntrf  27621  pntrmax  27622  pntrsumo1  27623  selberg3r  27627  selberg4r  27628  selberg34r  27629  pntrlog2bndlem1  27635  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntrlog2bnd  27642  pntpbnd1a  27643  pntpbnd2  27645  pntibndlem2  27649  pntlemg  27656  pntlemn  27658  pntlemj  27661  pntlemf  27663  pntlemo  27665  pntlem3  27667  pntleml  27669  ttgcontlem1  28913  eqeelen  28933  brbtwn2  28934  colinearalg  28939  axcgrid  28945  axsegconlem1  28946  axsegconlem3  28948  axsegconlem8  28953  axsegconlem9  28954  axsegconlem10  28955  ax5seglem3a  28959  ax5seg  28967  axpaschlem  28969  axcontlem8  29000  nbusgrvtxm1  29410  crctcshwlkn0lem3  29841  crctcshwlkn0lem5  29843  crctcsh  29853  clwlkclwwlklem2fv2  30024  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  nvabs  30700  dipcj  30742  minvecolem4  30908  lt2addrd  32761  xlt2addrd  32768  fzsplit3  32801  bcm1n  32802  ply1degltel  33594  ply1degltlss  33596  submateqlem1  33767  cnre2csqlem  33870  tpr2rico  33872  dya2ub  34251  dya2icoseg  34258  ballotlemfcc  34474  ballotlemfrcn0  34510  sgnsub  34525  signslema  34555  ftc2re  34591  subfacval3  35173  dnibndlem8  36467  dnibndlem10  36469  dnibndlem11  36470  dnibndlem12  36471  dnicn  36474  knoppcnlem4  36478  unblimceq0  36489  unbdqndv2lem2  36492  knoppndvlem11  36504  knoppndvlem14  36507  knoppndvlem15  36508  knoppndvlem17  36510  knoppndvlem20  36513  irrdifflemf  37307  poimirlem29  37635  broucube  37640  opnmbllem0  37642  mblfinlem3  37645  mblfinlem4  37646  itg2addnclem  37657  itg2addnclem3  37659  itg2gt0cn  37661  ftc1cnnclem  37677  areacirclem1  37694  areacirclem2  37695  areacirclem4  37697  areacirclem5  37698  areacirc  37699  cntotbnd  37782  rrnmet  37815  rrndstprj1  37816  rrndstprj2  37817  lcmineqlem23  42032  intlewftc  42042  aks4d1p1p2  42051  aks4d1p1p4  42052  dvle2  42053  aks4d1p1  42057  primrootlekpowne0  42086  hashscontpow1  42102  aks6d1c2  42111  aks6d1c5lem2  42119  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem3  42153  bcled  42159  bcle2d  42160  unitscyglem2  42177  unitscyglem4  42179  metakunt1  42186  metakunt7  42192  metakunt16  42201  metakunt18  42203  metakunt28  42213  metakunt29  42214  metakunt30  42215  readdrcl2d  42286  frlmvscadiccat  42492  fltnlta  42649  3cubeslem2  42672  3cubeslem4  42676  irrapxlem2  42810  irrapxlem3  42811  irrapxlem4  42812  irrapxlem5  42813  pellexlem2  42817  pellexlem6  42821  pell1qrgaplem  42860  rmspecsqrtnq  42893  rmspecfund  42896  rmspecpos  42904  jm2.24nn  42947  jm2.17c  42950  fzmaxdif  42969  acongeq  42971  modabsdifz  42974  jm3.1lem2  43006  areaquad  43204  sqrtcvallem2  43626  sqrtcvallem3  43627  sqrtcval  43630  imo72b2lem0  44154  cvgdvgrat  44308  hashnzfzclim  44317  binomcxplemdvbinom  44348  oddfl  45227  lefldiveq  45242  fperiodmul  45254  fzdifsuc2  45260  suprltrp  45277  supxrgere  45282  supxrgelem  45286  suplesup  45288  infleinflem2  45320  infleinf  45321  xrralrecnnge  45339  iccshift  45470  iooshift  45474  iooiinicc  45494  fmul01lt1lem2  45540  climinf  45561  sumnnodd  45585  ltmod  45593  lptre2pt  45595  climleltrp  45631  limsupgtlem  45732  liminflimsupclim  45762  fperdvper  45874  dvbdfbdioolem1  45883  dvbdfbdioolem2  45884  dvbdfbdioo  45885  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnmul  45898  iblspltprt  45928  itgspltprt  45934  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  sublevolico  45939  stoweidlem1  45956  stoweidlem11  45966  stoweidlem12  45967  stoweidlem13  45968  stoweidlem14  45969  stoweidlem23  45978  stoweidlem24  45979  stoweidlem25  45980  stoweidlem26  45981  stoweidlem34  45989  stoweidlem40  45995  stoweidlem41  45996  stoweidlem42  45997  stoweidlem45  46000  stoweidlem60  46015  stoweidlem62  46017  wallispilem3  46022  wallispilem4  46023  wallispi  46025  wallispi2lem1  46026  stirlinglem5  46033  stirlinglem11  46039  stirlinglem12  46040  dirkercncflem1  46058  fourierdlem4  46066  fourierdlem6  46068  fourierdlem7  46069  fourierdlem9  46071  fourierdlem13  46075  fourierdlem14  46076  fourierdlem15  46077  fourierdlem19  46081  fourierdlem26  46088  fourierdlem35  46097  fourierdlem39  46101  fourierdlem40  46102  fourierdlem41  46103  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem51  46112  fourierdlem56  46117  fourierdlem57  46118  fourierdlem59  46120  fourierdlem60  46121  fourierdlem61  46122  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem66  46127  fourierdlem68  46129  fourierdlem71  46132  fourierdlem72  46133  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem78  46139  fourierdlem79  46140  fourierdlem81  46142  fourierdlem82  46143  fourierdlem83  46144  fourierdlem84  46145  fourierdlem88  46149  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem92  46153  fourierdlem93  46154  fourierdlem95  46156  fourierdlem97  46158  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem107  46168  fourierdlem109  46170  fourierdlem111  46172  fouriersw  46186  elaa2lem  46188  etransclem23  46212  rrxtopnfi  46242  rrndistlt  46245  ioorrnopnlem  46259  ioorrnopnxrlem  46261  sge0gtfsumgt  46398  iundjiun  46415  volicorecl  46501  hoiprodcl  46502  hoiprodcl3  46535  volicore  46536  hoidmvcl  46537  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem2  46551  hoiqssbllem1  46577  hoiqssbllem2  46578  hoiqssbllem3  46579  hspmbllem1  46581  ovolval5lem1  46607  ovolval5lem2  46608  iunhoiioolem  46630  iccvonmbllem  46633  vonicclem1  46638  preimageiingt  46675  salpreimagtge  46680  smfaddlem1  46718  smflimlem4  46729  smfmullem1  46746  smfmullem2  46747  smfmullem3  46748  ltsubsubaddltsub  47250  2elfz2melfz  47267  requad01  47545  requad1  47546  requad2  47547  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbndlem4  47732  bgoldbtbnd  47733  2tceilhalfelfzo1  47952  gpgedgvtx0  47953  gpgedgvtx1  47954  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx13starlem2  47962  ply1mulgsumlem2  48232  difmodm1lt  48371  nnpw2pmod  48432  dignn0flhalflem1  48464  affinecomb1  48551  rrxlinesc  48584  rrxlinec  48585  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  rrx2vlinest  48590  rrx2linest2  48593  2sphere  48598  line2  48601  itsclc0lem2  48606  itsclc0lem3  48607  itscnhlc0yqe  48608  itsclc0yqsollem2  48612  itsclc0yqsol  48613  itscnhlc0xyqsol  48614  itsclinecirc0  48622  itsclinecirc0b  48623  itsclinecirc0in  48624  itsclquadb  48625  2itscp  48630  itscnhlinecirc02plem1  48631  itscnhlinecirc02p  48634  inlinecirc02plem  48635  amgmwlem  49032