Theorem resubcld 11106

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

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7150  ℝcr 10574   − cmin 10908

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-po 5443  df-so 5444  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-er 8299  df-en 8528  df-dom 8529  df-sdom 8530  df-pnf 10715  df-mnf 10716  df-ltxr 10718  df-sub 10910  df-neg 10911

This theorem is referenced by:  ltsubadd  11148  lesubadd  11150  lesub1  11172  lesub2  11173  ltsub1  11174  ltsub2  11175  lt2sub  11176  le2sub  11177  ltmul1a  11527  supaddc  11644  cru  11666  qbtwnre  12633  lincmb01cmp  12927  iccf1o  12928  xov1plusxeqvd  12930  intfracq  13276  fldiv  13277  modlt  13297  modsubdir  13357  modsumfzodifsn  13361  serle  13475  expmulnbnd  13646  discr  13651  fzsdom2  13839  cshwidxmod  14212  crre  14521  remullem  14535  sqrlem7  14656  absrdbnd  14749  fzomaxdiflem  14750  caubnd2  14765  amgm2  14777  icodiamlt  14843  bhmafibid1  14873  mulcn2  15000  reccn2  15001  rlimo1  15021  climle  15044  climsqz  15045  climsqz2  15046  rlimle  15052  isercolllem1  15069  climsup  15074  caucvgrlem  15077  caucvgrlem2  15079  iseraltlem2  15087  iseraltlem3  15088  iseralt  15089  fsumle  15202  cvgcmp  15219  cvgcmpce  15221  bpoly4  15461  eflt  15518  resinhcl  15557  tanhlt1  15561  sin01bnd  15586  sin01gt0  15591  moddvds  15666  bitscmp  15837  bitsinv1lem  15840  smueqlem  15889  modprm0  16197  pcbc  16291  4sqlem15  16350  blss2ps  23105  blss2  23106  blssps  23126  blss  23127  nm2dif  23327  nlmvscnlem2  23387  nrginvrcnlem  23393  iccntr  23522  icccmplem2  23524  metdstri  23552  cnllycmp  23657  evth  23660  lebnumii  23667  ipcnlem2  23944  cncmet  24022  rrxds  24093  rrxmval  24105  rrxmet  24108  rrxdstprj1  24109  rrxdsfi  24111  ehl1eudis  24120  ehl2eudis  24122  minveclem3b  24128  minveclem4  24132  ivthlem2  24152  ivthlem3  24153  ovollb2lem  24188  ovoliunlem1  24202  ovolscalem1  24213  ovolicc1  24216  ovolicc2lem4  24220  ovolicc2  24222  ovolicc  24223  voliunlem2  24251  ovolioo  24268  ioorcl2  24272  uniioovol  24279  uniioombllem2  24283  uniioombllem3a  24284  uniioombllem3  24285  uniioombllem4  24286  uniioombllem6  24288  opnmbllem  24301  volcn  24306  vitalilem2  24309  ismbf3d  24354  mbfaddlem  24360  i1fadd  24395  itg1addlem4  24399  mbfi1fseqlem6  24420  itg2seq  24442  itg2split  24449  itg2cnlem2  24462  itg2cn  24463  itgrevallem1  24494  dvcjbr  24648  dvferm1lem  24683  dvferm2lem  24685  cmvth  24690  mvth  24691  dvlip  24692  dvlip2  24694  c1liplem1  24695  dvgt0  24703  dvlt0  24704  dvge0  24705  dvle  24706  dvivthlem1  24707  lhop1lem  24712  lhop  24715  dvcnvrelem1  24716  dvcnvrelem2  24717  dvcnvre  24718  dvcvx  24719  dvfsumle  24720  dvfsumge  24721  dvfsumrlimf  24724  dvfsumlem2  24726  dvfsumlem3  24727  dvfsumlem4  24728  dvfsum2  24733  ftc1a  24736  ftc1lem4  24738  coe1mul3  24799  ply1divex  24836  plydivex  24992  aalioulem2  25028  aalioulem3  25029  aalioulem4  25030  aalioulem5  25031  aalioulem6  25032  aaliou3lem7  25044  taylthlem2  25068  mtest  25098  pilem2  25146  tangtx  25197  cosordlem  25221  efif1olem2  25234  logcnlem3  25334  logcnlem4  25335  isosctrlem2  25504  chordthmlem2  25518  chordthmlem4  25520  heron  25523  atanlogsublem  25600  atantan  25608  birthdaylem3  25638  logdifbnd  25678  emcllem1  25680  emcllem2  25681  emcllem5  25684  emcllem6  25685  harmonicbnd4  25695  fsumharmonic  25696  lgamgulmlem2  25714  lgamgulmlem3  25715  lgamucov  25722  relgamcl  25746  ftalem2  25758  ftalem5  25761  chpub  25903  logfaclbnd  25905  logfacbnd3  25906  logexprlim  25908  bposlem1  25967  bposlem9  25975  gausslemma2dlem1a  26048  lgseisenlem1  26058  lgsquadlem1  26063  2sqmod  26119  chtppilimlem1  26156  vmadivsum  26165  vmadivsumb  26166  rplogsumlem1  26167  rplogsumlem2  26168  rpvmasumlem  26170  dchrisumlem2  26173  dchrisum0re  26196  rplogsum  26210  mulogsumlem  26214  mulog2sumlem1  26217  vmalogdivsum2  26221  vmalogdivsum  26222  2vmadivsumlem  26223  log2sumbnd  26227  selbergb  26232  selberg2lem  26233  selberg2b  26235  chpdifbndlem1  26236  selberg3lem1  26240  selberg3lem2  26241  selberg3  26242  selberg4lem1  26243  selberg4  26244  pntrf  26246  pntrmax  26247  pntrsumo1  26248  selberg3r  26252  selberg4r  26253  selberg34r  26254  pntrlog2bndlem1  26260  pntrlog2bndlem2  26261  pntrlog2bndlem3  26262  pntrlog2bndlem4  26263  pntrlog2bndlem5  26264  pntrlog2bndlem6  26266  pntrlog2bnd  26267  pntpbnd1a  26268  pntpbnd2  26270  pntibndlem2  26274  pntlemg  26281  pntlemn  26283  pntlemj  26286  pntlemf  26288  pntlemo  26290  pntlem3  26292  pntleml  26294  ttgcontlem1  26778  eqeelen  26797  brbtwn2  26798  colinearalg  26803  axcgrid  26809  axsegconlem1  26810  axsegconlem3  26812  axsegconlem8  26817  axsegconlem9  26818  axsegconlem10  26819  ax5seglem3a  26823  ax5seg  26831  axpaschlem  26833  axcontlem8  26864  nbusgrvtxm1  27268  crctcshwlkn0lem3  27697  crctcshwlkn0lem5  27699  crctcsh  27709  clwlkclwwlklem2fv2  27880  clwlkclwwlklem2a4  27881  clwlkclwwlklem2a  27882  nvabs  28554  dipcj  28596  minvecolem4  28762  lt2addrd  30598  xlt2addrd  30605  fzsplit3  30639  bcm1n  30640  submateqlem1  31278  cnre2csqlem  31381  tpr2rico  31383  dya2ub  31756  dya2icoseg  31763  ballotlemfcc  31979  ballotlemfrcn0  32015  sgnsub  32030  signslema  32060  ftc2re  32097  subfacval3  32667  dnibndlem8  34214  dnibndlem10  34216  dnibndlem11  34217  dnibndlem12  34218  dnicn  34221  knoppcnlem4  34225  unblimceq0  34236  unbdqndv2lem2  34239  knoppndvlem11  34251  knoppndvlem14  34254  knoppndvlem15  34255  knoppndvlem17  34257  knoppndvlem20  34260  irrdifflemf  35019  poimirlem29  35366  broucube  35371  opnmbllem0  35373  mblfinlem3  35376  mblfinlem4  35377  itg2addnclem  35388  itg2addnclem3  35390  itg2gt0cn  35392  ftc1cnnclem  35408  areacirclem1  35425  areacirclem2  35426  areacirclem4  35428  areacirclem5  35429  areacirc  35430  cntotbnd  35514  rrnmet  35547  rrndstprj1  35548  rrndstprj2  35549  lcmineqlem23  39618  intlewftc  39628  aks4d1p1p2  39636  aks4d1p1p4  39637  dvle2  39638  aks4d1p1  39642  metakunt1  39647  metakunt7  39653  metakunt16  39662  metakunt18  39664  metakunt28  39674  metakunt29  39675  metakunt30  39676  frlmvscadiccat  39744  fltnlta  39992  3cubeslem2  39999  3cubeslem4  40003  irrapxlem2  40137  irrapxlem3  40138  irrapxlem4  40139  irrapxlem5  40140  pellexlem2  40144  pellexlem6  40148  pell1qrgaplem  40187  rmspecsqrtnq  40220  rmspecfund  40223  rmspecpos  40230  jm2.24nn  40273  jm2.17c  40276  fzmaxdif  40295  acongeq  40297  modabsdifz  40300  jm3.1lem2  40332  areaquad  40539  sqrtcvallem2  40710  sqrtcvallem3  40711  sqrtcval  40714  imo72b2lem0  41242  cvgdvgrat  41390  hashnzfzclim  41399  binomcxplemdvbinom  41430  oddfl  42276  lefldiveq  42292  fperiodmul  42304  fzdifsuc2  42310  suprltrp  42328  supxrgere  42333  supxrgelem  42337  suplesup  42339  infleinflem2  42371  infleinf  42372  xrralrecnnge  42393  iccshift  42521  iooshift  42525  iooiinicc  42545  fmul01lt1lem2  42593  climinf  42614  sumnnodd  42638  ltmod  42646  lptre2pt  42648  climleltrp  42684  limsupgtlem  42785  liminflimsupclim  42815  fperdvper  42927  dvbdfbdioolem1  42936  dvbdfbdioolem2  42937  dvbdfbdioo  42938  ioodvbdlimc1lem1  42939  ioodvbdlimc1lem2  42940  ioodvbdlimc2lem  42942  dvnmul  42951  iblspltprt  42981  itgspltprt  42987  itgiccshift  42988  itgperiod  42989  itgsbtaddcnst  42990  sublevolico  42992  stoweidlem1  43009  stoweidlem11  43019  stoweidlem12  43020  stoweidlem13  43021  stoweidlem14  43022  stoweidlem23  43031  stoweidlem24  43032  stoweidlem25  43033  stoweidlem26  43034  stoweidlem34  43042  stoweidlem40  43048  stoweidlem41  43049  stoweidlem42  43050  stoweidlem45  43053  stoweidlem60  43068  stoweidlem62  43070  wallispilem3  43075  wallispilem4  43076  wallispi  43078  wallispi2lem1  43079  stirlinglem5  43086  stirlinglem11  43092  stirlinglem12  43093  dirkercncflem1  43111  fourierdlem4  43119  fourierdlem6  43121  fourierdlem7  43122  fourierdlem9  43124  fourierdlem13  43128  fourierdlem14  43129  fourierdlem15  43130  fourierdlem19  43134  fourierdlem26  43141  fourierdlem35  43150  fourierdlem39  43154  fourierdlem40  43155  fourierdlem41  43156  fourierdlem42  43157  fourierdlem48  43162  fourierdlem49  43163  fourierdlem50  43164  fourierdlem51  43165  fourierdlem56  43170  fourierdlem57  43171  fourierdlem59  43173  fourierdlem60  43174  fourierdlem61  43175  fourierdlem63  43177  fourierdlem64  43178  fourierdlem65  43179  fourierdlem66  43180  fourierdlem68  43182  fourierdlem71  43185  fourierdlem72  43186  fourierdlem73  43187  fourierdlem74  43188  fourierdlem75  43189  fourierdlem76  43190  fourierdlem78  43192  fourierdlem79  43193  fourierdlem81  43195  fourierdlem82  43196  fourierdlem83  43197  fourierdlem84  43198  fourierdlem88  43202  fourierdlem89  43203  fourierdlem90  43204  fourierdlem91  43205  fourierdlem92  43206  fourierdlem93  43207  fourierdlem95  43209  fourierdlem97  43211  fourierdlem101  43215  fourierdlem103  43217  fourierdlem104  43218  fourierdlem107  43221  fourierdlem109  43223  fourierdlem111  43225  fouriersw  43239  elaa2lem  43241  etransclem23  43265  rrxtopnfi  43295  rrndistlt  43298  ioorrnopnlem  43312  ioorrnopnxrlem  43314  sge0gtfsumgt  43448  iundjiun  43465  volicorecl  43551  hoiprodcl  43552  hoiprodcl3  43585  volicore  43586  hoidmvcl  43587  hoidmv1lelem2  43597  hoidmv1lelem3  43598  hoidmv1le  43599  hoidmvlelem1  43600  hoidmvlelem2  43601  hoiqssbllem1  43627  hoiqssbllem2  43628  hoiqssbllem3  43629  hspmbllem1  43631  ovolval5lem1  43657  ovolval5lem2  43658  iunhoiioolem  43680  iccvonmbllem  43683  vonicclem1  43688  preimageiingt  43721  salpreimagtge  43725  smfaddlem1  43762  smflimlem4  43773  smfmullem1  43789  smfmullem2  43790  smfmullem3  43791  ltsubsubaddltsub  44226  2elfz2melfz  44243  requad01  44506  requad1  44507  requad2  44508  bgoldbtbndlem2  44691  bgoldbtbndlem3  44692  bgoldbtbndlem4  44693  bgoldbtbnd  44694  ply1mulgsumlem2  45161  difmodm1lt  45301  nnpw2pmod  45362  dignn0flhalflem1  45394  affinecomb1  45481  rrxlinesc  45514  rrxlinec  45515  eenglngeehlnmlem1  45516  eenglngeehlnmlem2  45517  rrx2vlinest  45520  rrx2linest2  45523  2sphere  45528  line2  45531  itsclc0lem2  45536  itsclc0lem3  45537  itscnhlc0yqe  45538  itsclc0yqsollem2  45542  itsclc0yqsol  45543  itscnhlc0xyqsol  45544  itsclinecirc0  45552  itsclinecirc0b  45553  itsclinecirc0in  45554  itsclquadb  45555  2itscp  45560  itscnhlinecirc02plem1  45561  itscnhlinecirc02p  45564  inlinecirc02plem  45565  amgmwlem  45721