Theorem resubcld 11637

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

Syntax hints:   → wi 4   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094   − cmin 11436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-ltxr 11243  df-sub 11438  df-neg 11439

This theorem is referenced by:  ltsubadd  11679  lesubadd  11681  lesub1  11703  lesub2  11704  ltsub1  11705  ltsub2  11706  lt2sub  11707  le2sub  11708  ltmul1a  12059  supaddc  12177  cru  12205  ge2halflem1  13128  qbtwnre  13220  lincmb01cmp  13517  iccf1o  13518  xov1plusxeqvd  13520  intfracq  13888  fldiv  13889  modlt  13909  modsubdir  13972  modsumfzodifsn  13976  serle  14089  expmulnbnd  14267  discr  14272  fzsdom2  14461  cshwidxmod  14836  sgnsub  15139  crre  15161  remullem  15175  01sqrexlem7  15295  absrdbnd  15389  fzomaxdiflem  15390  caubnd2  15405  amgm2  15417  icodiamlt  15485  bhmafibid1  15515  mulcn2  15643  reccn2  15644  rlimo1  15664  climle  15687  climsqz  15688  climsqz2  15689  rlimle  15695  isercolllem1  15712  climsup  15717  caucvgrlem  15720  caucvgrlem2  15722  iseraltlem2  15730  iseraltlem3  15731  iseralt  15732  fsumle  15847  cvgcmp  15864  cvgcmpce  15866  bpoly4  16108  eflt  16168  resinhcl  16207  tanhlt1  16211  sin01bnd  16236  sin01gt0  16241  moddvds  16316  bitscmp  16491  bitsinv1lem  16494  smueqlem  16543  modprm0  16860  pcbc  16955  4sqlem15  17014  blss2ps  24560  blss2  24561  blssps  24581  blss  24582  nm2dif  24782  nlmvscnlem2  24842  nrginvrcnlem  24848  iccntr  24979  icccmplem2  24981  metdstri  25009  cnllycmp  25115  evth  25118  lebnumii  25125  ipcnlem2  25403  cncmet  25481  rrxds  25552  rrxmval  25564  rrxmet  25567  rrxdstprj1  25568  rrxdsfi  25570  ehl1eudis  25579  ehl2eudis  25581  minveclem3b  25587  minveclem4  25591  ivthlem2  25611  ivthlem3  25612  ovollb2lem  25647  ovoliunlem1  25661  ovolscalem1  25672  ovolicc1  25675  ovolicc2lem4  25679  ovolicc2  25681  ovolicc  25682  voliunlem2  25710  ovolioo  25727  ioorcl2  25731  uniioovol  25738  uniioombllem2  25742  uniioombllem3a  25743  uniioombllem3  25744  uniioombllem4  25745  uniioombllem6  25747  opnmbllem  25760  volcn  25765  vitalilem2  25768  ismbf3d  25813  mbfaddlem  25819  i1fadd  25854  itg1addlem4  25858  mbfi1fseqlem6  25879  itg2seq  25901  itg2split  25908  itg2cnlem2  25921  itg2cn  25922  itgrevallem1  25954  dvcjbr  26108  dvferm1lem  26143  dvferm2lem  26145  cmvth  26150  mvth  26151  dvlip  26152  dvlip2  26154  c1liplem1  26155  dvgt0  26163  dvlt0  26164  dvge0  26165  dvle  26166  dvivthlem1  26167  lhop1lem  26172  lhop  26175  dvcnvrelem1  26176  dvcnvrelem2  26177  dvcnvre  26178  dvcvx  26179  dvfsumle  26180  dvfsumge  26181  dvfsumrlimf  26184  dvfsumlem2  26186  dvfsumlem3  26187  dvfsumlem4  26188  dvfsum2  26193  ftc1a  26196  ftc1lem4  26198  coe1mul3  26256  ply1divex  26294  plydivex  26458  aalioulem2  26496  aalioulem3  26497  aalioulem4  26498  aalioulem5  26499  aalioulem6  26500  aaliou3lem7  26512  taylthlem2  26537  mtest  26567  pilem2  26615  tangtx  26670  cosordlem  26695  efif1olem2  26708  logcnlem3  26809  logcnlem4  26810  isosctrlem2  26984  chordthmlem2  26998  chordthmlem4  27000  heron  27003  atanlogsublem  27080  atantan  27088  birthdaylem3  27118  logdifbnd  27158  emcllem1  27160  emcllem2  27161  emcllem5  27164  emcllem6  27165  harmonicbnd4  27175  fsumharmonic  27176  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamucov  27202  relgamcl  27226  ftalem2  27238  ftalem5  27241  chpub  27384  logfaclbnd  27386  logfacbnd3  27387  logexprlim  27389  bposlem1  27448  bposlem9  27456  gausslemma2dlem1a  27529  lgseisenlem1  27539  lgsquadlem1  27544  2sqmod  27600  chtppilimlem1  27637  vmadivsum  27646  vmadivsumb  27647  rplogsumlem1  27648  rplogsumlem2  27649  rpvmasumlem  27651  dchrisumlem2  27654  dchrisum0re  27677  rplogsum  27691  mulogsumlem  27695  mulog2sumlem1  27698  vmalogdivsum2  27702  vmalogdivsum  27703  2vmadivsumlem  27704  log2sumbnd  27708  selbergb  27713  selberg2lem  27714  selberg2b  27716  chpdifbndlem1  27717  selberg3lem1  27721  selberg3lem2  27722  selberg3  27723  selberg4lem1  27724  selberg4  27725  pntrf  27727  pntrmax  27728  pntrsumo1  27729  selberg3r  27733  selberg4r  27734  selberg34r  27735  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntrlog2bnd  27748  pntpbnd1a  27749  pntpbnd2  27751  pntibndlem2  27755  pntlemg  27762  pntlemn  27764  pntlemj  27767  pntlemf  27769  pntlemo  27771  pntlem3  27773  pntleml  27775  ttgcontlem1  29234  eqeelen  29254  brbtwn2  29255  colinearalg  29260  axcgrid  29266  axsegconlem1  29267  axsegconlem3  29269  axsegconlem8  29274  axsegconlem9  29275  axsegconlem10  29276  ax5seglem3a  29280  ax5seg  29288  axpaschlem  29290  axcontlem8  29321  nbusgrvtxm1  29729  crctcshwlkn0lem3  30161  crctcshwlkn0lem5  30163  crctcsh  30173  clwlkclwwlklem2fv2  30347  clwlkclwwlklem2a4  30348  clwlkclwwlklem2a  30349  nvabs  31024  dipcj  31066  minvecolem4  31232  lt2addrd  33095  xlt2addrd  33104  fzsplit3  33138  bcm1n  33140  ply1degltel  33884  ply1degltlss  33886  iconstr  34156  constrresqrtcl  34167  cos9thpiminplylem1  34172  submateqlem1  34197  cnre2csqlem  34300  tpr2rico  34302  dya2ub  34660  dya2icoseg  34667  ballotlemfcc  34884  ballotlemfrcn0  34920  signslema  34949  ftc2re  34985  subfacval3  35681  dnibndlem8  37094  dnibndlem10  37096  dnibndlem11  37097  dnibndlem12  37098  dnicn  37101  knoppcnlem4  37105  unblimceq0  37116  unbdqndv2lem2  37119  knoppndvlem11  37131  knoppndvlem14  37134  knoppndvlem15  37135  knoppndvlem17  37137  knoppndvlem20  37140  irrdifflemf  37989  qdiff  37991  poimirlem29  38320  broucube  38325  opnmbllem0  38327  mblfinlem3  38330  mblfinlem4  38331  itg2addnclem  38342  itg2addnclem3  38344  itg2gt0cn  38346  ftc1cnnclem  38362  areacirclem1  38379  areacirclem2  38380  areacirclem4  38382  areacirclem5  38383  areacirc  38384  cntotbnd  38467  rrnmet  38500  rrndstprj1  38501  rrndstprj2  38502  lcmineqlem23  42838  intlewftc  42848  aks4d1p1p2  42857  aks4d1p1p4  42858  dvle2  42859  aks4d1p1  42863  primrootlekpowne0  42892  hashscontpow1  42908  aks6d1c2  42917  aks6d1c5lem2  42925  sticksstones10  42942  sticksstones12a  42944  sticksstones12  42945  aks6d1c6lem3  42959  bcled  42965  bcle2d  42966  unitscyglem2  42983  unitscyglem4  42985  readdrcl2d  43054  frlmvscadiccat  43300  fltnlta  43415  3cubeslem2  43436  3cubeslem4  43440  irrapxlem2  43570  irrapxlem3  43571  irrapxlem4  43572  irrapxlem5  43573  pellexlem2  43577  pellexlem6  43581  pell1qrgaplem  43620  rmspecsqrtnq  43653  rmspecfund  43656  rmspecpos  43663  jm2.24nn  43706  jm2.17c  43709  fzmaxdif  43728  acongeq  43730  modabsdifz  43733  jm3.1lem2  43765  areaquad  43963  sqrtcvallem2  44383  sqrtcvallem3  44384  sqrtcval  44387  imo72b2lem0  44911  cvgdvgrat  45043  hashnzfzclim  45052  binomcxplemdvbinom  45083  oddfl  46017  lefldiveq  46031  fperiodmul  46043  fzdifsuc2  46049  suprltrp  46064  supxrgere  46069  supxrgelem  46073  suplesup  46075  infleinflem2  46106  infleinf  46107  xrralrecnnge  46125  iccshift  46254  iooshift  46258  iooiinicc  46278  fmul01lt1lem2  46321  climinf  46342  sumnnodd  46366  ltmod  46372  lptre2pt  46374  climleltrp  46410  limsupgtlem  46511  liminflimsupclim  46541  fperdvper  46653  dvbdfbdioolem1  46662  dvbdfbdioolem2  46663  dvbdfbdioo  46664  ioodvbdlimc1lem1  46665  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  dvnmul  46677  iblspltprt  46707  itgspltprt  46713  itgiccshift  46714  itgperiod  46715  itgsbtaddcnst  46716  sublevolico  46718  stoweidlem1  46735  stoweidlem11  46745  stoweidlem12  46746  stoweidlem13  46747  stoweidlem14  46748  stoweidlem23  46757  stoweidlem24  46758  stoweidlem25  46759  stoweidlem26  46760  stoweidlem34  46768  stoweidlem40  46774  stoweidlem41  46775  stoweidlem42  46776  stoweidlem45  46779  stoweidlem60  46794  stoweidlem62  46796  wallispilem3  46801  wallispilem4  46802  wallispi  46804  wallispi2lem1  46805  stirlinglem5  46812  stirlinglem11  46818  stirlinglem12  46819  dirkercncflem1  46837  fourierdlem4  46845  fourierdlem6  46847  fourierdlem7  46848  fourierdlem9  46850  fourierdlem13  46854  fourierdlem14  46855  fourierdlem15  46856  fourierdlem19  46860  fourierdlem26  46867  fourierdlem35  46876  fourierdlem39  46880  fourierdlem40  46881  fourierdlem41  46882  fourierdlem42  46883  fourierdlem48  46888  fourierdlem49  46889  fourierdlem50  46890  fourierdlem51  46891  fourierdlem56  46896  fourierdlem57  46897  fourierdlem59  46899  fourierdlem60  46900  fourierdlem61  46901  fourierdlem63  46903  fourierdlem64  46904  fourierdlem65  46905  fourierdlem66  46906  fourierdlem68  46908  fourierdlem71  46911  fourierdlem72  46912  fourierdlem73  46913  fourierdlem74  46914  fourierdlem75  46915  fourierdlem76  46916  fourierdlem78  46918  fourierdlem79  46919  fourierdlem81  46921  fourierdlem82  46922  fourierdlem83  46923  fourierdlem84  46924  fourierdlem88  46928  fourierdlem89  46929  fourierdlem90  46930  fourierdlem91  46931  fourierdlem92  46932  fourierdlem93  46933  fourierdlem95  46935  fourierdlem97  46937  fourierdlem101  46941  fourierdlem103  46943  fourierdlem104  46944  fourierdlem107  46947  fourierdlem109  46949  fourierdlem111  46951  fouriersw  46965  elaa2lem  46967  etransclem23  46991  rrxtopnfi  47021  rrndistlt  47024  ioorrnopnlem  47038  ioorrnopnxrlem  47040  sge0gtfsumgt  47177  iundjiun  47194  volicorecl  47280  hoiprodcl  47281  hoiprodcl3  47314  volicore  47315  hoidmvcl  47316  hoidmv1lelem2  47326  hoidmv1lelem3  47327  hoidmv1le  47328  hoidmvlelem1  47329  hoidmvlelem2  47330  hoiqssbllem1  47356  hoiqssbllem2  47357  hoiqssbllem3  47358  hspmbllem1  47360  ovolval5lem1  47386  ovolval5lem2  47387  iunhoiioolem  47409  iccvonmbllem  47412  vonicclem1  47417  preimageiingt  47454  salpreimagtge  47459  smfaddlem1  47497  smflimlem4  47508  smfmullem1  47525  smfmullem2  47526  smfmullem3  47527  ltsubsubaddltsub  48058  2elfz2melfz  48075  2tceilhalfelfzo1  48093  flmrecm1  48100  requad01  48406  requad1  48407  requad2  48408  bgoldbtbndlem2  48591  bgoldbtbndlem3  48592  bgoldbtbndlem4  48593  bgoldbtbnd  48594  gpgedgvtx0  48846  gpgedgvtx1  48847  gpg5nbgrvtx03starlem2  48854  gpg5nbgrvtx13starlem2  48857  ply1mulgsumlem2  49187  nnpw2pmod  49383  dignn0flhalflem1  49415  affinecomb1  49502  rrxlinesc  49535  rrxlinec  49536  eenglngeehlnmlem1  49537  eenglngeehlnmlem2  49538  rrx2vlinest  49541  rrx2linest2  49544  2sphere  49549  line2  49552  itsclc0lem2  49557  itsclc0lem3  49558  itscnhlc0yqe  49559  itsclc0yqsollem2  49563  itsclc0yqsol  49564  itscnhlc0xyqsol  49565  itsclinecirc0  49573  itsclinecirc0b  49574  itsclinecirc0in  49575  itsclquadb  49576  2itscp  49581  itscnhlinecirc02plem1  49582  itscnhlinecirc02p  49585  inlinecirc02plem  49586  crossp3i  50668  amgmwlem  50669