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

Theorem resubcld 10737
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 10624 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵) ∈ ℝ)
41, 2, 3syl2anc 575 1 (𝜑 → (𝐴𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  (class class class)co 6868  cr 10214  cmin 10545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-resscn 10272  ax-1cn 10273  ax-icn 10274  ax-addcl 10275  ax-addrcl 10276  ax-mulcl 10277  ax-mulrcl 10278  ax-mulcom 10279  ax-addass 10280  ax-mulass 10281  ax-distr 10282  ax-i2m1 10283  ax-1ne0 10284  ax-1rid 10285  ax-rnegex 10286  ax-rrecex 10287  ax-cnre 10288  ax-pre-lttri 10289  ax-pre-lttrn 10290  ax-pre-ltadd 10291
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-nel 3078  df-ral 3097  df-rex 3098  df-reu 3099  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-op 4371  df-uni 4624  df-br 4838  df-opab 4900  df-mpt 4917  df-id 5213  df-po 5226  df-so 5227  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-riota 6829  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-er 7973  df-en 8187  df-dom 8188  df-sdom 8189  df-pnf 10355  df-mnf 10356  df-ltxr 10358  df-sub 10547  df-neg 10548
This theorem is referenced by:  ltsubadd  10777  lesubadd  10779  lesub1  10801  lesub2  10802  ltsub1  10803  ltsub2  10804  lt2sub  10805  le2sub  10806  ltmul1a  11151  supaddc  11269  cru  11291  qbtwnre  12242  lincmb01cmp  12532  iccf1o  12533  xov1plusxeqvd  12535  intfracq  12876  fldiv  12877  modlt  12897  modsubdir  12957  modsumfzodifsn  12961  serle  13073  expmulnbnd  13213  discr  13218  fzsdom2  13426  cshwidxmod  13767  crre  14071  remullem  14085  sqrlem7  14206  absrdbnd  14298  fzomaxdiflem  14299  caubnd2  14314  amgm2  14326  icodiamlt  14391  mulcn2  14543  reccn2  14544  rlimo1  14564  climle  14587  climsqz  14588  climsqz2  14589  rlimle  14595  isercolllem1  14612  climsup  14617  caucvgrlem  14620  caucvgrlem2  14622  iseraltlem2  14630  iseraltlem3  14631  iseralt  14632  fsumle  14747  cvgcmp  14764  cvgcmpce  14766  bpoly4  15004  eflt  15061  resinhcl  15100  tanhlt1  15104  sin01bnd  15129  sin01gt0  15134  moddvds  15208  bitscmp  15373  bitsinv1lem  15376  smueqlem  15425  modprm0  15721  pcbc  15815  4sqlem15  15874  blss2ps  22415  blss2  22416  blssps  22436  blss  22437  nm2dif  22636  nlmvscnlem2  22696  nrginvrcnlem  22702  iccntr  22831  icccmplem2  22833  metdstri  22861  cnllycmp  22962  evth  22965  lebnumii  22972  ipcnlem2  23249  cncmet  23325  rrxds  23387  rrxmval  23394  rrxmet  23397  rrxdstprj1  23398  minveclem3b  23405  minveclem4  23409  ivthlem2  23427  ivthlem3  23428  ovollb2lem  23463  ovoliunlem1  23477  ovolscalem1  23488  ovolicc1  23491  ovolicc2lem4  23495  ovolicc2  23497  ovolicc  23498  voliunlem2  23526  ovolioo  23543  ioorcl2  23547  uniioovol  23554  uniioombllem2  23558  uniioombllem3a  23559  uniioombllem3  23560  uniioombllem4  23561  uniioombllem6  23563  opnmbllem  23576  volcn  23581  vitalilem2  23584  ismbf3d  23629  mbfaddlem  23635  i1fadd  23670  itg1addlem4  23674  mbfi1fseqlem6  23695  itg2seq  23717  itg2split  23724  itg2cnlem2  23737  itg2cn  23738  itgrevallem1  23769  dvcjbr  23920  dvferm1lem  23955  dvferm2lem  23957  cmvth  23962  mvth  23963  dvlip  23964  dvlip2  23966  c1liplem1  23967  dvgt0  23975  dvlt0  23976  dvge0  23977  dvle  23978  dvivthlem1  23979  lhop1lem  23984  lhop  23987  dvcnvrelem1  23988  dvcnvrelem2  23989  dvcnvre  23990  dvcvx  23991  dvfsumle  23992  dvfsumge  23993  dvfsumrlimf  23996  dvfsumlem2  23998  dvfsumlem3  23999  dvfsumlem4  24000  dvfsum2  24005  ftc1a  24008  ftc1lem4  24010  coe1mul3  24067  ply1divex  24104  plydivex  24260  aalioulem2  24296  aalioulem3  24297  aalioulem4  24298  aalioulem5  24299  aalioulem6  24300  aaliou3lem7  24312  taylthlem2  24336  mtest  24366  pilem2  24414  tangtx  24466  cosordlem  24486  efif1olem2  24498  logcnlem3  24598  logcnlem4  24599  isosctrlem2  24757  chordthmlem2  24768  chordthmlem4  24770  heron  24773  atanlogsublem  24850  atantan  24858  birthdaylem3  24888  logdifbnd  24928  emcllem1  24930  emcllem2  24931  emcllem5  24934  emcllem6  24935  harmonicbnd4  24945  fsumharmonic  24946  lgamgulmlem2  24964  lgamgulmlem3  24965  lgamucov  24972  relgamcl  24996  ftalem2  25008  ftalem5  25011  chpub  25153  logfaclbnd  25155  logfacbnd3  25156  logexprlim  25158  bposlem1  25217  bposlem9  25225  gausslemma2dlem1a  25298  lgseisenlem1  25308  lgsquadlem1  25313  chtppilimlem1  25370  vmadivsum  25379  vmadivsumb  25380  rplogsumlem1  25381  rplogsumlem2  25382  rpvmasumlem  25384  dchrisumlem2  25387  dchrisum0re  25410  rplogsum  25424  mulogsumlem  25428  mulog2sumlem1  25431  vmalogdivsum2  25435  vmalogdivsum  25436  2vmadivsumlem  25437  log2sumbnd  25441  selbergb  25446  selberg2lem  25447  selberg2b  25449  chpdifbndlem1  25450  selberg3lem1  25454  selberg3lem2  25455  selberg3  25456  selberg4lem1  25457  selberg4  25458  pntrf  25460  pntrmax  25461  pntrsumo1  25462  selberg3r  25466  selberg4r  25467  selberg34r  25468  pntrlog2bndlem1  25474  pntrlog2bndlem2  25475  pntrlog2bndlem3  25476  pntrlog2bndlem4  25477  pntrlog2bndlem5  25478  pntrlog2bndlem6  25480  pntrlog2bnd  25481  pntpbnd1a  25482  pntpbnd2  25484  pntibndlem2  25488  pntlemg  25495  pntlemn  25497  pntlemj  25500  pntlemf  25502  pntlemo  25504  pntlem3  25506  pntleml  25508  ttgcontlem1  25973  eqeelen  25992  brbtwn2  25993  colinearalg  25998  axcgrid  26004  axsegconlem1  26005  axsegconlem3  26007  axsegconlem8  26012  axsegconlem9  26013  axsegconlem10  26014  ax5seglem3a  26018  ax5seg  26026  axpaschlem  26028  axcontlem8  26059  nbusgrvtxm1  26491  crctcshwlkn0lem3  26927  crctcshwlkn0lem5  26929  crctcsh  26939  clwlkclwwlklem2fv2  27133  clwlkclwwlklem2a4  27134  clwlkclwwlklem2a  27135  nvabs  27849  dipcj  27891  minvecolem4  28058  lt2addrd  29837  xlt2addrd  29844  fzsplit3  29874  bcm1n  29875  bhmafibid1  29963  2sqmod  29967  submateqlem1  30192  cnre2csqlem  30275  tpr2rico  30277  dya2ub  30651  dya2icoseg  30658  ballotlemfcc  30874  ballotlemfrcn0  30910  sgnsub  30925  signslema  30958  ftc2re  30995  subfacval3  31488  dnibndlem8  32786  dnibndlem10  32788  dnibndlem11  32789  dnibndlem12  32790  dnicn  32793  knoppcnlem4  32797  unblimceq0  32809  unbdqndv2lem2  32812  knoppndvlem11  32824  knoppndvlem14  32827  knoppndvlem15  32828  knoppndvlem17  32830  knoppndvlem20  32833  poimirlem29  33745  broucube  33750  opnmbllem0  33752  mblfinlem3  33755  mblfinlem4  33756  itg2addnclem  33767  itg2addnclem3  33769  itg2gt0cn  33771  ftc1cnnclem  33789  areacirclem1  33806  areacirclem2  33807  areacirclem4  33809  areacirclem5  33810  areacirc  33811  cntotbnd  33900  rrnmet  33933  rrndstprj1  33934  rrndstprj2  33935  irrapxlem2  37883  irrapxlem3  37884  irrapxlem4  37885  irrapxlem5  37886  pellexlem2  37890  pellexlem6  37894  pell1qrgaplem  37933  rmspecsqrtnq  37966  rmspecfund  37969  rmspecpos  37976  jm2.24nn  38021  jm2.17c  38024  fzmaxdif  38043  acongeq  38045  modabsdifz  38048  jm3.1lem2  38080  areaquad  38296  imo72b2lem0  38959  cvgdvgrat  39006  hashnzfzclim  39015  binomcxplemdvbinom  39046  oddfl  39965  lefldiveq  39981  fperiodmul  39993  fzdifsuc2  39999  suprltrp  40018  supxrgere  40023  supxrgelem  40027  suplesup  40029  infleinflem2  40061  infleinf  40062  xrralrecnnge  40086  iccshift  40219  iooshift  40223  iooiinicc  40243  fmul01lt1lem2  40291  climinf  40312  sumnnodd  40336  ltmod  40344  lptre2pt  40346  climleltrp  40382  limsupgtlem  40483  liminflimsupclim  40513  fperdvper  40607  dvbdfbdioolem1  40617  dvbdfbdioolem2  40618  dvbdfbdioo  40619  ioodvbdlimc1lem1  40620  ioodvbdlimc1lem2  40621  ioodvbdlimc2lem  40623  dvnmul  40632  iblspltprt  40662  itgspltprt  40668  itgiccshift  40669  itgperiod  40670  itgsbtaddcnst  40671  sublevolico  40674  stoweidlem1  40691  stoweidlem11  40701  stoweidlem12  40702  stoweidlem13  40703  stoweidlem14  40704  stoweidlem23  40713  stoweidlem24  40714  stoweidlem25  40715  stoweidlem26  40716  stoweidlem34  40724  stoweidlem40  40730  stoweidlem41  40731  stoweidlem42  40732  stoweidlem45  40735  stoweidlem60  40750  stoweidlem62  40752  wallispilem3  40757  wallispilem4  40758  wallispi  40760  wallispi2lem1  40761  stirlinglem5  40768  stirlinglem11  40774  stirlinglem12  40775  dirkercncflem1  40793  fourierdlem4  40801  fourierdlem6  40803  fourierdlem7  40804  fourierdlem9  40806  fourierdlem13  40810  fourierdlem14  40811  fourierdlem15  40812  fourierdlem19  40816  fourierdlem26  40823  fourierdlem35  40832  fourierdlem39  40836  fourierdlem40  40837  fourierdlem41  40838  fourierdlem42  40839  fourierdlem48  40844  fourierdlem49  40845  fourierdlem50  40846  fourierdlem51  40847  fourierdlem56  40852  fourierdlem57  40853  fourierdlem59  40855  fourierdlem60  40856  fourierdlem61  40857  fourierdlem63  40859  fourierdlem64  40860  fourierdlem65  40861  fourierdlem66  40862  fourierdlem68  40864  fourierdlem71  40867  fourierdlem72  40868  fourierdlem73  40869  fourierdlem74  40870  fourierdlem75  40871  fourierdlem76  40872  fourierdlem78  40874  fourierdlem79  40875  fourierdlem81  40877  fourierdlem82  40878  fourierdlem83  40879  fourierdlem84  40880  fourierdlem88  40884  fourierdlem89  40885  fourierdlem90  40886  fourierdlem91  40887  fourierdlem92  40888  fourierdlem93  40889  fourierdlem95  40891  fourierdlem97  40893  fourierdlem101  40897  fourierdlem103  40899  fourierdlem104  40900  fourierdlem107  40903  fourierdlem109  40905  fourierdlem111  40907  fouriersw  40921  elaa2lem  40923  etransclem23  40947  rrxdsfi  40978  rrxtopnfi  40979  rrndistlt  40983  ioorrnopnlem  40997  ioorrnopnxrlem  40999  sge0gtfsumgt  41133  iundjiun  41150  volicorecl  41236  hoiprodcl  41237  hoiprodcl3  41270  volicore  41271  hoidmvcl  41272  hoidmv1lelem2  41282  hoidmv1lelem3  41283  hoidmv1le  41284  hoidmvlelem1  41285  hoidmvlelem2  41286  hoiqssbllem1  41312  hoiqssbllem2  41313  hoiqssbllem3  41314  hspmbllem1  41316  ovolval5lem1  41342  ovolval5lem2  41343  iunhoiioolem  41365  iccvonmbllem  41368  vonicclem1  41373  preimageiingt  41406  salpreimagtge  41410  smfaddlem1  41447  smflimlem4  41458  smfmullem1  41474  smfmullem2  41475  smfmullem3  41476  ltsubsubaddltsub  41885  2elfz2melfz  41897  bgoldbtbndlem2  42263  bgoldbtbndlem3  42264  bgoldbtbndlem4  42265  bgoldbtbnd  42266  ply1mulgsumlem2  42737  difmodm1lt  42879  nnpw2pmod  42939  dignn0flhalflem1  42971  amgmwlem  43113
  Copyright terms: Public domain W3C validator