Theorem resubcld 11718

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7448  ℝcr 11183   − cmin 11520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-ltxr 11329  df-sub 11522  df-neg 11523

This theorem is referenced by:  ltsubadd  11760  lesubadd  11762  lesub1  11784  lesub2  11785  ltsub1  11786  ltsub2  11787  lt2sub  11788  le2sub  11789  ltmul1a  12143  supaddc  12262  cru  12285  qbtwnre  13261  lincmb01cmp  13555  iccf1o  13556  xov1plusxeqvd  13558  intfracq  13910  fldiv  13911  modlt  13931  modsubdir  13991  modsumfzodifsn  13995  serle  14108  expmulnbnd  14284  discr  14289  fzsdom2  14477  cshwidxmod  14851  crre  15163  remullem  15177  01sqrexlem7  15297  absrdbnd  15390  fzomaxdiflem  15391  caubnd2  15406  amgm2  15418  icodiamlt  15484  bhmafibid1  15514  mulcn2  15642  reccn2  15643  rlimo1  15663  climle  15686  climsqz  15687  climsqz2  15688  rlimle  15696  isercolllem1  15713  climsup  15718  caucvgrlem  15721  caucvgrlem2  15723  iseraltlem2  15731  iseraltlem3  15732  iseralt  15733  fsumle  15847  cvgcmp  15864  cvgcmpce  15866  bpoly4  16107  eflt  16165  resinhcl  16204  tanhlt1  16208  sin01bnd  16233  sin01gt0  16238  moddvds  16313  bitscmp  16484  bitsinv1lem  16487  smueqlem  16536  modprm0  16852  pcbc  16947  4sqlem15  17006  blss2ps  24434  blss2  24435  blssps  24455  blss  24456  nm2dif  24659  nlmvscnlem2  24727  nrginvrcnlem  24733  iccntr  24862  icccmplem2  24864  metdstri  24892  cnllycmp  25007  evth  25010  lebnumii  25017  ipcnlem2  25297  cncmet  25375  rrxds  25446  rrxmval  25458  rrxmet  25461  rrxdstprj1  25462  rrxdsfi  25464  ehl1eudis  25473  ehl2eudis  25475  minveclem3b  25481  minveclem4  25485  ivthlem2  25506  ivthlem3  25507  ovollb2lem  25542  ovoliunlem1  25556  ovolscalem1  25567  ovolicc1  25570  ovolicc2lem4  25574  ovolicc2  25576  ovolicc  25577  voliunlem2  25605  ovolioo  25622  ioorcl2  25626  uniioovol  25633  uniioombllem2  25637  uniioombllem3a  25638  uniioombllem3  25639  uniioombllem4  25640  uniioombllem6  25642  opnmbllem  25655  volcn  25660  vitalilem2  25663  ismbf3d  25708  mbfaddlem  25714  i1fadd  25749  itg1addlem4  25753  itg1addlem4OLD  25754  mbfi1fseqlem6  25775  itg2seq  25797  itg2split  25804  itg2cnlem2  25817  itg2cn  25818  itgrevallem1  25850  dvcjbr  26007  dvferm1lem  26042  dvferm2lem  26044  cmvth  26049  cmvthOLD  26050  mvth  26051  dvlip  26052  dvlip2  26054  c1liplem1  26055  dvgt0  26063  dvlt0  26064  dvge0  26065  dvle  26066  dvivthlem1  26067  lhop1lem  26072  lhop  26075  dvcnvrelem1  26076  dvcnvrelem2  26077  dvcnvre  26078  dvcvx  26079  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumrlimf  26085  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumlem4  26090  dvfsum2  26095  ftc1a  26098  ftc1lem4  26100  coe1mul3  26158  ply1divex  26196  plydivex  26357  aalioulem2  26393  aalioulem3  26394  aalioulem4  26395  aalioulem5  26396  aalioulem6  26397  aaliou3lem7  26409  taylthlem2  26434  taylthlem2OLD  26435  mtest  26465  pilem2  26514  tangtx  26565  cosordlem  26590  efif1olem2  26603  logcnlem3  26704  logcnlem4  26705  isosctrlem2  26880  chordthmlem2  26894  chordthmlem4  26896  heron  26899  atanlogsublem  26976  atantan  26984  birthdaylem3  27014  logdifbnd  27055  emcllem1  27057  emcllem2  27058  emcllem5  27061  emcllem6  27062  harmonicbnd4  27072  fsumharmonic  27073  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamucov  27099  relgamcl  27123  ftalem2  27135  ftalem5  27138  chpub  27282  logfaclbnd  27284  logfacbnd3  27285  logexprlim  27287  bposlem1  27346  bposlem9  27354  gausslemma2dlem1a  27427  lgseisenlem1  27437  lgsquadlem1  27442  2sqmod  27498  chtppilimlem1  27535  vmadivsum  27544  vmadivsumb  27545  rplogsumlem1  27546  rplogsumlem2  27547  rpvmasumlem  27549  dchrisumlem2  27552  dchrisum0re  27575  rplogsum  27589  mulogsumlem  27593  mulog2sumlem1  27596  vmalogdivsum2  27600  vmalogdivsum  27601  2vmadivsumlem  27602  log2sumbnd  27606  selbergb  27611  selberg2lem  27612  selberg2b  27614  chpdifbndlem1  27615  selberg3lem1  27619  selberg3lem2  27620  selberg3  27621  selberg4lem1  27622  selberg4  27623  pntrf  27625  pntrmax  27626  pntrsumo1  27627  selberg3r  27631  selberg4r  27632  selberg34r  27633  pntrlog2bndlem1  27639  pntrlog2bndlem2  27640  pntrlog2bndlem3  27641  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntrlog2bnd  27646  pntpbnd1a  27647  pntpbnd2  27649  pntibndlem2  27653  pntlemg  27660  pntlemn  27662  pntlemj  27665  pntlemf  27667  pntlemo  27669  pntlem3  27671  pntleml  27673  ttgcontlem1  28917  eqeelen  28937  brbtwn2  28938  colinearalg  28943  axcgrid  28949  axsegconlem1  28950  axsegconlem3  28952  axsegconlem8  28957  axsegconlem9  28958  axsegconlem10  28959  ax5seglem3a  28963  ax5seg  28971  axpaschlem  28973  axcontlem8  29004  nbusgrvtxm1  29414  crctcshwlkn0lem3  29845  crctcshwlkn0lem5  29847  crctcsh  29857  clwlkclwwlklem2fv2  30028  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  nvabs  30704  dipcj  30746  minvecolem4  30912  lt2addrd  32758  xlt2addrd  32765  fzsplit3  32799  bcm1n  32800  ply1degltel  33580  ply1degltlss  33582  submateqlem1  33753  cnre2csqlem  33856  tpr2rico  33858  dya2ub  34235  dya2icoseg  34242  ballotlemfcc  34458  ballotlemfrcn0  34494  sgnsub  34509  signslema  34539  ftc2re  34575  subfacval3  35157  dnibndlem8  36451  dnibndlem10  36453  dnibndlem11  36454  dnibndlem12  36455  dnicn  36458  knoppcnlem4  36462  unblimceq0  36473  unbdqndv2lem2  36476  knoppndvlem11  36488  knoppndvlem14  36491  knoppndvlem15  36492  knoppndvlem17  36494  knoppndvlem20  36497  irrdifflemf  37291  poimirlem29  37609  broucube  37614  opnmbllem0  37616  mblfinlem3  37619  mblfinlem4  37620  itg2addnclem  37631  itg2addnclem3  37633  itg2gt0cn  37635  ftc1cnnclem  37651  areacirclem1  37668  areacirclem2  37669  areacirclem4  37671  areacirclem5  37672  areacirc  37673  cntotbnd  37756  rrnmet  37789  rrndstprj1  37790  rrndstprj2  37791  lcmineqlem23  42008  intlewftc  42018  aks4d1p1p2  42027  aks4d1p1p4  42028  dvle2  42029  aks4d1p1  42033  primrootlekpowne0  42062  hashscontpow1  42078  aks6d1c2  42087  aks6d1c5lem2  42095  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  aks6d1c6lem3  42129  bcled  42135  bcle2d  42136  unitscyglem2  42153  unitscyglem4  42155  metakunt1  42162  metakunt7  42168  metakunt16  42177  metakunt18  42179  metakunt28  42189  metakunt29  42190  metakunt30  42191  readdrcl2d  42262  frlmvscadiccat  42461  fltnlta  42618  3cubeslem2  42641  3cubeslem4  42645  irrapxlem2  42779  irrapxlem3  42780  irrapxlem4  42781  irrapxlem5  42782  pellexlem2  42786  pellexlem6  42790  pell1qrgaplem  42829  rmspecsqrtnq  42862  rmspecfund  42865  rmspecpos  42873  jm2.24nn  42916  jm2.17c  42919  fzmaxdif  42938  acongeq  42940  modabsdifz  42943  jm3.1lem2  42975  areaquad  43177  sqrtcvallem2  43599  sqrtcvallem3  43600  sqrtcval  43603  imo72b2lem0  44127  cvgdvgrat  44282  hashnzfzclim  44291  binomcxplemdvbinom  44322  oddfl  45192  lefldiveq  45207  fperiodmul  45219  fzdifsuc2  45225  suprltrp  45243  supxrgere  45248  supxrgelem  45252  suplesup  45254  infleinflem2  45286  infleinf  45287  xrralrecnnge  45305  iccshift  45436  iooshift  45440  iooiinicc  45460  fmul01lt1lem2  45506  climinf  45527  sumnnodd  45551  ltmod  45559  lptre2pt  45561  climleltrp  45597  limsupgtlem  45698  liminflimsupclim  45728  fperdvper  45840  dvbdfbdioolem1  45849  dvbdfbdioolem2  45850  dvbdfbdioo  45851  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnmul  45864  iblspltprt  45894  itgspltprt  45900  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  sublevolico  45905  stoweidlem1  45922  stoweidlem11  45932  stoweidlem12  45933  stoweidlem13  45934  stoweidlem14  45935  stoweidlem23  45944  stoweidlem24  45945  stoweidlem25  45946  stoweidlem26  45947  stoweidlem34  45955  stoweidlem40  45961  stoweidlem41  45962  stoweidlem42  45963  stoweidlem45  45966  stoweidlem60  45981  stoweidlem62  45983  wallispilem3  45988  wallispilem4  45989  wallispi  45991  wallispi2lem1  45992  stirlinglem5  45999  stirlinglem11  46005  stirlinglem12  46006  dirkercncflem1  46024  fourierdlem4  46032  fourierdlem6  46034  fourierdlem7  46035  fourierdlem9  46037  fourierdlem13  46041  fourierdlem14  46042  fourierdlem15  46043  fourierdlem19  46047  fourierdlem26  46054  fourierdlem35  46063  fourierdlem39  46067  fourierdlem40  46068  fourierdlem41  46069  fourierdlem42  46070  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem51  46078  fourierdlem56  46083  fourierdlem57  46084  fourierdlem59  46086  fourierdlem60  46087  fourierdlem61  46088  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem66  46093  fourierdlem68  46095  fourierdlem71  46098  fourierdlem72  46099  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem78  46105  fourierdlem79  46106  fourierdlem81  46108  fourierdlem82  46109  fourierdlem83  46110  fourierdlem84  46111  fourierdlem88  46115  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem92  46119  fourierdlem93  46120  fourierdlem95  46122  fourierdlem97  46124  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  fourierdlem109  46136  fourierdlem111  46138  fouriersw  46152  elaa2lem  46154  etransclem23  46178  rrxtopnfi  46208  rrndistlt  46211  ioorrnopnlem  46225  ioorrnopnxrlem  46227  sge0gtfsumgt  46364  iundjiun  46381  volicorecl  46467  hoiprodcl  46468  hoiprodcl3  46501  volicore  46502  hoidmvcl  46503  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoiqssbllem1  46543  hoiqssbllem2  46544  hoiqssbllem3  46545  hspmbllem1  46547  ovolval5lem1  46573  ovolval5lem2  46574  iunhoiioolem  46596  iccvonmbllem  46599  vonicclem1  46604  preimageiingt  46641  salpreimagtge  46646  smfaddlem1  46684  smflimlem4  46695  smfmullem1  46712  smfmullem2  46713  smfmullem3  46714  ltsubsubaddltsub  47216  2elfz2melfz  47233  requad01  47495  requad1  47496  requad2  47497  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  bgoldbtbnd  47683  ply1mulgsumlem2  48116  difmodm1lt  48256  nnpw2pmod  48317  dignn0flhalflem1  48349  affinecomb1  48436  rrxlinesc  48469  rrxlinec  48470  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  rrx2vlinest  48475  rrx2linest2  48478  2sphere  48483  line2  48486  itsclc0lem2  48491  itsclc0lem3  48492  itscnhlc0yqe  48493  itsclc0yqsollem2  48497  itsclc0yqsol  48498  itscnhlc0xyqsol  48499  itsclinecirc0  48507  itsclinecirc0b  48508  itsclinecirc0in  48509  itsclquadb  48510  2itscp  48515  itscnhlinecirc02plem1  48516  itscnhlinecirc02p  48519  inlinecirc02plem  48520  amgmwlem  48896