Theorem resubcld 11545

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

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7346  ℝcr 11005   − cmin 11344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-ltxr 11151  df-sub 11346  df-neg 11347

This theorem is referenced by:  ltsubadd  11587  lesubadd  11589  lesub1  11611  lesub2  11612  ltsub1  11613  ltsub2  11614  lt2sub  11615  le2sub  11616  ltmul1a  11970  supaddc  12089  cru  12117  ge2halflem1  13007  qbtwnre  13098  lincmb01cmp  13395  iccf1o  13396  xov1plusxeqvd  13398  intfracq  13763  fldiv  13764  modlt  13784  modsubdir  13847  modsumfzodifsn  13851  serle  13964  expmulnbnd  14142  discr  14147  fzsdom2  14335  cshwidxmod  14710  crre  15021  remullem  15035  01sqrexlem7  15155  absrdbnd  15249  fzomaxdiflem  15250  caubnd2  15265  amgm2  15277  icodiamlt  15345  bhmafibid1  15375  mulcn2  15503  reccn2  15504  rlimo1  15524  climle  15547  climsqz  15548  climsqz2  15549  rlimle  15555  isercolllem1  15572  climsup  15577  caucvgrlem  15580  caucvgrlem2  15582  iseraltlem2  15590  iseraltlem3  15591  iseralt  15592  fsumle  15706  cvgcmp  15723  cvgcmpce  15725  bpoly4  15966  eflt  16026  resinhcl  16065  tanhlt1  16069  sin01bnd  16094  sin01gt0  16099  moddvds  16174  bitscmp  16349  bitsinv1lem  16352  smueqlem  16401  modprm0  16717  pcbc  16812  4sqlem15  16871  blss2ps  24318  blss2  24319  blssps  24339  blss  24340  nm2dif  24540  nlmvscnlem2  24600  nrginvrcnlem  24606  iccntr  24737  icccmplem2  24739  metdstri  24767  cnllycmp  24882  evth  24885  lebnumii  24892  ipcnlem2  25171  cncmet  25249  rrxds  25320  rrxmval  25332  rrxmet  25335  rrxdstprj1  25336  rrxdsfi  25338  ehl1eudis  25347  ehl2eudis  25349  minveclem3b  25355  minveclem4  25359  ivthlem2  25380  ivthlem3  25381  ovollb2lem  25416  ovoliunlem1  25430  ovolscalem1  25441  ovolicc1  25444  ovolicc2lem4  25448  ovolicc2  25450  ovolicc  25451  voliunlem2  25479  ovolioo  25496  ioorcl2  25500  uniioovol  25507  uniioombllem2  25511  uniioombllem3a  25512  uniioombllem3  25513  uniioombllem4  25514  uniioombllem6  25516  opnmbllem  25529  volcn  25534  vitalilem2  25537  ismbf3d  25582  mbfaddlem  25588  i1fadd  25623  itg1addlem4  25627  mbfi1fseqlem6  25648  itg2seq  25670  itg2split  25677  itg2cnlem2  25690  itg2cn  25691  itgrevallem1  25723  dvcjbr  25880  dvferm1lem  25915  dvferm2lem  25917  cmvth  25922  cmvthOLD  25923  mvth  25924  dvlip  25925  dvlip2  25927  c1liplem1  25928  dvgt0  25936  dvlt0  25937  dvge0  25938  dvle  25939  dvivthlem1  25940  lhop1lem  25945  lhop  25948  dvcnvrelem1  25949  dvcnvrelem2  25950  dvcnvre  25951  dvcvx  25952  dvfsumle  25953  dvfsumleOLD  25954  dvfsumge  25955  dvfsumrlimf  25958  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem3  25962  dvfsumlem4  25963  dvfsum2  25968  ftc1a  25971  ftc1lem4  25973  coe1mul3  26031  ply1divex  26069  plydivex  26232  aalioulem2  26268  aalioulem3  26269  aalioulem4  26270  aalioulem5  26271  aalioulem6  26272  aaliou3lem7  26284  taylthlem2  26309  taylthlem2OLD  26310  mtest  26340  pilem2  26389  tangtx  26441  cosordlem  26466  efif1olem2  26479  logcnlem3  26580  logcnlem4  26581  isosctrlem2  26756  chordthmlem2  26770  chordthmlem4  26772  heron  26775  atanlogsublem  26852  atantan  26860  birthdaylem3  26890  logdifbnd  26931  emcllem1  26933  emcllem2  26934  emcllem5  26937  emcllem6  26938  harmonicbnd4  26948  fsumharmonic  26949  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamucov  26975  relgamcl  26999  ftalem2  27011  ftalem5  27014  chpub  27158  logfaclbnd  27160  logfacbnd3  27161  logexprlim  27163  bposlem1  27222  bposlem9  27230  gausslemma2dlem1a  27303  lgseisenlem1  27313  lgsquadlem1  27318  2sqmod  27374  chtppilimlem1  27411  vmadivsum  27420  vmadivsumb  27421  rplogsumlem1  27422  rplogsumlem2  27423  rpvmasumlem  27425  dchrisumlem2  27428  dchrisum0re  27451  rplogsum  27465  mulogsumlem  27469  mulog2sumlem1  27472  vmalogdivsum2  27476  vmalogdivsum  27477  2vmadivsumlem  27478  log2sumbnd  27482  selbergb  27487  selberg2lem  27488  selberg2b  27490  chpdifbndlem1  27491  selberg3lem1  27495  selberg3lem2  27496  selberg3  27497  selberg4lem1  27498  selberg4  27499  pntrf  27501  pntrmax  27502  pntrsumo1  27503  selberg3r  27507  selberg4r  27508  selberg34r  27509  pntrlog2bndlem1  27515  pntrlog2bndlem2  27516  pntrlog2bndlem3  27517  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntrlog2bndlem6  27521  pntrlog2bnd  27522  pntpbnd1a  27523  pntpbnd2  27525  pntibndlem2  27529  pntlemg  27536  pntlemn  27538  pntlemj  27541  pntlemf  27543  pntlemo  27545  pntlem3  27547  pntleml  27549  ttgcontlem1  28863  eqeelen  28882  brbtwn2  28883  colinearalg  28888  axcgrid  28894  axsegconlem1  28895  axsegconlem3  28897  axsegconlem8  28902  axsegconlem9  28903  axsegconlem10  28904  ax5seglem3a  28908  ax5seg  28916  axpaschlem  28918  axcontlem8  28949  nbusgrvtxm1  29357  crctcshwlkn0lem3  29790  crctcshwlkn0lem5  29792  crctcsh  29802  clwlkclwwlklem2fv2  29976  clwlkclwwlklem2a4  29977  clwlkclwwlklem2a  29978  nvabs  30652  dipcj  30694  minvecolem4  30860  lt2addrd  32734  xlt2addrd  32742  fzsplit3  32776  bcm1n  32777  sgnsub  32820  ply1degltel  33555  ply1degltlss  33557  iconstr  33779  constrresqrtcl  33790  cos9thpiminplylem1  33795  submateqlem1  33820  cnre2csqlem  33923  tpr2rico  33925  dya2ub  34283  dya2icoseg  34290  ballotlemfcc  34507  ballotlemfrcn0  34543  signslema  34575  ftc2re  34611  subfacval3  35233  dnibndlem8  36529  dnibndlem10  36531  dnibndlem11  36532  dnibndlem12  36533  dnicn  36536  knoppcnlem4  36540  unblimceq0  36551  unbdqndv2lem2  36554  knoppndvlem11  36566  knoppndvlem14  36569  knoppndvlem15  36570  knoppndvlem17  36572  knoppndvlem20  36575  irrdifflemf  37369  poimirlem29  37699  broucube  37704  opnmbllem0  37706  mblfinlem3  37709  mblfinlem4  37710  itg2addnclem  37721  itg2addnclem3  37723  itg2gt0cn  37725  ftc1cnnclem  37741  areacirclem1  37758  areacirclem2  37759  areacirclem4  37761  areacirclem5  37762  areacirc  37763  cntotbnd  37846  rrnmet  37879  rrndstprj1  37880  rrndstprj2  37881  lcmineqlem23  42154  intlewftc  42164  aks4d1p1p2  42173  aks4d1p1p4  42174  dvle2  42175  aks4d1p1  42179  primrootlekpowne0  42208  hashscontpow1  42224  aks6d1c2  42233  aks6d1c5lem2  42241  sticksstones10  42258  sticksstones12a  42260  sticksstones12  42261  aks6d1c6lem3  42275  bcled  42281  bcle2d  42282  unitscyglem2  42299  unitscyglem4  42301  readdrcl2d  42376  frlmvscadiccat  42609  fltnlta  42766  3cubeslem2  42788  3cubeslem4  42792  irrapxlem2  42926  irrapxlem3  42927  irrapxlem4  42928  irrapxlem5  42929  pellexlem2  42933  pellexlem6  42937  pell1qrgaplem  42976  rmspecsqrtnq  43009  rmspecfund  43012  rmspecpos  43019  jm2.24nn  43062  jm2.17c  43065  fzmaxdif  43084  acongeq  43086  modabsdifz  43089  jm3.1lem2  43121  areaquad  43319  sqrtcvallem2  43740  sqrtcvallem3  43741  sqrtcval  43744  imo72b2lem0  44268  cvgdvgrat  44416  hashnzfzclim  44425  binomcxplemdvbinom  44456  oddfl  45389  lefldiveq  45403  fperiodmul  45415  fzdifsuc2  45421  suprltrp  45437  supxrgere  45442  supxrgelem  45446  suplesup  45448  infleinflem2  45479  infleinf  45480  xrralrecnnge  45498  iccshift  45628  iooshift  45632  iooiinicc  45652  fmul01lt1lem2  45695  climinf  45716  sumnnodd  45740  ltmod  45746  lptre2pt  45748  climleltrp  45784  limsupgtlem  45885  liminflimsupclim  45915  fperdvper  46027  dvbdfbdioolem1  46036  dvbdfbdioolem2  46037  dvbdfbdioo  46038  ioodvbdlimc1lem1  46039  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  dvnmul  46051  iblspltprt  46081  itgspltprt  46087  itgiccshift  46088  itgperiod  46089  itgsbtaddcnst  46090  sublevolico  46092  stoweidlem1  46109  stoweidlem11  46119  stoweidlem12  46120  stoweidlem13  46121  stoweidlem14  46122  stoweidlem23  46131  stoweidlem24  46132  stoweidlem25  46133  stoweidlem26  46134  stoweidlem34  46142  stoweidlem40  46148  stoweidlem41  46149  stoweidlem42  46150  stoweidlem45  46153  stoweidlem60  46168  stoweidlem62  46170  wallispilem3  46175  wallispilem4  46176  wallispi  46178  wallispi2lem1  46179  stirlinglem5  46186  stirlinglem11  46192  stirlinglem12  46193  dirkercncflem1  46211  fourierdlem4  46219  fourierdlem6  46221  fourierdlem7  46222  fourierdlem9  46224  fourierdlem13  46228  fourierdlem14  46229  fourierdlem15  46230  fourierdlem19  46234  fourierdlem26  46241  fourierdlem35  46250  fourierdlem39  46254  fourierdlem40  46255  fourierdlem41  46256  fourierdlem42  46257  fourierdlem48  46262  fourierdlem49  46263  fourierdlem50  46264  fourierdlem51  46265  fourierdlem56  46270  fourierdlem57  46271  fourierdlem59  46273  fourierdlem60  46274  fourierdlem61  46275  fourierdlem63  46277  fourierdlem64  46278  fourierdlem65  46279  fourierdlem66  46280  fourierdlem68  46282  fourierdlem71  46285  fourierdlem72  46286  fourierdlem73  46287  fourierdlem74  46288  fourierdlem75  46289  fourierdlem76  46290  fourierdlem78  46292  fourierdlem79  46293  fourierdlem81  46295  fourierdlem82  46296  fourierdlem83  46297  fourierdlem84  46298  fourierdlem88  46302  fourierdlem89  46303  fourierdlem90  46304  fourierdlem91  46305  fourierdlem92  46306  fourierdlem93  46307  fourierdlem95  46309  fourierdlem97  46311  fourierdlem101  46315  fourierdlem103  46317  fourierdlem104  46318  fourierdlem107  46321  fourierdlem109  46323  fourierdlem111  46325  fouriersw  46339  elaa2lem  46341  etransclem23  46365  rrxtopnfi  46395  rrndistlt  46398  ioorrnopnlem  46412  ioorrnopnxrlem  46414  sge0gtfsumgt  46551  iundjiun  46568  volicorecl  46654  hoiprodcl  46655  hoiprodcl3  46688  volicore  46689  hoidmvcl  46690  hoidmv1lelem2  46700  hoidmv1lelem3  46701  hoidmv1le  46702  hoidmvlelem1  46703  hoidmvlelem2  46704  hoiqssbllem1  46730  hoiqssbllem2  46731  hoiqssbllem3  46732  hspmbllem1  46734  ovolval5lem1  46760  ovolval5lem2  46761  iunhoiioolem  46783  iccvonmbllem  46786  vonicclem1  46791  preimageiingt  46828  salpreimagtge  46833  smfaddlem1  46871  smflimlem4  46882  smfmullem1  46899  smfmullem2  46900  smfmullem3  46901  ltsubsubaddltsub  47411  2elfz2melfz  47428  2tceilhalfelfzo1  47442  requad01  47731  requad1  47732  requad2  47733  bgoldbtbndlem2  47916  bgoldbtbndlem3  47917  bgoldbtbndlem4  47918  bgoldbtbnd  47919  gpgedgvtx0  48171  gpgedgvtx1  48172  gpg5nbgrvtx03starlem2  48179  gpg5nbgrvtx13starlem2  48182  ply1mulgsumlem2  48498  nnpw2pmod  48694  dignn0flhalflem1  48726  affinecomb1  48813  rrxlinesc  48846  rrxlinec  48847  eenglngeehlnmlem1  48848  eenglngeehlnmlem2  48849  rrx2vlinest  48852  rrx2linest2  48855  2sphere  48860  line2  48863  itsclc0lem2  48868  itsclc0lem3  48869  itscnhlc0yqe  48870  itsclc0yqsollem2  48874  itsclc0yqsol  48875  itscnhlc0xyqsol  48876  itsclinecirc0  48884  itsclinecirc0b  48885  itsclinecirc0in  48886  itsclquadb  48887  2itscp  48892  itscnhlinecirc02plem1  48893  itscnhlinecirc02p  48896  inlinecirc02plem  48897  amgmwlem  49913