Theorem resubcld 11663

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7403  ℝcr 11126   − cmin 11464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-ltxr 11272  df-sub 11466  df-neg 11467

This theorem is referenced by:  ltsubadd  11705  lesubadd  11707  lesub1  11729  lesub2  11730  ltsub1  11731  ltsub2  11732  lt2sub  11733  le2sub  11734  ltmul1a  12088  supaddc  12207  cru  12230  ge2halflem1  13122  qbtwnre  13213  lincmb01cmp  13510  iccf1o  13511  xov1plusxeqvd  13513  intfracq  13874  fldiv  13875  modlt  13895  modsubdir  13956  modsumfzodifsn  13960  serle  14073  expmulnbnd  14251  discr  14256  fzsdom2  14444  cshwidxmod  14819  crre  15131  remullem  15145  01sqrexlem7  15265  absrdbnd  15358  fzomaxdiflem  15359  caubnd2  15374  amgm2  15386  icodiamlt  15452  bhmafibid1  15482  mulcn2  15610  reccn2  15611  rlimo1  15631  climle  15654  climsqz  15655  climsqz2  15656  rlimle  15662  isercolllem1  15679  climsup  15684  caucvgrlem  15687  caucvgrlem2  15689  iseraltlem2  15697  iseraltlem3  15698  iseralt  15699  fsumle  15813  cvgcmp  15830  cvgcmpce  15832  bpoly4  16073  eflt  16133  resinhcl  16172  tanhlt1  16176  sin01bnd  16201  sin01gt0  16206  moddvds  16281  bitscmp  16455  bitsinv1lem  16458  smueqlem  16507  modprm0  16823  pcbc  16918  4sqlem15  16977  blss2ps  24340  blss2  24341  blssps  24361  blss  24362  nm2dif  24562  nlmvscnlem2  24622  nrginvrcnlem  24628  iccntr  24759  icccmplem2  24761  metdstri  24789  cnllycmp  24904  evth  24907  lebnumii  24914  ipcnlem2  25194  cncmet  25272  rrxds  25343  rrxmval  25355  rrxmet  25358  rrxdstprj1  25359  rrxdsfi  25361  ehl1eudis  25370  ehl2eudis  25372  minveclem3b  25378  minveclem4  25382  ivthlem2  25403  ivthlem3  25404  ovollb2lem  25439  ovoliunlem1  25453  ovolscalem1  25464  ovolicc1  25467  ovolicc2lem4  25471  ovolicc2  25473  ovolicc  25474  voliunlem2  25502  ovolioo  25519  ioorcl2  25523  uniioovol  25530  uniioombllem2  25534  uniioombllem3a  25535  uniioombllem3  25536  uniioombllem4  25537  uniioombllem6  25539  opnmbllem  25552  volcn  25557  vitalilem2  25560  ismbf3d  25605  mbfaddlem  25611  i1fadd  25646  itg1addlem4  25650  mbfi1fseqlem6  25671  itg2seq  25693  itg2split  25700  itg2cnlem2  25713  itg2cn  25714  itgrevallem1  25746  dvcjbr  25903  dvferm1lem  25938  dvferm2lem  25940  cmvth  25945  cmvthOLD  25946  mvth  25947  dvlip  25948  dvlip2  25950  c1liplem1  25951  dvgt0  25959  dvlt0  25960  dvge0  25961  dvle  25962  dvivthlem1  25963  lhop1lem  25968  lhop  25971  dvcnvrelem1  25972  dvcnvrelem2  25973  dvcnvre  25974  dvcvx  25975  dvfsumle  25976  dvfsumleOLD  25977  dvfsumge  25978  dvfsumrlimf  25981  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem3  25985  dvfsumlem4  25986  dvfsum2  25991  ftc1a  25994  ftc1lem4  25996  coe1mul3  26054  ply1divex  26092  plydivex  26255  aalioulem2  26291  aalioulem3  26292  aalioulem4  26293  aalioulem5  26294  aalioulem6  26295  aaliou3lem7  26307  taylthlem2  26332  taylthlem2OLD  26333  mtest  26363  pilem2  26412  tangtx  26464  cosordlem  26489  efif1olem2  26502  logcnlem3  26603  logcnlem4  26604  isosctrlem2  26779  chordthmlem2  26793  chordthmlem4  26795  heron  26798  atanlogsublem  26875  atantan  26883  birthdaylem3  26913  logdifbnd  26954  emcllem1  26956  emcllem2  26957  emcllem5  26960  emcllem6  26961  harmonicbnd4  26971  fsumharmonic  26972  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamucov  26998  relgamcl  27022  ftalem2  27034  ftalem5  27037  chpub  27181  logfaclbnd  27183  logfacbnd3  27184  logexprlim  27186  bposlem1  27245  bposlem9  27253  gausslemma2dlem1a  27326  lgseisenlem1  27336  lgsquadlem1  27341  2sqmod  27397  chtppilimlem1  27434  vmadivsum  27443  vmadivsumb  27444  rplogsumlem1  27445  rplogsumlem2  27446  rpvmasumlem  27448  dchrisumlem2  27451  dchrisum0re  27474  rplogsum  27488  mulogsumlem  27492  mulog2sumlem1  27495  vmalogdivsum2  27499  vmalogdivsum  27500  2vmadivsumlem  27501  log2sumbnd  27505  selbergb  27510  selberg2lem  27511  selberg2b  27513  chpdifbndlem1  27514  selberg3lem1  27518  selberg3lem2  27519  selberg3  27520  selberg4lem1  27521  selberg4  27522  pntrf  27524  pntrmax  27525  pntrsumo1  27526  selberg3r  27530  selberg4r  27531  selberg34r  27532  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntrlog2bnd  27545  pntpbnd1a  27546  pntpbnd2  27548  pntibndlem2  27552  pntlemg  27559  pntlemn  27561  pntlemj  27564  pntlemf  27566  pntlemo  27568  pntlem3  27570  pntleml  27572  ttgcontlem1  28810  eqeelen  28829  brbtwn2  28830  colinearalg  28835  axcgrid  28841  axsegconlem1  28842  axsegconlem3  28844  axsegconlem8  28849  axsegconlem9  28850  axsegconlem10  28851  ax5seglem3a  28855  ax5seg  28863  axpaschlem  28865  axcontlem8  28896  nbusgrvtxm1  29304  crctcshwlkn0lem3  29740  crctcshwlkn0lem5  29742  crctcsh  29752  clwlkclwwlklem2fv2  29923  clwlkclwwlklem2a4  29924  clwlkclwwlklem2a  29925  nvabs  30599  dipcj  30641  minvecolem4  30807  lt2addrd  32674  xlt2addrd  32682  fzsplit3  32716  bcm1n  32718  sgnsub  32762  ply1degltel  33550  ply1degltlss  33552  iconstr  33746  constrresqrtcl  33757  cos9thpiminplylem1  33762  submateqlem1  33784  cnre2csqlem  33887  tpr2rico  33889  dya2ub  34248  dya2icoseg  34255  ballotlemfcc  34472  ballotlemfrcn0  34508  signslema  34540  ftc2re  34576  subfacval3  35157  dnibndlem8  36449  dnibndlem10  36451  dnibndlem11  36452  dnibndlem12  36453  dnicn  36456  knoppcnlem4  36460  unblimceq0  36471  unbdqndv2lem2  36474  knoppndvlem11  36486  knoppndvlem14  36489  knoppndvlem15  36490  knoppndvlem17  36492  knoppndvlem20  36495  irrdifflemf  37289  poimirlem29  37619  broucube  37624  opnmbllem0  37626  mblfinlem3  37629  mblfinlem4  37630  itg2addnclem  37641  itg2addnclem3  37643  itg2gt0cn  37645  ftc1cnnclem  37661  areacirclem1  37678  areacirclem2  37679  areacirclem4  37681  areacirclem5  37682  areacirc  37683  cntotbnd  37766  rrnmet  37799  rrndstprj1  37800  rrndstprj2  37801  lcmineqlem23  42010  intlewftc  42020  aks4d1p1p2  42029  aks4d1p1p4  42030  dvle2  42031  aks4d1p1  42035  primrootlekpowne0  42064  hashscontpow1  42080  aks6d1c2  42089  aks6d1c5lem2  42097  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  aks6d1c6lem3  42131  bcled  42137  bcle2d  42138  unitscyglem2  42155  unitscyglem4  42157  metakunt1  42164  metakunt7  42170  metakunt16  42179  metakunt18  42181  metakunt28  42191  metakunt29  42192  metakunt30  42193  readdrcl2d  42270  frlmvscadiccat  42476  fltnlta  42633  3cubeslem2  42655  3cubeslem4  42659  irrapxlem2  42793  irrapxlem3  42794  irrapxlem4  42795  irrapxlem5  42796  pellexlem2  42800  pellexlem6  42804  pell1qrgaplem  42843  rmspecsqrtnq  42876  rmspecfund  42879  rmspecpos  42887  jm2.24nn  42930  jm2.17c  42933  fzmaxdif  42952  acongeq  42954  modabsdifz  42957  jm3.1lem2  42989  areaquad  43187  sqrtcvallem2  43608  sqrtcvallem3  43609  sqrtcval  43612  imo72b2lem0  44136  cvgdvgrat  44285  hashnzfzclim  44294  binomcxplemdvbinom  44325  oddfl  45254  lefldiveq  45269  fperiodmul  45281  fzdifsuc2  45287  suprltrp  45303  supxrgere  45308  supxrgelem  45312  suplesup  45314  infleinflem2  45346  infleinf  45347  xrralrecnnge  45365  iccshift  45495  iooshift  45499  iooiinicc  45519  fmul01lt1lem2  45562  climinf  45583  sumnnodd  45607  ltmod  45615  lptre2pt  45617  climleltrp  45653  limsupgtlem  45754  liminflimsupclim  45784  fperdvper  45896  dvbdfbdioolem1  45905  dvbdfbdioolem2  45906  dvbdfbdioo  45907  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnmul  45920  iblspltprt  45950  itgspltprt  45956  itgiccshift  45957  itgperiod  45958  itgsbtaddcnst  45959  sublevolico  45961  stoweidlem1  45978  stoweidlem11  45988  stoweidlem12  45989  stoweidlem13  45990  stoweidlem14  45991  stoweidlem23  46000  stoweidlem24  46001  stoweidlem25  46002  stoweidlem26  46003  stoweidlem34  46011  stoweidlem40  46017  stoweidlem41  46018  stoweidlem42  46019  stoweidlem45  46022  stoweidlem60  46037  stoweidlem62  46039  wallispilem3  46044  wallispilem4  46045  wallispi  46047  wallispi2lem1  46048  stirlinglem5  46055  stirlinglem11  46061  stirlinglem12  46062  dirkercncflem1  46080  fourierdlem4  46088  fourierdlem6  46090  fourierdlem7  46091  fourierdlem9  46093  fourierdlem13  46097  fourierdlem14  46098  fourierdlem15  46099  fourierdlem19  46103  fourierdlem26  46110  fourierdlem35  46119  fourierdlem39  46123  fourierdlem40  46124  fourierdlem41  46125  fourierdlem42  46126  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem51  46134  fourierdlem56  46139  fourierdlem57  46140  fourierdlem59  46142  fourierdlem60  46143  fourierdlem61  46144  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem66  46149  fourierdlem68  46151  fourierdlem71  46154  fourierdlem72  46155  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem78  46161  fourierdlem79  46162  fourierdlem81  46164  fourierdlem82  46165  fourierdlem83  46166  fourierdlem84  46167  fourierdlem88  46171  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem92  46175  fourierdlem93  46176  fourierdlem95  46178  fourierdlem97  46180  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem107  46190  fourierdlem109  46192  fourierdlem111  46194  fouriersw  46208  elaa2lem  46210  etransclem23  46234  rrxtopnfi  46264  rrndistlt  46267  ioorrnopnlem  46281  ioorrnopnxrlem  46283  sge0gtfsumgt  46420  iundjiun  46437  volicorecl  46523  hoiprodcl  46524  hoiprodcl3  46557  volicore  46558  hoidmvcl  46559  hoidmv1lelem2  46569  hoidmv1lelem3  46570  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem2  46573  hoiqssbllem1  46599  hoiqssbllem2  46600  hoiqssbllem3  46601  hspmbllem1  46603  ovolval5lem1  46629  ovolval5lem2  46630  iunhoiioolem  46652  iccvonmbllem  46655  vonicclem1  46660  preimageiingt  46697  salpreimagtge  46702  smfaddlem1  46740  smflimlem4  46751  smfmullem1  46768  smfmullem2  46769  smfmullem3  46770  ltsubsubaddltsub  47278  2elfz2melfz  47295  2tceilhalfelfzo1  47309  requad01  47583  requad1  47584  requad2  47585  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  bgoldbtbndlem4  47770  bgoldbtbnd  47771  gpgedgvtx0  48013  gpgedgvtx1  48014  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx13starlem2  48022  ply1mulgsumlem2  48311  difmodm1lt  48450  nnpw2pmod  48511  dignn0flhalflem1  48543  affinecomb1  48630  rrxlinesc  48663  rrxlinec  48664  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  rrx2vlinest  48669  rrx2linest2  48672  2sphere  48677  line2  48680  itsclc0lem2  48685  itsclc0lem3  48686  itscnhlc0yqe  48687  itsclc0yqsollem2  48691  itsclc0yqsol  48692  itscnhlc0xyqsol  48693  itsclinecirc0  48701  itsclinecirc0b  48702  itsclinecirc0in  48703  itsclquadb  48704  2itscp  48709  itscnhlinecirc02plem1  48710  itscnhlinecirc02p  48713  inlinecirc02plem  48714  amgmwlem  49614