Theorem resubcld 11644

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7411  ℝcr 11111   − cmin 11446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11252  df-mnf 11253  df-ltxr 11255  df-sub 11448  df-neg 11449

This theorem is referenced by:  ltsubadd  11686  lesubadd  11688  lesub1  11710  lesub2  11711  ltsub1  11712  ltsub2  11713  lt2sub  11714  le2sub  11715  ltmul1a  12065  supaddc  12183  cru  12206  qbtwnre  13180  lincmb01cmp  13474  iccf1o  13475  xov1plusxeqvd  13477  intfracq  13826  fldiv  13827  modlt  13847  modsubdir  13907  modsumfzodifsn  13911  serle  14025  expmulnbnd  14200  discr  14205  fzsdom2  14390  cshwidxmod  14755  crre  15063  remullem  15077  01sqrexlem7  15197  absrdbnd  15290  fzomaxdiflem  15291  caubnd2  15306  amgm2  15318  icodiamlt  15384  bhmafibid1  15414  mulcn2  15542  reccn2  15543  rlimo1  15563  climle  15586  climsqz  15587  climsqz2  15588  rlimle  15596  isercolllem1  15613  climsup  15618  caucvgrlem  15621  caucvgrlem2  15623  iseraltlem2  15631  iseraltlem3  15632  iseralt  15633  fsumle  15747  cvgcmp  15764  cvgcmpce  15766  bpoly4  16005  eflt  16062  resinhcl  16101  tanhlt1  16105  sin01bnd  16130  sin01gt0  16135  moddvds  16210  bitscmp  16381  bitsinv1lem  16384  smueqlem  16433  modprm0  16740  pcbc  16835  4sqlem15  16894  blss2ps  23916  blss2  23917  blssps  23937  blss  23938  nm2dif  24141  nlmvscnlem2  24209  nrginvrcnlem  24215  iccntr  24344  icccmplem2  24346  metdstri  24374  cnllycmp  24479  evth  24482  lebnumii  24489  ipcnlem2  24768  cncmet  24846  rrxds  24917  rrxmval  24929  rrxmet  24932  rrxdstprj1  24933  rrxdsfi  24935  ehl1eudis  24944  ehl2eudis  24946  minveclem3b  24952  minveclem4  24956  ivthlem2  24976  ivthlem3  24977  ovollb2lem  25012  ovoliunlem1  25026  ovolscalem1  25037  ovolicc1  25040  ovolicc2lem4  25044  ovolicc2  25046  ovolicc  25047  voliunlem2  25075  ovolioo  25092  ioorcl2  25096  uniioovol  25103  uniioombllem2  25107  uniioombllem3a  25108  uniioombllem3  25109  uniioombllem4  25110  uniioombllem6  25112  opnmbllem  25125  volcn  25130  vitalilem2  25133  ismbf3d  25178  mbfaddlem  25184  i1fadd  25219  itg1addlem4  25223  itg1addlem4OLD  25224  mbfi1fseqlem6  25245  itg2seq  25267  itg2split  25274  itg2cnlem2  25287  itg2cn  25288  itgrevallem1  25319  dvcjbr  25473  dvferm1lem  25508  dvferm2lem  25510  cmvth  25515  mvth  25516  dvlip  25517  dvlip2  25519  c1liplem1  25520  dvgt0  25528  dvlt0  25529  dvge0  25530  dvle  25531  dvivthlem1  25532  lhop1lem  25537  lhop  25540  dvcnvrelem1  25541  dvcnvrelem2  25542  dvcnvre  25543  dvcvx  25544  dvfsumle  25545  dvfsumge  25546  dvfsumrlimf  25549  dvfsumlem2  25551  dvfsumlem3  25552  dvfsumlem4  25553  dvfsum2  25558  ftc1a  25561  ftc1lem4  25563  coe1mul3  25624  ply1divex  25661  plydivex  25817  aalioulem2  25853  aalioulem3  25854  aalioulem4  25855  aalioulem5  25856  aalioulem6  25857  aaliou3lem7  25869  taylthlem2  25893  mtest  25923  pilem2  25971  tangtx  26022  cosordlem  26046  efif1olem2  26059  logcnlem3  26159  logcnlem4  26160  isosctrlem2  26331  chordthmlem2  26345  chordthmlem4  26347  heron  26350  atanlogsublem  26427  atantan  26435  birthdaylem3  26465  logdifbnd  26505  emcllem1  26507  emcllem2  26508  emcllem5  26511  emcllem6  26512  harmonicbnd4  26522  fsumharmonic  26523  lgamgulmlem2  26541  lgamgulmlem3  26542  lgamucov  26549  relgamcl  26573  ftalem2  26585  ftalem5  26588  chpub  26730  logfaclbnd  26732  logfacbnd3  26733  logexprlim  26735  bposlem1  26794  bposlem9  26802  gausslemma2dlem1a  26875  lgseisenlem1  26885  lgsquadlem1  26890  2sqmod  26946  chtppilimlem1  26983  vmadivsum  26992  vmadivsumb  26993  rplogsumlem1  26994  rplogsumlem2  26995  rpvmasumlem  26997  dchrisumlem2  27000  dchrisum0re  27023  rplogsum  27037  mulogsumlem  27041  mulog2sumlem1  27044  vmalogdivsum2  27048  vmalogdivsum  27049  2vmadivsumlem  27050  log2sumbnd  27054  selbergb  27059  selberg2lem  27060  selberg2b  27062  chpdifbndlem1  27063  selberg3lem1  27067  selberg3lem2  27068  selberg3  27069  selberg4lem1  27070  selberg4  27071  pntrf  27073  pntrmax  27074  pntrsumo1  27075  selberg3r  27079  selberg4r  27080  selberg34r  27081  pntrlog2bndlem1  27087  pntrlog2bndlem2  27088  pntrlog2bndlem3  27089  pntrlog2bndlem4  27090  pntrlog2bndlem5  27091  pntrlog2bndlem6  27093  pntrlog2bnd  27094  pntpbnd1a  27095  pntpbnd2  27097  pntibndlem2  27101  pntlemg  27108  pntlemn  27110  pntlemj  27113  pntlemf  27115  pntlemo  27117  pntlem3  27119  pntleml  27121  ttgcontlem1  28180  eqeelen  28200  brbtwn2  28201  colinearalg  28206  axcgrid  28212  axsegconlem1  28213  axsegconlem3  28215  axsegconlem8  28220  axsegconlem9  28221  axsegconlem10  28222  ax5seglem3a  28226  ax5seg  28234  axpaschlem  28236  axcontlem8  28267  nbusgrvtxm1  28674  crctcshwlkn0lem3  29104  crctcshwlkn0lem5  29106  crctcsh  29116  clwlkclwwlklem2fv2  29287  clwlkclwwlklem2a4  29288  clwlkclwwlklem2a  29289  nvabs  29963  dipcj  30005  minvecolem4  30171  lt2addrd  32002  xlt2addrd  32009  fzsplit3  32043  bcm1n  32044  ply1degltel  32711  ply1degltlss  32713  submateqlem1  32856  cnre2csqlem  32959  tpr2rico  32961  dya2ub  33338  dya2icoseg  33345  ballotlemfcc  33561  ballotlemfrcn0  33597  sgnsub  33612  signslema  33642  ftc2re  33679  subfacval3  34249  gg-cmvth  35250  gg-dvfsumle  35251  gg-dvfsumlem2  35252  dnibndlem8  35447  dnibndlem10  35449  dnibndlem11  35450  dnibndlem12  35451  dnicn  35454  knoppcnlem4  35458  unblimceq0  35469  unbdqndv2lem2  35472  knoppndvlem11  35484  knoppndvlem14  35487  knoppndvlem15  35488  knoppndvlem17  35490  knoppndvlem20  35493  irrdifflemf  36292  poimirlem29  36603  broucube  36608  opnmbllem0  36610  mblfinlem3  36613  mblfinlem4  36614  itg2addnclem  36625  itg2addnclem3  36627  itg2gt0cn  36629  ftc1cnnclem  36645  areacirclem1  36662  areacirclem2  36663  areacirclem4  36665  areacirclem5  36666  areacirc  36667  cntotbnd  36750  rrnmet  36783  rrndstprj1  36784  rrndstprj2  36785  lcmineqlem23  41002  intlewftc  41012  aks4d1p1p2  41021  aks4d1p1p4  41022  dvle2  41023  aks4d1p1  41027  sticksstones10  41057  sticksstones12a  41059  sticksstones12  41060  metakunt1  41071  metakunt7  41077  metakunt16  41086  metakunt18  41088  metakunt28  41098  metakunt29  41099  metakunt30  41100  frlmvscadiccat  41166  fltnlta  41487  3cubeslem2  41505  3cubeslem4  41509  irrapxlem2  41643  irrapxlem3  41644  irrapxlem4  41645  irrapxlem5  41646  pellexlem2  41650  pellexlem6  41654  pell1qrgaplem  41693  rmspecsqrtnq  41726  rmspecfund  41729  rmspecpos  41737  jm2.24nn  41780  jm2.17c  41783  fzmaxdif  41802  acongeq  41804  modabsdifz  41807  jm3.1lem2  41839  areaquad  42047  sqrtcvallem2  42470  sqrtcvallem3  42471  sqrtcval  42474  imo72b2lem0  42999  cvgdvgrat  43154  hashnzfzclim  43163  binomcxplemdvbinom  43194  oddfl  44066  lefldiveq  44081  fperiodmul  44093  fzdifsuc2  44099  suprltrp  44117  supxrgere  44122  supxrgelem  44126  suplesup  44128  infleinflem2  44160  infleinf  44161  xrralrecnnge  44179  iccshift  44310  iooshift  44314  iooiinicc  44334  fmul01lt1lem2  44380  climinf  44401  sumnnodd  44425  ltmod  44433  lptre2pt  44435  climleltrp  44471  limsupgtlem  44572  liminflimsupclim  44602  fperdvper  44714  dvbdfbdioolem1  44723  dvbdfbdioolem2  44724  dvbdfbdioo  44725  ioodvbdlimc1lem1  44726  ioodvbdlimc1lem2  44727  ioodvbdlimc2lem  44729  dvnmul  44738  iblspltprt  44768  itgspltprt  44774  itgiccshift  44775  itgperiod  44776  itgsbtaddcnst  44777  sublevolico  44779  stoweidlem1  44796  stoweidlem11  44806  stoweidlem12  44807  stoweidlem13  44808  stoweidlem14  44809  stoweidlem23  44818  stoweidlem24  44819  stoweidlem25  44820  stoweidlem26  44821  stoweidlem34  44829  stoweidlem40  44835  stoweidlem41  44836  stoweidlem42  44837  stoweidlem45  44840  stoweidlem60  44855  stoweidlem62  44857  wallispilem3  44862  wallispilem4  44863  wallispi  44865  wallispi2lem1  44866  stirlinglem5  44873  stirlinglem11  44879  stirlinglem12  44880  dirkercncflem1  44898  fourierdlem4  44906  fourierdlem6  44908  fourierdlem7  44909  fourierdlem9  44911  fourierdlem13  44915  fourierdlem14  44916  fourierdlem15  44917  fourierdlem19  44921  fourierdlem26  44928  fourierdlem35  44937  fourierdlem39  44941  fourierdlem40  44942  fourierdlem41  44943  fourierdlem42  44944  fourierdlem48  44949  fourierdlem49  44950  fourierdlem50  44951  fourierdlem51  44952  fourierdlem56  44957  fourierdlem57  44958  fourierdlem59  44960  fourierdlem60  44961  fourierdlem61  44962  fourierdlem63  44964  fourierdlem64  44965  fourierdlem65  44966  fourierdlem66  44967  fourierdlem68  44969  fourierdlem71  44972  fourierdlem72  44973  fourierdlem73  44974  fourierdlem74  44975  fourierdlem75  44976  fourierdlem76  44977  fourierdlem78  44979  fourierdlem79  44980  fourierdlem81  44982  fourierdlem82  44983  fourierdlem83  44984  fourierdlem84  44985  fourierdlem88  44989  fourierdlem89  44990  fourierdlem90  44991  fourierdlem91  44992  fourierdlem92  44993  fourierdlem93  44994  fourierdlem95  44996  fourierdlem97  44998  fourierdlem101  45002  fourierdlem103  45004  fourierdlem104  45005  fourierdlem107  45008  fourierdlem109  45010  fourierdlem111  45012  fouriersw  45026  elaa2lem  45028  etransclem23  45052  rrxtopnfi  45082  rrndistlt  45085  ioorrnopnlem  45099  ioorrnopnxrlem  45101  sge0gtfsumgt  45238  iundjiun  45255  volicorecl  45341  hoiprodcl  45342  hoiprodcl3  45375  volicore  45376  hoidmvcl  45377  hoidmv1lelem2  45387  hoidmv1lelem3  45388  hoidmv1le  45389  hoidmvlelem1  45390  hoidmvlelem2  45391  hoiqssbllem1  45417  hoiqssbllem2  45418  hoiqssbllem3  45419  hspmbllem1  45421  ovolval5lem1  45447  ovolval5lem2  45448  iunhoiioolem  45470  iccvonmbllem  45473  vonicclem1  45478  preimageiingt  45515  salpreimagtge  45520  smfaddlem1  45558  smflimlem4  45569  smfmullem1  45586  smfmullem2  45587  smfmullem3  45588  ltsubsubaddltsub  46088  2elfz2melfz  46105  requad01  46368  requad1  46369  requad2  46370  bgoldbtbndlem2  46553  bgoldbtbndlem3  46554  bgoldbtbndlem4  46555  bgoldbtbnd  46556  ply1mulgsumlem2  47146  difmodm1lt  47286  nnpw2pmod  47347  dignn0flhalflem1  47379  affinecomb1  47466  rrxlinesc  47499  rrxlinec  47500  eenglngeehlnmlem1  47501  eenglngeehlnmlem2  47502  rrx2vlinest  47505  rrx2linest2  47508  2sphere  47513  line2  47516  itsclc0lem2  47521  itsclc0lem3  47522  itscnhlc0yqe  47523  itsclc0yqsollem2  47527  itsclc0yqsol  47528  itscnhlc0xyqsol  47529  itsclinecirc0  47537  itsclinecirc0b  47538  itsclinecirc0in  47539  itsclquadb  47540  2itscp  47545  itscnhlinecirc02plem1  47546  itscnhlinecirc02p  47549  inlinecirc02plem  47550  amgmwlem  47927