Theorem resubcld 11642

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7409  ℝcr 11109   − cmin 11444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-ltxr 11253  df-sub 11446  df-neg 11447

This theorem is referenced by:  ltsubadd  11684  lesubadd  11686  lesub1  11708  lesub2  11709  ltsub1  11710  ltsub2  11711  lt2sub  11712  le2sub  11713  ltmul1a  12063  supaddc  12181  cru  12204  qbtwnre  13178  lincmb01cmp  13472  iccf1o  13473  xov1plusxeqvd  13475  intfracq  13824  fldiv  13825  modlt  13845  modsubdir  13905  modsumfzodifsn  13909  serle  14023  expmulnbnd  14198  discr  14203  fzsdom2  14388  cshwidxmod  14753  crre  15061  remullem  15075  01sqrexlem7  15195  absrdbnd  15288  fzomaxdiflem  15289  caubnd2  15304  amgm2  15316  icodiamlt  15382  bhmafibid1  15412  mulcn2  15540  reccn2  15541  rlimo1  15561  climle  15584  climsqz  15585  climsqz2  15586  rlimle  15594  isercolllem1  15611  climsup  15616  caucvgrlem  15619  caucvgrlem2  15621  iseraltlem2  15629  iseraltlem3  15630  iseralt  15631  fsumle  15745  cvgcmp  15762  cvgcmpce  15764  bpoly4  16003  eflt  16060  resinhcl  16099  tanhlt1  16103  sin01bnd  16128  sin01gt0  16133  moddvds  16208  bitscmp  16379  bitsinv1lem  16382  smueqlem  16431  modprm0  16738  pcbc  16833  4sqlem15  16892  blss2ps  23909  blss2  23910  blssps  23930  blss  23931  nm2dif  24134  nlmvscnlem2  24202  nrginvrcnlem  24208  iccntr  24337  icccmplem2  24339  metdstri  24367  cnllycmp  24472  evth  24475  lebnumii  24482  ipcnlem2  24761  cncmet  24839  rrxds  24910  rrxmval  24922  rrxmet  24925  rrxdstprj1  24926  rrxdsfi  24928  ehl1eudis  24937  ehl2eudis  24939  minveclem3b  24945  minveclem4  24949  ivthlem2  24969  ivthlem3  24970  ovollb2lem  25005  ovoliunlem1  25019  ovolscalem1  25030  ovolicc1  25033  ovolicc2lem4  25037  ovolicc2  25039  ovolicc  25040  voliunlem2  25068  ovolioo  25085  ioorcl2  25089  uniioovol  25096  uniioombllem2  25100  uniioombllem3a  25101  uniioombllem3  25102  uniioombllem4  25103  uniioombllem6  25105  opnmbllem  25118  volcn  25123  vitalilem2  25126  ismbf3d  25171  mbfaddlem  25177  i1fadd  25212  itg1addlem4  25216  itg1addlem4OLD  25217  mbfi1fseqlem6  25238  itg2seq  25260  itg2split  25267  itg2cnlem2  25280  itg2cn  25281  itgrevallem1  25312  dvcjbr  25466  dvferm1lem  25501  dvferm2lem  25503  cmvth  25508  mvth  25509  dvlip  25510  dvlip2  25512  c1liplem1  25513  dvgt0  25521  dvlt0  25522  dvge0  25523  dvle  25524  dvivthlem1  25525  lhop1lem  25530  lhop  25533  dvcnvrelem1  25534  dvcnvrelem2  25535  dvcnvre  25536  dvcvx  25537  dvfsumle  25538  dvfsumge  25539  dvfsumrlimf  25542  dvfsumlem2  25544  dvfsumlem3  25545  dvfsumlem4  25546  dvfsum2  25551  ftc1a  25554  ftc1lem4  25556  coe1mul3  25617  ply1divex  25654  plydivex  25810  aalioulem2  25846  aalioulem3  25847  aalioulem4  25848  aalioulem5  25849  aalioulem6  25850  aaliou3lem7  25862  taylthlem2  25886  mtest  25916  pilem2  25964  tangtx  26015  cosordlem  26039  efif1olem2  26052  logcnlem3  26152  logcnlem4  26153  isosctrlem2  26324  chordthmlem2  26338  chordthmlem4  26340  heron  26343  atanlogsublem  26420  atantan  26428  birthdaylem3  26458  logdifbnd  26498  emcllem1  26500  emcllem2  26501  emcllem5  26504  emcllem6  26505  harmonicbnd4  26515  fsumharmonic  26516  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamucov  26542  relgamcl  26566  ftalem2  26578  ftalem5  26581  chpub  26723  logfaclbnd  26725  logfacbnd3  26726  logexprlim  26728  bposlem1  26787  bposlem9  26795  gausslemma2dlem1a  26868  lgseisenlem1  26878  lgsquadlem1  26883  2sqmod  26939  chtppilimlem1  26976  vmadivsum  26985  vmadivsumb  26986  rplogsumlem1  26987  rplogsumlem2  26988  rpvmasumlem  26990  dchrisumlem2  26993  dchrisum0re  27016  rplogsum  27030  mulogsumlem  27034  mulog2sumlem1  27037  vmalogdivsum2  27041  vmalogdivsum  27042  2vmadivsumlem  27043  log2sumbnd  27047  selbergb  27052  selberg2lem  27053  selberg2b  27055  chpdifbndlem1  27056  selberg3lem1  27060  selberg3lem2  27061  selberg3  27062  selberg4lem1  27063  selberg4  27064  pntrf  27066  pntrmax  27067  pntrsumo1  27068  selberg3r  27072  selberg4r  27073  selberg34r  27074  pntrlog2bndlem1  27080  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntrlog2bndlem6  27086  pntrlog2bnd  27087  pntpbnd1a  27088  pntpbnd2  27090  pntibndlem2  27094  pntlemg  27101  pntlemn  27103  pntlemj  27106  pntlemf  27108  pntlemo  27110  pntlem3  27112  pntleml  27114  ttgcontlem1  28142  eqeelen  28162  brbtwn2  28163  colinearalg  28168  axcgrid  28174  axsegconlem1  28175  axsegconlem3  28177  axsegconlem8  28182  axsegconlem9  28183  axsegconlem10  28184  ax5seglem3a  28188  ax5seg  28196  axpaschlem  28198  axcontlem8  28229  nbusgrvtxm1  28636  crctcshwlkn0lem3  29066  crctcshwlkn0lem5  29068  crctcsh  29078  clwlkclwwlklem2fv2  29249  clwlkclwwlklem2a4  29250  clwlkclwwlklem2a  29251  nvabs  29925  dipcj  29967  minvecolem4  30133  lt2addrd  31964  xlt2addrd  31971  fzsplit3  32005  bcm1n  32006  ply1degltel  32666  ply1degltlss  32667  submateqlem1  32787  cnre2csqlem  32890  tpr2rico  32892  dya2ub  33269  dya2icoseg  33276  ballotlemfcc  33492  ballotlemfrcn0  33528  sgnsub  33543  signslema  33573  ftc2re  33610  subfacval3  34180  gg-cmvth  35181  gg-dvfsumle  35182  gg-dvfsumlem2  35183  dnibndlem8  35361  dnibndlem10  35363  dnibndlem11  35364  dnibndlem12  35365  dnicn  35368  knoppcnlem4  35372  unblimceq0  35383  unbdqndv2lem2  35386  knoppndvlem11  35398  knoppndvlem14  35401  knoppndvlem15  35402  knoppndvlem17  35404  knoppndvlem20  35407  irrdifflemf  36206  poimirlem29  36517  broucube  36522  opnmbllem0  36524  mblfinlem3  36527  mblfinlem4  36528  itg2addnclem  36539  itg2addnclem3  36541  itg2gt0cn  36543  ftc1cnnclem  36559  areacirclem1  36576  areacirclem2  36577  areacirclem4  36579  areacirclem5  36580  areacirc  36581  cntotbnd  36664  rrnmet  36697  rrndstprj1  36698  rrndstprj2  36699  lcmineqlem23  40916  intlewftc  40926  aks4d1p1p2  40935  aks4d1p1p4  40936  dvle2  40937  aks4d1p1  40941  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  metakunt1  40985  metakunt7  40991  metakunt16  41000  metakunt18  41002  metakunt28  41012  metakunt29  41013  metakunt30  41014  frlmvscadiccat  41080  fltnlta  41405  3cubeslem2  41423  3cubeslem4  41427  irrapxlem2  41561  irrapxlem3  41562  irrapxlem4  41563  irrapxlem5  41564  pellexlem2  41568  pellexlem6  41572  pell1qrgaplem  41611  rmspecsqrtnq  41644  rmspecfund  41647  rmspecpos  41655  jm2.24nn  41698  jm2.17c  41701  fzmaxdif  41720  acongeq  41722  modabsdifz  41725  jm3.1lem2  41757  areaquad  41965  sqrtcvallem2  42388  sqrtcvallem3  42389  sqrtcval  42392  imo72b2lem0  42917  cvgdvgrat  43072  hashnzfzclim  43081  binomcxplemdvbinom  43112  oddfl  43987  lefldiveq  44002  fperiodmul  44014  fzdifsuc2  44020  suprltrp  44038  supxrgere  44043  supxrgelem  44047  suplesup  44049  infleinflem2  44081  infleinf  44082  xrralrecnnge  44100  iccshift  44231  iooshift  44235  iooiinicc  44255  fmul01lt1lem2  44301  climinf  44322  sumnnodd  44346  ltmod  44354  lptre2pt  44356  climleltrp  44392  limsupgtlem  44493  liminflimsupclim  44523  fperdvper  44635  dvbdfbdioolem1  44644  dvbdfbdioolem2  44645  dvbdfbdioo  44646  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnmul  44659  iblspltprt  44689  itgspltprt  44695  itgiccshift  44696  itgperiod  44697  itgsbtaddcnst  44698  sublevolico  44700  stoweidlem1  44717  stoweidlem11  44727  stoweidlem12  44728  stoweidlem13  44729  stoweidlem14  44730  stoweidlem23  44739  stoweidlem24  44740  stoweidlem25  44741  stoweidlem26  44742  stoweidlem34  44750  stoweidlem40  44756  stoweidlem41  44757  stoweidlem42  44758  stoweidlem45  44761  stoweidlem60  44776  stoweidlem62  44778  wallispilem3  44783  wallispilem4  44784  wallispi  44786  wallispi2lem1  44787  stirlinglem5  44794  stirlinglem11  44800  stirlinglem12  44801  dirkercncflem1  44819  fourierdlem4  44827  fourierdlem6  44829  fourierdlem7  44830  fourierdlem9  44832  fourierdlem13  44836  fourierdlem14  44837  fourierdlem15  44838  fourierdlem19  44842  fourierdlem26  44849  fourierdlem35  44858  fourierdlem39  44862  fourierdlem40  44863  fourierdlem41  44864  fourierdlem42  44865  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem51  44873  fourierdlem56  44878  fourierdlem57  44879  fourierdlem59  44881  fourierdlem60  44882  fourierdlem61  44883  fourierdlem63  44885  fourierdlem64  44886  fourierdlem65  44887  fourierdlem66  44888  fourierdlem68  44890  fourierdlem71  44893  fourierdlem72  44894  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem78  44900  fourierdlem79  44901  fourierdlem81  44903  fourierdlem82  44904  fourierdlem83  44905  fourierdlem84  44906  fourierdlem88  44910  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  fourierdlem92  44914  fourierdlem93  44915  fourierdlem95  44917  fourierdlem97  44919  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  fourierdlem107  44929  fourierdlem109  44931  fourierdlem111  44933  fouriersw  44947  elaa2lem  44949  etransclem23  44973  rrxtopnfi  45003  rrndistlt  45006  ioorrnopnlem  45020  ioorrnopnxrlem  45022  sge0gtfsumgt  45159  iundjiun  45176  volicorecl  45262  hoiprodcl  45263  hoiprodcl3  45296  volicore  45297  hoidmvcl  45298  hoidmv1lelem2  45308  hoidmv1lelem3  45309  hoidmv1le  45310  hoidmvlelem1  45311  hoidmvlelem2  45312  hoiqssbllem1  45338  hoiqssbllem2  45339  hoiqssbllem3  45340  hspmbllem1  45342  ovolval5lem1  45368  ovolval5lem2  45369  iunhoiioolem  45391  iccvonmbllem  45394  vonicclem1  45399  preimageiingt  45436  salpreimagtge  45441  smfaddlem1  45479  smflimlem4  45490  smfmullem1  45507  smfmullem2  45508  smfmullem3  45509  ltsubsubaddltsub  46009  2elfz2melfz  46026  requad01  46289  requad1  46290  requad2  46291  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  bgoldbtbndlem4  46476  bgoldbtbnd  46477  ply1mulgsumlem2  47068  difmodm1lt  47208  nnpw2pmod  47269  dignn0flhalflem1  47301  affinecomb1  47388  rrxlinesc  47421  rrxlinec  47422  eenglngeehlnmlem1  47423  eenglngeehlnmlem2  47424  rrx2vlinest  47427  rrx2linest2  47430  2sphere  47435  line2  47438  itsclc0lem2  47443  itsclc0lem3  47444  itscnhlc0yqe  47445  itsclc0yqsollem2  47449  itsclc0yqsol  47450  itscnhlc0xyqsol  47451  itsclinecirc0  47459  itsclinecirc0b  47460  itsclinecirc0in  47461  itsclquadb  47462  2itscp  47467  itscnhlinecirc02plem1  47468  itscnhlinecirc02p  47471  inlinecirc02plem  47472  amgmwlem  47849