MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  resubcld Structured version   Visualization version   GIF version

Theorem resubcld 10310
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
StepHypRef Expression
1 renegcld.1 . 2 (𝜑𝐴 ∈ ℝ)
2 resubcld.2 . 2 (𝜑𝐵 ∈ ℝ)
3 resubcl 10197 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵) ∈ ℝ)
41, 2, 3syl2anc 690 1 (𝜑 → (𝐴𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  (class class class)co 6527  cr 9792  cmin 10118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-pnf 9933  df-mnf 9934  df-ltxr 9936  df-sub 10120  df-neg 10121
This theorem is referenced by:  ltsubadd  10350  lesubadd  10352  lesub1  10374  lesub2  10375  ltsub1  10376  ltsub2  10377  lt2sub  10378  le2sub  10379  ltmul1a  10724  supaddc  10840  cru  10862  qbtwnre  11866  lincmb01cmp  12145  iccf1o  12146  xov1plusxeqvd  12148  intfracq  12478  fldiv  12479  modlt  12499  modsubdir  12559  modsumfzodifsn  12563  serle  12676  expmulnbnd  12816  discr  12821  fzsdom2  13030  cshwidxmod  13349  crre  13651  remullem  13665  sqrlem7  13786  absrdbnd  13878  fzomaxdiflem  13879  caubnd2  13894  amgm2  13906  icodiamlt  13971  mulcn2  14123  reccn2  14124  rlimo1  14144  climle  14167  climsqz  14168  climsqz2  14169  rlimle  14175  isercolllem1  14192  climsup  14197  caucvgrlem  14200  caucvgrlem2  14202  iseraltlem2  14210  iseraltlem3  14211  iseralt  14212  fsumle  14321  cvgcmp  14338  cvgcmpce  14340  bpoly4  14578  eflt  14635  resinhcl  14674  tanhlt1  14678  sin01bnd  14703  sin01gt0  14708  moddvds  14778  bitscmp  14947  bitsinv1lem  14950  smueqlem  14999  modprm0  15297  pcbc  15391  4sqlem15  15450  blss2ps  21966  blss2  21967  blssps  21987  blss  21988  nm2dif  22187  nlmvscnlem2  22247  nrginvrcnlem  22253  iccntr  22380  icccmplem2  22382  metdstri  22410  cnllycmp  22511  evth  22514  lebnumii  22521  ipcnlem2  22796  cncmet  22872  rrxds  22934  rrxmval  22941  rrxmet  22944  rrxdstprj1  22945  minveclem3b  22952  minveclem4  22956  ivthlem2  22973  ivthlem3  22974  ovollb2lem  23008  ovoliunlem1  23022  ovolscalem1  23033  ovolicc1  23036  ovolicc2lem4  23040  ovolicc2  23042  ovolicc  23043  voliunlem2  23071  ovolioo  23088  ioorcl2  23091  uniioovol  23098  uniioombllem2  23102  uniioombllem3a  23103  uniioombllem3  23104  uniioombllem4  23105  uniioombllem6  23107  opnmbllem  23120  volcn  23125  vitalilem2  23129  ismbf3d  23172  mbfaddlem  23178  i1fadd  23213  itg1addlem4  23217  mbfi1fseqlem6  23238  itg2seq  23260  itg2split  23267  itg2cnlem2  23280  itg2cn  23281  itgrevallem1  23312  dvcjbr  23463  dvferm1lem  23496  dvferm2lem  23498  cmvth  23503  mvth  23504  dvlip  23505  dvlip2  23507  c1liplem1  23508  dvgt0  23516  dvlt0  23517  dvge0  23518  dvle  23519  dvivthlem1  23520  lhop1lem  23525  lhop  23528  dvcnvrelem1  23529  dvcnvrelem2  23530  dvcnvre  23531  dvcvx  23532  dvfsumle  23533  dvfsumge  23534  dvfsumrlimf  23537  dvfsumlem2  23539  dvfsumlem3  23540  dvfsumlem4  23541  dvfsum2  23546  ftc1a  23549  ftc1lem4  23551  coe1mul3  23608  ply1divex  23645  plydivex  23801  aalioulem2  23837  aalioulem3  23838  aalioulem4  23839  aalioulem5  23840  aalioulem6  23841  aaliou3lem7  23853  taylthlem2  23877  mtest  23907  pilem2  23955  tangtx  24006  cosordlem  24026  efif1olem2  24038  logcnlem3  24135  logcnlem4  24136  isosctrlem2  24294  chordthmlem2  24305  chordthmlem4  24307  heron  24310  atanlogsublem  24387  atantan  24395  birthdaylem3  24425  logdifbnd  24465  emcllem1  24467  emcllem2  24468  emcllem5  24471  emcllem6  24472  harmonicbnd4  24482  fsumharmonic  24483  lgamgulmlem2  24501  lgamgulmlem3  24502  lgamucov  24509  relgamcl  24533  ftalem2  24545  ftalem5  24548  chpub  24690  logfaclbnd  24692  logfacbnd3  24693  logexprlim  24695  bposlem1  24754  bposlem9  24762  gausslemma2dlem1a  24835  lgseisenlem1  24845  lgsquadlem1  24850  chtppilimlem1  24907  vmadivsum  24916  vmadivsumb  24917  rplogsumlem1  24918  rplogsumlem2  24919  rpvmasumlem  24921  dchrisumlem2  24924  dchrisum0re  24947  rplogsum  24961  mulogsumlem  24965  mulog2sumlem1  24968  vmalogdivsum2  24972  vmalogdivsum  24973  2vmadivsumlem  24974  log2sumbnd  24978  selbergb  24983  selberg2lem  24984  selberg2b  24986  chpdifbndlem1  24987  selberg3lem1  24991  selberg3lem2  24992  selberg3  24993  selberg4lem1  24994  selberg4  24995  pntrf  24997  pntrmax  24998  pntrsumo1  24999  selberg3r  25003  selberg4r  25004  selberg34r  25005  pntrlog2bndlem1  25011  pntrlog2bndlem2  25012  pntrlog2bndlem3  25013  pntrlog2bndlem4  25014  pntrlog2bndlem5  25015  pntrlog2bndlem6  25017  pntrlog2bnd  25018  pntpbnd1a  25019  pntpbnd2  25021  pntibndlem2  25025  pntlemg  25032  pntlemn  25034  pntlemj  25037  pntlemf  25039  pntlemo  25041  pntlem3  25043  pntleml  25045  ttgcontlem1  25511  eqeelen  25530  brbtwn2  25531  colinearalg  25536  axcgrid  25542  axsegconlem1  25543  axsegconlem3  25545  axsegconlem8  25550  axsegconlem9  25551  axsegconlem10  25552  ax5seglem3a  25556  ax5seg  25564  axpaschlem  25566  axcontlem8  25597  clwlkisclwwlklem2fv2  26105  clwlkisclwwlklem2a4  26106  clwlkisclwwlklem2a  26107  extwwlkfablem2  26399  nvabs  26734  dipcj  26785  minvecolem4  26954  lt2addrd  28737  xlt2addrd  28747  fzsplit3  28774  bcm1n  28775  bhmafibid1  28809  2sqmod  28813  submateqlem1  29035  cnre2csqlem  29118  tpr2rico  29120  dya2ub  29493  dya2icoseg  29500  ballotlemfcc  29716  ballotlemfrcn0  29752  sgnsub  29767  signslema  29799  subfacval3  30259  dnibndlem8  31479  dnibndlem10  31481  dnibndlem11  31482  dnibndlem12  31483  dnicn  31486  knoppcnlem4  31490  unblimceq0  31502  unbdqndv2lem2  31505  knoppndvlem11  31517  knoppndvlem14  31520  knoppndvlem15  31521  knoppndvlem17  31523  knoppndvlem20  31526  poimirlem29  32432  broucube  32437  opnmbllem0  32439  mblfinlem3  32442  mblfinlem4  32443  itg2addnclem  32455  itg2addnclem3  32457  itg2gt0cn  32459  ftc1cnnclem  32477  areacirclem1  32494  areacirclem2  32495  areacirclem4  32497  areacirclem5  32498  areacirc  32499  cntotbnd  32589  rrnmet  32622  rrndstprj1  32623  rrndstprj2  32624  irrapxlem2  36229  irrapxlem3  36230  irrapxlem4  36231  irrapxlem5  36232  pellexlem2  36236  pellexlem6  36240  pell1qrgaplem  36279  rmspecsqrtnq  36312  rmspecfund  36316  rmspecpos  36323  jm2.24nn  36368  jm2.17c  36371  fzmaxdif  36390  acongeq  36392  modabsdifz  36395  jm3.1lem2  36427  areaquad  36645  imo72b2lem0  37311  cvgdvgrat  37358  hashnzfzclim  37367  binomcxplemdvbinom  37398  oddfl  38254  lefldiveq  38270  fperiodmul  38283  fzdifsuc2  38290  suprltrp  38309  supxrgere  38314  supxrgelem  38318  suplesup  38320  infleinflem2  38352  infleinf  38353  xrralrecnnge  38378  iccshift  38415  iooshift  38419  iooiinicc  38440  fmul01lt1lem2  38476  climinf  38497  sumnnodd  38521  ltmod  38529  lptre2pt  38531  climleltrp  38567  fperdvper  38632  dvbdfbdioolem1  38642  dvbdfbdioolem2  38643  dvbdfbdioo  38644  ioodvbdlimc1lem1  38645  ioodvbdlimc1lem2  38646  ioodvbdlimc2lem  38648  dvnmul  38657  iblspltprt  38689  itgspltprt  38695  itgiccshift  38696  itgperiod  38697  itgsbtaddcnst  38698  sublevolico  38701  stoweidlem1  38718  stoweidlem11  38728  stoweidlem12  38729  stoweidlem13  38730  stoweidlem14  38731  stoweidlem23  38740  stoweidlem24  38741  stoweidlem25  38742  stoweidlem26  38743  stoweidlem34  38751  stoweidlem40  38757  stoweidlem41  38758  stoweidlem42  38759  stoweidlem45  38762  stoweidlem60  38777  stoweidlem62  38779  wallispilem3  38784  wallispilem4  38785  wallispi  38787  wallispi2lem1  38788  stirlinglem5  38795  stirlinglem11  38801  stirlinglem12  38802  dirkercncflem1  38820  fourierdlem4  38828  fourierdlem6  38830  fourierdlem7  38831  fourierdlem9  38833  fourierdlem13  38837  fourierdlem14  38838  fourierdlem15  38839  fourierdlem19  38843  fourierdlem26  38850  fourierdlem35  38859  fourierdlem39  38863  fourierdlem40  38864  fourierdlem41  38865  fourierdlem42  38866  fourierdlem48  38871  fourierdlem49  38872  fourierdlem50  38873  fourierdlem51  38874  fourierdlem56  38879  fourierdlem57  38880  fourierdlem59  38882  fourierdlem60  38883  fourierdlem61  38884  fourierdlem63  38886  fourierdlem64  38887  fourierdlem65  38888  fourierdlem66  38889  fourierdlem68  38891  fourierdlem71  38894  fourierdlem72  38895  fourierdlem73  38896  fourierdlem74  38897  fourierdlem75  38898  fourierdlem76  38899  fourierdlem78  38901  fourierdlem79  38902  fourierdlem81  38904  fourierdlem82  38905  fourierdlem83  38906  fourierdlem84  38907  fourierdlem88  38911  fourierdlem89  38912  fourierdlem90  38913  fourierdlem91  38914  fourierdlem92  38915  fourierdlem93  38916  fourierdlem95  38918  fourierdlem97  38920  fourierdlem101  38924  fourierdlem103  38926  fourierdlem104  38927  fourierdlem107  38930  fourierdlem109  38932  fourierdlem111  38934  fouriersw  38948  elaa2lem  38950  etransclem23  38974  rrxdsfi  39005  rrxtopnfi  39006  rrndistlt  39010  ioorrnopnlem  39024  ioorrnopnxrlem  39026  sge0gtfsumgt  39160  iundjiun  39177  volicorecl  39260  hoiprodcl  39261  hoiprodcl3  39294  volicore  39295  hoidmvcl  39296  hoidmv1lelem2  39306  hoidmv1lelem3  39307  hoidmv1le  39308  hoidmvlelem1  39309  hoidmvlelem2  39310  hoiqssbllem1  39336  hoiqssbllem2  39337  hoiqssbllem3  39338  hspmbllem1  39340  ovolval5lem1  39366  ovolval5lem2  39367  iunhoiioolem  39390  iccvonmbllem  39393  vonicclem1  39398  preimageiingt  39431  salpreimagtge  39435  smfaddlem1  39473  smflimlem4  39484  smfmullem1  39500  smfmullem2  39501  smfmullem3  39502  bgoldbtbndlem2  40047  bgoldbtbndlem3  40048  bgoldbtbndlem4  40049  bgoldbtbnd  40050  ltsubsubaddltsub  40194  2elfz2melfz  40202  nbusgrvtxm1  40629  crctcsh1wlkn0lem3  41037  crctcsh1wlkn0lem5  41039  crctcsh  41049  clwlkclwwlklem2fv2  41227  clwlkclwwlklem2a4  41228  clwlkclwwlklem2a  41229  av-extwwlkfablem2  41532  ply1mulgsumlem2  41991  difmodm1lt  42133  nnpw2pmod  42197  dignn0flhalflem1  42229  amgmwlem  42340
  Copyright terms: Public domain W3C validator