Theorem resubcld 10337

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

Syntax hints:   → wi 4   ∈ wcel 1977  (class class class)co 6549  ℝcr 9814   − cmin 10145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-ltxr 9958  df-sub 10147  df-neg 10148

This theorem is referenced by:  ltsubadd  10377  lesubadd  10379  lesub1  10401  lesub2  10402  ltsub1  10403  ltsub2  10404  lt2sub  10405  le2sub  10406  ltmul1a  10751  supaddc  10867  cru  10889  qbtwnre  11904  lincmb01cmp  12186  iccf1o  12187  xov1plusxeqvd  12189  intfracq  12520  fldiv  12521  modlt  12541  modsubdir  12601  modsumfzodifsn  12605  serle  12718  expmulnbnd  12858  discr  12863  fzsdom2  13075  cshwidxmod  13400  crre  13702  remullem  13716  sqrlem7  13837  absrdbnd  13929  fzomaxdiflem  13930  caubnd2  13945  amgm2  13957  icodiamlt  14022  mulcn2  14174  reccn2  14175  rlimo1  14195  climle  14218  climsqz  14219  climsqz2  14220  rlimle  14226  isercolllem1  14243  climsup  14248  caucvgrlem  14251  caucvgrlem2  14253  iseraltlem2  14261  iseraltlem3  14262  iseralt  14263  fsumle  14372  cvgcmp  14389  cvgcmpce  14391  bpoly4  14629  eflt  14686  resinhcl  14725  tanhlt1  14729  sin01bnd  14754  sin01gt0  14759  moddvds  14829  bitscmp  14998  bitsinv1lem  15001  smueqlem  15050  modprm0  15348  pcbc  15442  4sqlem15  15501  blss2ps  22018  blss2  22019  blssps  22039  blss  22040  nm2dif  22239  nlmvscnlem2  22299  nrginvrcnlem  22305  iccntr  22432  icccmplem2  22434  metdstri  22462  cnllycmp  22563  evth  22566  lebnumii  22573  ipcnlem2  22851  cncmet  22927  rrxds  22989  rrxmval  22996  rrxmet  22999  rrxdstprj1  23000  minveclem3b  23007  minveclem4  23011  ivthlem2  23028  ivthlem3  23029  ovollb2lem  23063  ovoliunlem1  23077  ovolscalem1  23088  ovolicc1  23091  ovolicc2lem4  23095  ovolicc2  23097  ovolicc  23098  voliunlem2  23126  ovolioo  23143  ioorcl2  23146  uniioovol  23153  uniioombllem2  23157  uniioombllem3a  23158  uniioombllem3  23159  uniioombllem4  23160  uniioombllem6  23162  opnmbllem  23175  volcn  23180  vitalilem2  23184  ismbf3d  23227  mbfaddlem  23233  i1fadd  23268  itg1addlem4  23272  mbfi1fseqlem6  23293  itg2seq  23315  itg2split  23322  itg2cnlem2  23335  itg2cn  23336  itgrevallem1  23367  dvcjbr  23518  dvferm1lem  23551  dvferm2lem  23553  cmvth  23558  mvth  23559  dvlip  23560  dvlip2  23562  c1liplem1  23563  dvgt0  23571  dvlt0  23572  dvge0  23573  dvle  23574  dvivthlem1  23575  lhop1lem  23580  lhop  23583  dvcnvrelem1  23584  dvcnvrelem2  23585  dvcnvre  23586  dvcvx  23587  dvfsumle  23588  dvfsumge  23589  dvfsumrlimf  23592  dvfsumlem2  23594  dvfsumlem3  23595  dvfsumlem4  23596  dvfsum2  23601  ftc1a  23604  ftc1lem4  23606  coe1mul3  23663  ply1divex  23700  plydivex  23856  aalioulem2  23892  aalioulem3  23893  aalioulem4  23894  aalioulem5  23895  aalioulem6  23896  aaliou3lem7  23908  taylthlem2  23932  mtest  23962  pilem2  24010  tangtx  24061  cosordlem  24081  efif1olem2  24093  logcnlem3  24190  logcnlem4  24191  isosctrlem2  24349  chordthmlem2  24360  chordthmlem4  24362  heron  24365  atanlogsublem  24442  atantan  24450  birthdaylem3  24480  logdifbnd  24520  emcllem1  24522  emcllem2  24523  emcllem5  24526  emcllem6  24527  harmonicbnd4  24537  fsumharmonic  24538  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamucov  24564  relgamcl  24588  ftalem2  24600  ftalem5  24603  chpub  24745  logfaclbnd  24747  logfacbnd3  24748  logexprlim  24750  bposlem1  24809  bposlem9  24817  gausslemma2dlem1a  24890  lgseisenlem1  24900  lgsquadlem1  24905  chtppilimlem1  24962  vmadivsum  24971  vmadivsumb  24972  rplogsumlem1  24973  rplogsumlem2  24974  rpvmasumlem  24976  dchrisumlem2  24979  dchrisum0re  25002  rplogsum  25016  mulogsumlem  25020  mulog2sumlem1  25023  vmalogdivsum2  25027  vmalogdivsum  25028  2vmadivsumlem  25029  log2sumbnd  25033  selbergb  25038  selberg2lem  25039  selberg2b  25041  chpdifbndlem1  25042  selberg3lem1  25046  selberg3lem2  25047  selberg3  25048  selberg4lem1  25049  selberg4  25050  pntrf  25052  pntrmax  25053  pntrsumo1  25054  selberg3r  25058  selberg4r  25059  selberg34r  25060  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntrlog2bnd  25073  pntpbnd1a  25074  pntpbnd2  25076  pntibndlem2  25080  pntlemg  25087  pntlemn  25089  pntlemj  25092  pntlemf  25094  pntlemo  25096  pntlem3  25098  pntleml  25100  ttgcontlem1  25565  eqeelen  25584  brbtwn2  25585  colinearalg  25590  axcgrid  25596  axsegconlem1  25597  axsegconlem3  25599  axsegconlem8  25604  axsegconlem9  25605  axsegconlem10  25606  ax5seglem3a  25610  ax5seg  25618  axpaschlem  25620  axcontlem8  25651  clwlkisclwwlklem2fv2  26311  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  extwwlkfablem2  26605  nvabs  26911  dipcj  26953  minvecolem4  27120  lt2addrd  28903  xlt2addrd  28913  fzsplit3  28940  bcm1n  28941  bhmafibid1  28975  2sqmod  28979  submateqlem1  29201  cnre2csqlem  29284  tpr2rico  29286  dya2ub  29659  dya2icoseg  29666  ballotlemfcc  29882  ballotlemfrcn0  29918  sgnsub  29933  signslema  29965  subfacval3  30425  dnibndlem8  31645  dnibndlem10  31647  dnibndlem11  31648  dnibndlem12  31649  dnicn  31652  knoppcnlem4  31656  unblimceq0  31668  unbdqndv2lem2  31671  knoppndvlem11  31683  knoppndvlem14  31686  knoppndvlem15  31687  knoppndvlem17  31689  knoppndvlem20  31692  poimirlem29  32608  broucube  32613  opnmbllem0  32615  mblfinlem3  32618  mblfinlem4  32619  itg2addnclem  32631  itg2addnclem3  32633  itg2gt0cn  32635  ftc1cnnclem  32653  areacirclem1  32670  areacirclem2  32671  areacirclem4  32673  areacirclem5  32674  areacirc  32675  cntotbnd  32765  rrnmet  32798  rrndstprj1  32799  rrndstprj2  32800  irrapxlem2  36405  irrapxlem3  36406  irrapxlem4  36407  irrapxlem5  36408  pellexlem2  36412  pellexlem6  36416  pell1qrgaplem  36455  rmspecsqrtnq  36488  rmspecfund  36492  rmspecpos  36499  jm2.24nn  36544  jm2.17c  36547  fzmaxdif  36566  acongeq  36568  modabsdifz  36571  jm3.1lem2  36603  areaquad  36821  imo72b2lem0  37487  cvgdvgrat  37534  hashnzfzclim  37543  binomcxplemdvbinom  37574  oddfl  38430  lefldiveq  38446  fperiodmul  38459  fzdifsuc2  38466  suprltrp  38485  supxrgere  38490  supxrgelem  38494  suplesup  38496  infleinflem2  38528  infleinf  38529  xrralrecnnge  38554  iccshift  38591  iooshift  38595  iooiinicc  38616  fmul01lt1lem2  38652  climinf  38673  sumnnodd  38697  ltmod  38705  lptre2pt  38707  climleltrp  38743  fperdvper  38808  dvbdfbdioolem1  38818  dvbdfbdioolem2  38819  dvbdfbdioo  38820  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnmul  38833  iblspltprt  38865  itgspltprt  38871  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  sublevolico  38877  stoweidlem1  38894  stoweidlem11  38904  stoweidlem12  38905  stoweidlem13  38906  stoweidlem14  38907  stoweidlem23  38916  stoweidlem24  38917  stoweidlem25  38918  stoweidlem26  38919  stoweidlem34  38927  stoweidlem40  38933  stoweidlem41  38934  stoweidlem42  38935  stoweidlem45  38938  stoweidlem60  38953  stoweidlem62  38955  wallispilem3  38960  wallispilem4  38961  wallispi  38963  wallispi2lem1  38964  stirlinglem5  38971  stirlinglem11  38977  stirlinglem12  38978  dirkercncflem1  38996  fourierdlem4  39004  fourierdlem6  39006  fourierdlem7  39007  fourierdlem9  39009  fourierdlem13  39013  fourierdlem14  39014  fourierdlem15  39015  fourierdlem19  39019  fourierdlem26  39026  fourierdlem35  39035  fourierdlem39  39039  fourierdlem40  39040  fourierdlem41  39041  fourierdlem42  39042  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem56  39055  fourierdlem57  39056  fourierdlem59  39058  fourierdlem60  39059  fourierdlem61  39060  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem66  39065  fourierdlem68  39067  fourierdlem71  39070  fourierdlem72  39071  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem83  39082  fourierdlem84  39083  fourierdlem88  39087  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem92  39091  fourierdlem93  39092  fourierdlem95  39094  fourierdlem97  39096  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem107  39106  fourierdlem109  39108  fourierdlem111  39110  fouriersw  39124  elaa2lem  39126  etransclem23  39150  rrxdsfi  39181  rrxtopnfi  39182  rrndistlt  39186  ioorrnopnlem  39200  ioorrnopnxrlem  39202  sge0gtfsumgt  39336  iundjiun  39353  volicorecl  39436  hoiprodcl  39437  hoiprodcl3  39470  volicore  39471  hoidmvcl  39472  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoiqssbllem1  39512  hoiqssbllem2  39513  hoiqssbllem3  39514  hspmbllem1  39516  ovolval5lem1  39542  ovolval5lem2  39543  iunhoiioolem  39566  iccvonmbllem  39569  vonicclem1  39574  preimageiingt  39607  salpreimagtge  39611  smfaddlem1  39649  smflimlem4  39660  smfmullem1  39676  smfmullem2  39677  smfmullem3  39678  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbndlem4  40224  bgoldbtbnd  40225  ltsubsubaddltsub  40347  2elfz2melfz  40355  nbusgrvtxm1  40607  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem5  41017  crctcsh  41027  clwlkclwwlklem2fv2  41205  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  av-extwwlkfablem2  41510  ply1mulgsumlem2  41969  difmodm1lt  42111  nnpw2pmod  42175  dignn0flhalflem1  42207  amgmwlem  42357