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  37530  poimirlem29  37850  broucube  37855  opnmbllem0  37857  mblfinlem3  37860  mblfinlem4  37861  itg2addnclem  37872  itg2addnclem3  37874  itg2gt0cn  37876  ftc1cnnclem  37892  areacirclem1  37909  areacirclem2  37910  areacirclem4  37912  areacirclem5  37913  areacirc  37914  cntotbnd  37997  rrnmet  38030  rrndstprj1  38031  rrndstprj2  38032  lcmineqlem23  42315  intlewftc  42325  aks4d1p1p2  42334  aks4d1p1p4  42335  dvle2  42336  aks4d1p1  42340  primrootlekpowne0  42369  hashscontpow1  42385  aks6d1c2  42394  aks6d1c5lem2  42402  sticksstones10  42419  sticksstones12a  42421  sticksstones12  42422  aks6d1c6lem3  42436  bcled  42442  bcle2d  42443  unitscyglem2  42460  unitscyglem4  42462  readdrcl2d  42538  frlmvscadiccat  42771  fltnlta  42916  3cubeslem2  42937  3cubeslem4  42941  irrapxlem2  43075  irrapxlem3  43076  irrapxlem4  43077  irrapxlem5  43078  pellexlem2  43082  pellexlem6  43086  pell1qrgaplem  43125  rmspecsqrtnq  43158  rmspecfund  43161  rmspecpos  43168  jm2.24nn  43211  jm2.17c  43214  fzmaxdif  43233  acongeq  43235  modabsdifz  43238  jm3.1lem2  43270  areaquad  43468  sqrtcvallem2  43888  sqrtcvallem3  43889  sqrtcval  43892  imo72b2lem0  44416  cvgdvgrat  44564  hashnzfzclim  44573  binomcxplemdvbinom  44604  oddfl  45536  lefldiveq  45550  fperiodmul  45562  fzdifsuc2  45568  suprltrp  45583  supxrgere  45588  supxrgelem  45592  suplesup  45594  infleinflem2  45625  infleinf  45626  xrralrecnnge  45644  iccshift  45774  iooshift  45778  iooiinicc  45798  fmul01lt1lem2  45841  climinf  45862  sumnnodd  45886  ltmod  45892  lptre2pt  45894  climleltrp  45930  limsupgtlem  46031  liminflimsupclim  46061  fperdvper  46173  dvbdfbdioolem1  46182  dvbdfbdioolem2  46183  dvbdfbdioo  46184  ioodvbdlimc1lem1  46185  ioodvbdlimc1lem2  46186  ioodvbdlimc2lem  46188  dvnmul  46197  iblspltprt  46227  itgspltprt  46233  itgiccshift  46234  itgperiod  46235  itgsbtaddcnst  46236  sublevolico  46238  stoweidlem1  46255  stoweidlem11  46265  stoweidlem12  46266  stoweidlem13  46267  stoweidlem14  46268  stoweidlem23  46277  stoweidlem24  46278  stoweidlem25  46279  stoweidlem26  46280  stoweidlem34  46288  stoweidlem40  46294  stoweidlem41  46295  stoweidlem42  46296  stoweidlem45  46299  stoweidlem60  46314  stoweidlem62  46316  wallispilem3  46321  wallispilem4  46322  wallispi  46324  wallispi2lem1  46325  stirlinglem5  46332  stirlinglem11  46338  stirlinglem12  46339  dirkercncflem1  46357  fourierdlem4  46365  fourierdlem6  46367  fourierdlem7  46368  fourierdlem9  46370  fourierdlem13  46374  fourierdlem14  46375  fourierdlem15  46376  fourierdlem19  46380  fourierdlem26  46387  fourierdlem35  46396  fourierdlem39  46400  fourierdlem40  46401  fourierdlem41  46402  fourierdlem42  46403  fourierdlem48  46408  fourierdlem49  46409  fourierdlem50  46410  fourierdlem51  46411  fourierdlem56  46416  fourierdlem57  46417  fourierdlem59  46419  fourierdlem60  46420  fourierdlem61  46421  fourierdlem63  46423  fourierdlem64  46424  fourierdlem65  46425  fourierdlem66  46426  fourierdlem68  46428  fourierdlem71  46431  fourierdlem72  46432  fourierdlem73  46433  fourierdlem74  46434  fourierdlem75  46435  fourierdlem76  46436  fourierdlem78  46438  fourierdlem79  46439  fourierdlem81  46441  fourierdlem82  46442  fourierdlem83  46443  fourierdlem84  46444  fourierdlem88  46448  fourierdlem89  46449  fourierdlem90  46450  fourierdlem91  46451  fourierdlem92  46452  fourierdlem93  46453  fourierdlem95  46455  fourierdlem97  46457  fourierdlem101  46461  fourierdlem103  46463  fourierdlem104  46464  fourierdlem107  46467  fourierdlem109  46469  fourierdlem111  46471  fouriersw  46485  elaa2lem  46487  etransclem23  46511  rrxtopnfi  46541  rrndistlt  46544  ioorrnopnlem  46558  ioorrnopnxrlem  46560  sge0gtfsumgt  46697  iundjiun  46714  volicorecl  46800  hoiprodcl  46801  hoiprodcl3  46834  volicore  46835  hoidmvcl  46836  hoidmv1lelem2  46846  hoidmv1lelem3  46847  hoidmv1le  46848  hoidmvlelem1  46849  hoidmvlelem2  46850  hoiqssbllem1  46876  hoiqssbllem2  46877  hoiqssbllem3  46878  hspmbllem1  46880  ovolval5lem1  46906  ovolval5lem2  46907  iunhoiioolem  46929  iccvonmbllem  46932  vonicclem1  46937  preimageiingt  46974  salpreimagtge  46979  smfaddlem1  47017  smflimlem4  47028  smfmullem1  47045  smfmullem2  47046  smfmullem3  47047  ltsubsubaddltsub  47557  2elfz2melfz  47574  2tceilhalfelfzo1  47588  requad01  47877  requad1  47878  requad2  47879  bgoldbtbndlem2  48062  bgoldbtbndlem3  48063  bgoldbtbndlem4  48064  bgoldbtbnd  48065  gpgedgvtx0  48317  gpgedgvtx1  48318  gpg5nbgrvtx03starlem2  48325  gpg5nbgrvtx13starlem2  48328  ply1mulgsumlem2  48643  nnpw2pmod  48839  dignn0flhalflem1  48871  affinecomb1  48958  rrxlinesc  48991  rrxlinec  48992  eenglngeehlnmlem1  48993  eenglngeehlnmlem2  48994  rrx2vlinest  48997  rrx2linest2  49000  2sphere  49005  line2  49008  itsclc0lem2  49013  itsclc0lem3  49014  itscnhlc0yqe  49015  itsclc0yqsollem2  49019  itsclc0yqsol  49020  itscnhlc0xyqsol  49021  itsclinecirc0  49029  itsclinecirc0b  49030  itsclinecirc0in  49031  itsclquadb  49032  2itscp  49037  itscnhlinecirc02plem1  49038  itscnhlinecirc02p  49041  inlinecirc02plem  49042  amgmwlem  50057