Theorem resubcld 11577

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7368  ℝcr 11037   − cmin 11376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183  df-sub 11378  df-neg 11379

This theorem is referenced by:  ltsubadd  11619  lesubadd  11621  lesub1  11643  lesub2  11644  ltsub1  11645  ltsub2  11646  lt2sub  11647  le2sub  11648  ltmul1a  12002  supaddc  12121  cru  12149  ge2halflem1  13034  qbtwnre  13126  lincmb01cmp  13423  iccf1o  13424  xov1plusxeqvd  13426  intfracq  13791  fldiv  13792  modlt  13812  modsubdir  13875  modsumfzodifsn  13879  serle  13992  expmulnbnd  14170  discr  14175  fzsdom2  14363  cshwidxmod  14738  crre  15049  remullem  15063  01sqrexlem7  15183  absrdbnd  15277  fzomaxdiflem  15278  caubnd2  15293  amgm2  15305  icodiamlt  15373  bhmafibid1  15403  mulcn2  15531  reccn2  15532  rlimo1  15552  climle  15575  climsqz  15576  climsqz2  15577  rlimle  15583  isercolllem1  15600  climsup  15605  caucvgrlem  15608  caucvgrlem2  15610  iseraltlem2  15618  iseraltlem3  15619  iseralt  15620  fsumle  15734  cvgcmp  15751  cvgcmpce  15753  bpoly4  15994  eflt  16054  resinhcl  16093  tanhlt1  16097  sin01bnd  16122  sin01gt0  16127  moddvds  16202  bitscmp  16377  bitsinv1lem  16380  smueqlem  16429  modprm0  16745  pcbc  16840  4sqlem15  16899  blss2ps  24359  blss2  24360  blssps  24380  blss  24381  nm2dif  24581  nlmvscnlem2  24641  nrginvrcnlem  24647  iccntr  24778  icccmplem2  24780  metdstri  24808  cnllycmp  24923  evth  24926  lebnumii  24933  ipcnlem2  25212  cncmet  25290  rrxds  25361  rrxmval  25373  rrxmet  25376  rrxdstprj1  25377  rrxdsfi  25379  ehl1eudis  25388  ehl2eudis  25390  minveclem3b  25396  minveclem4  25400  ivthlem2  25421  ivthlem3  25422  ovollb2lem  25457  ovoliunlem1  25471  ovolscalem1  25482  ovolicc1  25485  ovolicc2lem4  25489  ovolicc2  25491  ovolicc  25492  voliunlem2  25520  ovolioo  25537  ioorcl2  25541  uniioovol  25548  uniioombllem2  25552  uniioombllem3a  25553  uniioombllem3  25554  uniioombllem4  25555  uniioombllem6  25557  opnmbllem  25570  volcn  25575  vitalilem2  25578  ismbf3d  25623  mbfaddlem  25629  i1fadd  25664  itg1addlem4  25668  mbfi1fseqlem6  25689  itg2seq  25711  itg2split  25718  itg2cnlem2  25731  itg2cn  25732  itgrevallem1  25764  dvcjbr  25921  dvferm1lem  25956  dvferm2lem  25958  cmvth  25963  cmvthOLD  25964  mvth  25965  dvlip  25966  dvlip2  25968  c1liplem1  25969  dvgt0  25977  dvlt0  25978  dvge0  25979  dvle  25980  dvivthlem1  25981  lhop1lem  25986  lhop  25989  dvcnvrelem1  25990  dvcnvrelem2  25991  dvcnvre  25992  dvcvx  25993  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvfsumrlimf  25999  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumlem3  26003  dvfsumlem4  26004  dvfsum2  26009  ftc1a  26012  ftc1lem4  26014  coe1mul3  26072  ply1divex  26110  plydivex  26273  aalioulem2  26309  aalioulem3  26310  aalioulem4  26311  aalioulem5  26312  aalioulem6  26313  aaliou3lem7  26325  taylthlem2  26350  taylthlem2OLD  26351  mtest  26381  pilem2  26430  tangtx  26482  cosordlem  26507  efif1olem2  26520  logcnlem3  26621  logcnlem4  26622  isosctrlem2  26797  chordthmlem2  26811  chordthmlem4  26813  heron  26816  atanlogsublem  26893  atantan  26901  birthdaylem3  26931  logdifbnd  26972  emcllem1  26974  emcllem2  26975  emcllem5  26978  emcllem6  26979  harmonicbnd4  26989  fsumharmonic  26990  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamucov  27016  relgamcl  27040  ftalem2  27052  ftalem5  27055  chpub  27199  logfaclbnd  27201  logfacbnd3  27202  logexprlim  27204  bposlem1  27263  bposlem9  27271  gausslemma2dlem1a  27344  lgseisenlem1  27354  lgsquadlem1  27359  2sqmod  27415  chtppilimlem1  27452  vmadivsum  27461  vmadivsumb  27462  rplogsumlem1  27463  rplogsumlem2  27464  rpvmasumlem  27466  dchrisumlem2  27469  dchrisum0re  27492  rplogsum  27506  mulogsumlem  27510  mulog2sumlem1  27513  vmalogdivsum2  27517  vmalogdivsum  27518  2vmadivsumlem  27519  log2sumbnd  27523  selbergb  27528  selberg2lem  27529  selberg2b  27531  chpdifbndlem1  27532  selberg3lem1  27536  selberg3lem2  27537  selberg3  27538  selberg4lem1  27539  selberg4  27540  pntrf  27542  pntrmax  27543  pntrsumo1  27544  selberg3r  27548  selberg4r  27549  selberg34r  27550  pntrlog2bndlem1  27556  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntrlog2bnd  27563  pntpbnd1a  27564  pntpbnd2  27566  pntibndlem2  27570  pntlemg  27577  pntlemn  27579  pntlemj  27582  pntlemf  27584  pntlemo  27586  pntlem3  27588  pntleml  27590  ttgcontlem1  28969  eqeelen  28989  brbtwn2  28990  colinearalg  28995  axcgrid  29001  axsegconlem1  29002  axsegconlem3  29004  axsegconlem8  29009  axsegconlem9  29010  axsegconlem10  29011  ax5seglem3a  29015  ax5seg  29023  axpaschlem  29025  axcontlem8  29056  nbusgrvtxm1  29464  crctcshwlkn0lem3  29897  crctcshwlkn0lem5  29899  crctcsh  29909  clwlkclwwlklem2fv2  30083  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  nvabs  30760  dipcj  30802  minvecolem4  30968  lt2addrd  32841  xlt2addrd  32850  fzsplit3  32884  bcm1n  32886  sgnsub  32929  ply1degltel  33687  ply1degltlss  33689  iconstr  33944  constrresqrtcl  33955  cos9thpiminplylem1  33960  submateqlem1  33985  cnre2csqlem  34088  tpr2rico  34090  dya2ub  34448  dya2icoseg  34455  ballotlemfcc  34672  ballotlemfrcn0  34708  signslema  34740  ftc2re  34776  subfacval3  35405  dnibndlem8  36707  dnibndlem10  36709  dnibndlem11  36710  dnibndlem12  36711  dnicn  36714  knoppcnlem4  36718  unblimceq0  36729  unbdqndv2lem2  36732  knoppndvlem11  36744  knoppndvlem14  36747  knoppndvlem15  36748  knoppndvlem17  36750  knoppndvlem20  36753  irrdifflemf  37580  poimirlem29  37900  broucube  37905  opnmbllem0  37907  mblfinlem3  37910  mblfinlem4  37911  itg2addnclem  37922  itg2addnclem3  37924  itg2gt0cn  37926  ftc1cnnclem  37942  areacirclem1  37959  areacirclem2  37960  areacirclem4  37962  areacirclem5  37963  areacirc  37964  cntotbnd  38047  rrnmet  38080  rrndstprj1  38081  rrndstprj2  38082  lcmineqlem23  42421  intlewftc  42431  aks4d1p1p2  42440  aks4d1p1p4  42441  dvle2  42442  aks4d1p1  42446  primrootlekpowne0  42475  hashscontpow1  42491  aks6d1c2  42500  aks6d1c5lem2  42508  sticksstones10  42525  sticksstones12a  42527  sticksstones12  42528  aks6d1c6lem3  42542  bcled  42548  bcle2d  42549  unitscyglem2  42566  unitscyglem4  42568  readdrcl2d  42643  frlmvscadiccat  42876  fltnlta  43021  3cubeslem2  43042  3cubeslem4  43046  irrapxlem2  43180  irrapxlem3  43181  irrapxlem4  43182  irrapxlem5  43183  pellexlem2  43187  pellexlem6  43191  pell1qrgaplem  43230  rmspecsqrtnq  43263  rmspecfund  43266  rmspecpos  43273  jm2.24nn  43316  jm2.17c  43319  fzmaxdif  43338  acongeq  43340  modabsdifz  43343  jm3.1lem2  43375  areaquad  43573  sqrtcvallem2  43993  sqrtcvallem3  43994  sqrtcval  43997  imo72b2lem0  44521  cvgdvgrat  44669  hashnzfzclim  44678  binomcxplemdvbinom  44709  oddfl  45640  lefldiveq  45654  fperiodmul  45666  fzdifsuc2  45672  suprltrp  45687  supxrgere  45692  supxrgelem  45696  suplesup  45698  infleinflem2  45729  infleinf  45730  xrralrecnnge  45748  iccshift  45878  iooshift  45882  iooiinicc  45902  fmul01lt1lem2  45945  climinf  45966  sumnnodd  45990  ltmod  45996  lptre2pt  45998  climleltrp  46034  limsupgtlem  46135  liminflimsupclim  46165  fperdvper  46277  dvbdfbdioolem1  46286  dvbdfbdioolem2  46287  dvbdfbdioo  46288  ioodvbdlimc1lem1  46289  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  dvnmul  46301  iblspltprt  46331  itgspltprt  46337  itgiccshift  46338  itgperiod  46339  itgsbtaddcnst  46340  sublevolico  46342  stoweidlem1  46359  stoweidlem11  46369  stoweidlem12  46370  stoweidlem13  46371  stoweidlem14  46372  stoweidlem23  46381  stoweidlem24  46382  stoweidlem25  46383  stoweidlem26  46384  stoweidlem34  46392  stoweidlem40  46398  stoweidlem41  46399  stoweidlem42  46400  stoweidlem45  46403  stoweidlem60  46418  stoweidlem62  46420  wallispilem3  46425  wallispilem4  46426  wallispi  46428  wallispi2lem1  46429  stirlinglem5  46436  stirlinglem11  46442  stirlinglem12  46443  dirkercncflem1  46461  fourierdlem4  46469  fourierdlem6  46471  fourierdlem7  46472  fourierdlem9  46474  fourierdlem13  46478  fourierdlem14  46479  fourierdlem15  46480  fourierdlem19  46484  fourierdlem26  46491  fourierdlem35  46500  fourierdlem39  46504  fourierdlem40  46505  fourierdlem41  46506  fourierdlem42  46507  fourierdlem48  46512  fourierdlem49  46513  fourierdlem50  46514  fourierdlem51  46515  fourierdlem56  46520  fourierdlem57  46521  fourierdlem59  46523  fourierdlem60  46524  fourierdlem61  46525  fourierdlem63  46527  fourierdlem64  46528  fourierdlem65  46529  fourierdlem66  46530  fourierdlem68  46532  fourierdlem71  46535  fourierdlem72  46536  fourierdlem73  46537  fourierdlem74  46538  fourierdlem75  46539  fourierdlem76  46540  fourierdlem78  46542  fourierdlem79  46543  fourierdlem81  46545  fourierdlem82  46546  fourierdlem83  46547  fourierdlem84  46548  fourierdlem88  46552  fourierdlem89  46553  fourierdlem90  46554  fourierdlem91  46555  fourierdlem92  46556  fourierdlem93  46557  fourierdlem95  46559  fourierdlem97  46561  fourierdlem101  46565  fourierdlem103  46567  fourierdlem104  46568  fourierdlem107  46571  fourierdlem109  46573  fourierdlem111  46575  fouriersw  46589  elaa2lem  46591  etransclem23  46615  rrxtopnfi  46645  rrndistlt  46648  ioorrnopnlem  46662  ioorrnopnxrlem  46664  sge0gtfsumgt  46801  iundjiun  46818  volicorecl  46904  hoiprodcl  46905  hoiprodcl3  46938  volicore  46939  hoidmvcl  46940  hoidmv1lelem2  46950  hoidmv1lelem3  46951  hoidmv1le  46952  hoidmvlelem1  46953  hoidmvlelem2  46954  hoiqssbllem1  46980  hoiqssbllem2  46981  hoiqssbllem3  46982  hspmbllem1  46984  ovolval5lem1  47010  ovolval5lem2  47011  iunhoiioolem  47033  iccvonmbllem  47036  vonicclem1  47041  preimageiingt  47078  salpreimagtge  47083  smfaddlem1  47121  smflimlem4  47132  smfmullem1  47149  smfmullem2  47150  smfmullem3  47151  ltsubsubaddltsub  47661  2elfz2melfz  47678  2tceilhalfelfzo1  47692  requad01  47981  requad1  47982  requad2  47983  bgoldbtbndlem2  48166  bgoldbtbndlem3  48167  bgoldbtbndlem4  48168  bgoldbtbnd  48169  gpgedgvtx0  48421  gpgedgvtx1  48422  gpg5nbgrvtx03starlem2  48429  gpg5nbgrvtx13starlem2  48432  ply1mulgsumlem2  48747  nnpw2pmod  48943  dignn0flhalflem1  48975  affinecomb1  49062  rrxlinesc  49095  rrxlinec  49096  eenglngeehlnmlem1  49097  eenglngeehlnmlem2  49098  rrx2vlinest  49101  rrx2linest2  49104  2sphere  49109  line2  49112  itsclc0lem2  49117  itsclc0lem3  49118  itscnhlc0yqe  49119  itsclc0yqsollem2  49123  itsclc0yqsol  49124  itscnhlc0xyqsol  49125  itsclinecirc0  49133  itsclinecirc0b  49134  itsclinecirc0in  49135  itsclquadb  49136  2itscp  49141  itscnhlinecirc02plem1  49142  itscnhlinecirc02p  49145  inlinecirc02plem  49146  amgmwlem  50161