Theorem resubcld 11565

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7358  ℝcr 11025   − cmin 11364

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-ltxr 11171  df-sub 11366  df-neg 11367

This theorem is referenced by:  ltsubadd  11607  lesubadd  11609  lesub1  11631  lesub2  11632  ltsub1  11633  ltsub2  11634  lt2sub  11635  le2sub  11636  ltmul1a  11990  supaddc  12109  cru  12137  ge2halflem1  13022  qbtwnre  13114  lincmb01cmp  13411  iccf1o  13412  xov1plusxeqvd  13414  intfracq  13779  fldiv  13780  modlt  13800  modsubdir  13863  modsumfzodifsn  13867  serle  13980  expmulnbnd  14158  discr  14163  fzsdom2  14351  cshwidxmod  14726  crre  15037  remullem  15051  01sqrexlem7  15171  absrdbnd  15265  fzomaxdiflem  15266  caubnd2  15281  amgm2  15293  icodiamlt  15361  bhmafibid1  15391  mulcn2  15519  reccn2  15520  rlimo1  15540  climle  15563  climsqz  15564  climsqz2  15565  rlimle  15571  isercolllem1  15588  climsup  15593  caucvgrlem  15596  caucvgrlem2  15598  iseraltlem2  15606  iseraltlem3  15607  iseralt  15608  fsumle  15722  cvgcmp  15739  cvgcmpce  15741  bpoly4  15982  eflt  16042  resinhcl  16081  tanhlt1  16085  sin01bnd  16110  sin01gt0  16115  moddvds  16190  bitscmp  16365  bitsinv1lem  16368  smueqlem  16417  modprm0  16733  pcbc  16828  4sqlem15  16887  blss2ps  24347  blss2  24348  blssps  24368  blss  24369  nm2dif  24569  nlmvscnlem2  24629  nrginvrcnlem  24635  iccntr  24766  icccmplem2  24768  metdstri  24796  cnllycmp  24911  evth  24914  lebnumii  24921  ipcnlem2  25200  cncmet  25278  rrxds  25349  rrxmval  25361  rrxmet  25364  rrxdstprj1  25365  rrxdsfi  25367  ehl1eudis  25376  ehl2eudis  25378  minveclem3b  25384  minveclem4  25388  ivthlem2  25409  ivthlem3  25410  ovollb2lem  25445  ovoliunlem1  25459  ovolscalem1  25470  ovolicc1  25473  ovolicc2lem4  25477  ovolicc2  25479  ovolicc  25480  voliunlem2  25508  ovolioo  25525  ioorcl2  25529  uniioovol  25536  uniioombllem2  25540  uniioombllem3a  25541  uniioombllem3  25542  uniioombllem4  25543  uniioombllem6  25545  opnmbllem  25558  volcn  25563  vitalilem2  25566  ismbf3d  25611  mbfaddlem  25617  i1fadd  25652  itg1addlem4  25656  mbfi1fseqlem6  25677  itg2seq  25699  itg2split  25706  itg2cnlem2  25719  itg2cn  25720  itgrevallem1  25752  dvcjbr  25909  dvferm1lem  25944  dvferm2lem  25946  cmvth  25951  cmvthOLD  25952  mvth  25953  dvlip  25954  dvlip2  25956  c1liplem1  25957  dvgt0  25965  dvlt0  25966  dvge0  25967  dvle  25968  dvivthlem1  25969  lhop1lem  25974  lhop  25977  dvcnvrelem1  25978  dvcnvrelem2  25979  dvcnvre  25980  dvcvx  25981  dvfsumle  25982  dvfsumleOLD  25983  dvfsumge  25984  dvfsumrlimf  25987  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem3  25991  dvfsumlem4  25992  dvfsum2  25997  ftc1a  26000  ftc1lem4  26002  coe1mul3  26060  ply1divex  26098  plydivex  26261  aalioulem2  26297  aalioulem3  26298  aalioulem4  26299  aalioulem5  26300  aalioulem6  26301  aaliou3lem7  26313  taylthlem2  26338  taylthlem2OLD  26339  mtest  26369  pilem2  26418  tangtx  26470  cosordlem  26495  efif1olem2  26508  logcnlem3  26609  logcnlem4  26610  isosctrlem2  26785  chordthmlem2  26799  chordthmlem4  26801  heron  26804  atanlogsublem  26881  atantan  26889  birthdaylem3  26919  logdifbnd  26960  emcllem1  26962  emcllem2  26963  emcllem5  26966  emcllem6  26967  harmonicbnd4  26977  fsumharmonic  26978  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamucov  27004  relgamcl  27028  ftalem2  27040  ftalem5  27043  chpub  27187  logfaclbnd  27189  logfacbnd3  27190  logexprlim  27192  bposlem1  27251  bposlem9  27259  gausslemma2dlem1a  27332  lgseisenlem1  27342  lgsquadlem1  27347  2sqmod  27403  chtppilimlem1  27440  vmadivsum  27449  vmadivsumb  27450  rplogsumlem1  27451  rplogsumlem2  27452  rpvmasumlem  27454  dchrisumlem2  27457  dchrisum0re  27480  rplogsum  27494  mulogsumlem  27498  mulog2sumlem1  27501  vmalogdivsum2  27505  vmalogdivsum  27506  2vmadivsumlem  27507  log2sumbnd  27511  selbergb  27516  selberg2lem  27517  selberg2b  27519  chpdifbndlem1  27520  selberg3lem1  27524  selberg3lem2  27525  selberg3  27526  selberg4lem1  27527  selberg4  27528  pntrf  27530  pntrmax  27531  pntrsumo1  27532  selberg3r  27536  selberg4r  27537  selberg34r  27538  pntrlog2bndlem1  27544  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntrlog2bnd  27551  pntpbnd1a  27552  pntpbnd2  27554  pntibndlem2  27558  pntlemg  27565  pntlemn  27567  pntlemj  27570  pntlemf  27572  pntlemo  27574  pntlem3  27576  pntleml  27578  ttgcontlem1  28957  eqeelen  28977  brbtwn2  28978  colinearalg  28983  axcgrid  28989  axsegconlem1  28990  axsegconlem3  28992  axsegconlem8  28997  axsegconlem9  28998  axsegconlem10  28999  ax5seglem3a  29003  ax5seg  29011  axpaschlem  29013  axcontlem8  29044  nbusgrvtxm1  29452  crctcshwlkn0lem3  29885  crctcshwlkn0lem5  29887  crctcsh  29897  clwlkclwwlklem2fv2  30071  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  nvabs  30747  dipcj  30789  minvecolem4  30955  lt2addrd  32830  xlt2addrd  32839  fzsplit3  32873  bcm1n  32875  sgnsub  32918  ply1degltel  33675  ply1degltlss  33677  iconstr  33923  constrresqrtcl  33934  cos9thpiminplylem1  33939  submateqlem1  33964  cnre2csqlem  34067  tpr2rico  34069  dya2ub  34427  dya2icoseg  34434  ballotlemfcc  34651  ballotlemfrcn0  34687  signslema  34719  ftc2re  34755  subfacval3  35383  dnibndlem8  36685  dnibndlem10  36687  dnibndlem11  36688  dnibndlem12  36689  dnicn  36692  knoppcnlem4  36696  unblimceq0  36707  unbdqndv2lem2  36710  knoppndvlem11  36722  knoppndvlem14  36725  knoppndvlem15  36726  knoppndvlem17  36728  knoppndvlem20  36731  irrdifflemf  37526  poimirlem29  37846  broucube  37851  opnmbllem0  37853  mblfinlem3  37856  mblfinlem4  37857  itg2addnclem  37868  itg2addnclem3  37870  itg2gt0cn  37872  ftc1cnnclem  37888  areacirclem1  37905  areacirclem2  37906  areacirclem4  37908  areacirclem5  37909  areacirc  37910  cntotbnd  37993  rrnmet  38026  rrndstprj1  38027  rrndstprj2  38028  lcmineqlem23  42301  intlewftc  42311  aks4d1p1p2  42320  aks4d1p1p4  42321  dvle2  42322  aks4d1p1  42326  primrootlekpowne0  42355  hashscontpow1  42371  aks6d1c2  42380  aks6d1c5lem2  42388  sticksstones10  42405  sticksstones12a  42407  sticksstones12  42408  aks6d1c6lem3  42422  bcled  42428  bcle2d  42429  unitscyglem2  42446  unitscyglem4  42448  readdrcl2d  42524  frlmvscadiccat  42757  fltnlta  42902  3cubeslem2  42923  3cubeslem4  42927  irrapxlem2  43061  irrapxlem3  43062  irrapxlem4  43063  irrapxlem5  43064  pellexlem2  43068  pellexlem6  43072  pell1qrgaplem  43111  rmspecsqrtnq  43144  rmspecfund  43147  rmspecpos  43154  jm2.24nn  43197  jm2.17c  43200  fzmaxdif  43219  acongeq  43221  modabsdifz  43224  jm3.1lem2  43256  areaquad  43454  sqrtcvallem2  43874  sqrtcvallem3  43875  sqrtcval  43878  imo72b2lem0  44402  cvgdvgrat  44550  hashnzfzclim  44559  binomcxplemdvbinom  44590  oddfl  45522  lefldiveq  45536  fperiodmul  45548  fzdifsuc2  45554  suprltrp  45569  supxrgere  45574  supxrgelem  45578  suplesup  45580  infleinflem2  45611  infleinf  45612  xrralrecnnge  45630  iccshift  45760  iooshift  45764  iooiinicc  45784  fmul01lt1lem2  45827  climinf  45848  sumnnodd  45872  ltmod  45878  lptre2pt  45880  climleltrp  45916  limsupgtlem  46017  liminflimsupclim  46047  fperdvper  46159  dvbdfbdioolem1  46168  dvbdfbdioolem2  46169  dvbdfbdioo  46170  ioodvbdlimc1lem1  46171  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvnmul  46183  iblspltprt  46213  itgspltprt  46219  itgiccshift  46220  itgperiod  46221  itgsbtaddcnst  46222  sublevolico  46224  stoweidlem1  46241  stoweidlem11  46251  stoweidlem12  46252  stoweidlem13  46253  stoweidlem14  46254  stoweidlem23  46263  stoweidlem24  46264  stoweidlem25  46265  stoweidlem26  46266  stoweidlem34  46274  stoweidlem40  46280  stoweidlem41  46281  stoweidlem42  46282  stoweidlem45  46285  stoweidlem60  46300  stoweidlem62  46302  wallispilem3  46307  wallispilem4  46308  wallispi  46310  wallispi2lem1  46311  stirlinglem5  46318  stirlinglem11  46324  stirlinglem12  46325  dirkercncflem1  46343  fourierdlem4  46351  fourierdlem6  46353  fourierdlem7  46354  fourierdlem9  46356  fourierdlem13  46360  fourierdlem14  46361  fourierdlem15  46362  fourierdlem19  46366  fourierdlem26  46373  fourierdlem35  46382  fourierdlem39  46386  fourierdlem40  46387  fourierdlem41  46388  fourierdlem42  46389  fourierdlem48  46394  fourierdlem49  46395  fourierdlem50  46396  fourierdlem51  46397  fourierdlem56  46402  fourierdlem57  46403  fourierdlem59  46405  fourierdlem60  46406  fourierdlem61  46407  fourierdlem63  46409  fourierdlem64  46410  fourierdlem65  46411  fourierdlem66  46412  fourierdlem68  46414  fourierdlem71  46417  fourierdlem72  46418  fourierdlem73  46419  fourierdlem74  46420  fourierdlem75  46421  fourierdlem76  46422  fourierdlem78  46424  fourierdlem79  46425  fourierdlem81  46427  fourierdlem82  46428  fourierdlem83  46429  fourierdlem84  46430  fourierdlem88  46434  fourierdlem89  46435  fourierdlem90  46436  fourierdlem91  46437  fourierdlem92  46438  fourierdlem93  46439  fourierdlem95  46441  fourierdlem97  46443  fourierdlem101  46447  fourierdlem103  46449  fourierdlem104  46450  fourierdlem107  46453  fourierdlem109  46455  fourierdlem111  46457  fouriersw  46471  elaa2lem  46473  etransclem23  46497  rrxtopnfi  46527  rrndistlt  46530  ioorrnopnlem  46544  ioorrnopnxrlem  46546  sge0gtfsumgt  46683  iundjiun  46700  volicorecl  46786  hoiprodcl  46787  hoiprodcl3  46820  volicore  46821  hoidmvcl  46822  hoidmv1lelem2  46832  hoidmv1lelem3  46833  hoidmv1le  46834  hoidmvlelem1  46835  hoidmvlelem2  46836  hoiqssbllem1  46862  hoiqssbllem2  46863  hoiqssbllem3  46864  hspmbllem1  46866  ovolval5lem1  46892  ovolval5lem2  46893  iunhoiioolem  46915  iccvonmbllem  46918  vonicclem1  46923  preimageiingt  46960  salpreimagtge  46965  smfaddlem1  47003  smflimlem4  47014  smfmullem1  47031  smfmullem2  47032  smfmullem3  47033  ltsubsubaddltsub  47543  2elfz2melfz  47560  2tceilhalfelfzo1  47574  requad01  47863  requad1  47864  requad2  47865  bgoldbtbndlem2  48048  bgoldbtbndlem3  48049  bgoldbtbndlem4  48050  bgoldbtbnd  48051  gpgedgvtx0  48303  gpgedgvtx1  48304  gpg5nbgrvtx03starlem2  48311  gpg5nbgrvtx13starlem2  48314  ply1mulgsumlem2  48629  nnpw2pmod  48825  dignn0flhalflem1  48857  affinecomb1  48944  rrxlinesc  48977  rrxlinec  48978  eenglngeehlnmlem1  48979  eenglngeehlnmlem2  48980  rrx2vlinest  48983  rrx2linest2  48986  2sphere  48991  line2  48994  itsclc0lem2  48999  itsclc0lem3  49000  itscnhlc0yqe  49001  itsclc0yqsollem2  49005  itsclc0yqsol  49006  itscnhlc0xyqsol  49007  itsclinecirc0  49015  itsclinecirc0b  49016  itsclinecirc0in  49017  itsclquadb  49018  2itscp  49023  itscnhlinecirc02plem1  49024  itscnhlinecirc02p  49027  inlinecirc02plem  49028  amgmwlem  50043