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

Theorem resubcld 11583
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 11465 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵) ∈ ℝ)
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  (class class class)co 7357  cr 11050  cmin 11385
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-ltxr 11194  df-sub 11387  df-neg 11388
This theorem is referenced by:  ltsubadd  11625  lesubadd  11627  lesub1  11649  lesub2  11650  ltsub1  11651  ltsub2  11652  lt2sub  11653  le2sub  11654  ltmul1a  12004  supaddc  12122  cru  12145  qbtwnre  13118  lincmb01cmp  13412  iccf1o  13413  xov1plusxeqvd  13415  intfracq  13764  fldiv  13765  modlt  13785  modsubdir  13845  modsumfzodifsn  13849  serle  13963  expmulnbnd  14138  discr  14143  fzsdom2  14328  cshwidxmod  14691  crre  14999  remullem  15013  01sqrexlem7  15133  absrdbnd  15226  fzomaxdiflem  15227  caubnd2  15242  amgm2  15254  icodiamlt  15320  bhmafibid1  15350  mulcn2  15478  reccn2  15479  rlimo1  15499  climle  15522  climsqz  15523  climsqz2  15524  rlimle  15532  isercolllem1  15549  climsup  15554  caucvgrlem  15557  caucvgrlem2  15559  iseraltlem2  15567  iseraltlem3  15568  iseralt  15569  fsumle  15684  cvgcmp  15701  cvgcmpce  15703  bpoly4  15942  eflt  15999  resinhcl  16038  tanhlt1  16042  sin01bnd  16067  sin01gt0  16072  moddvds  16147  bitscmp  16318  bitsinv1lem  16321  smueqlem  16370  modprm0  16677  pcbc  16772  4sqlem15  16831  blss2ps  23756  blss2  23757  blssps  23777  blss  23778  nm2dif  23981  nlmvscnlem2  24049  nrginvrcnlem  24055  iccntr  24184  icccmplem2  24186  metdstri  24214  cnllycmp  24319  evth  24322  lebnumii  24329  ipcnlem2  24608  cncmet  24686  rrxds  24757  rrxmval  24769  rrxmet  24772  rrxdstprj1  24773  rrxdsfi  24775  ehl1eudis  24784  ehl2eudis  24786  minveclem3b  24792  minveclem4  24796  ivthlem2  24816  ivthlem3  24817  ovollb2lem  24852  ovoliunlem1  24866  ovolscalem1  24877  ovolicc1  24880  ovolicc2lem4  24884  ovolicc2  24886  ovolicc  24887  voliunlem2  24915  ovolioo  24932  ioorcl2  24936  uniioovol  24943  uniioombllem2  24947  uniioombllem3a  24948  uniioombllem3  24949  uniioombllem4  24950  uniioombllem6  24952  opnmbllem  24965  volcn  24970  vitalilem2  24973  ismbf3d  25018  mbfaddlem  25024  i1fadd  25059  itg1addlem4  25063  itg1addlem4OLD  25064  mbfi1fseqlem6  25085  itg2seq  25107  itg2split  25114  itg2cnlem2  25127  itg2cn  25128  itgrevallem1  25159  dvcjbr  25313  dvferm1lem  25348  dvferm2lem  25350  cmvth  25355  mvth  25356  dvlip  25357  dvlip2  25359  c1liplem1  25360  dvgt0  25368  dvlt0  25369  dvge0  25370  dvle  25371  dvivthlem1  25372  lhop1lem  25377  lhop  25380  dvcnvrelem1  25381  dvcnvrelem2  25382  dvcnvre  25383  dvcvx  25384  dvfsumle  25385  dvfsumge  25386  dvfsumrlimf  25389  dvfsumlem2  25391  dvfsumlem3  25392  dvfsumlem4  25393  dvfsum2  25398  ftc1a  25401  ftc1lem4  25403  coe1mul3  25464  ply1divex  25501  plydivex  25657  aalioulem2  25693  aalioulem3  25694  aalioulem4  25695  aalioulem5  25696  aalioulem6  25697  aaliou3lem7  25709  taylthlem2  25733  mtest  25763  pilem2  25811  tangtx  25862  cosordlem  25886  efif1olem2  25899  logcnlem3  25999  logcnlem4  26000  isosctrlem2  26169  chordthmlem2  26183  chordthmlem4  26185  heron  26188  atanlogsublem  26265  atantan  26273  birthdaylem3  26303  logdifbnd  26343  emcllem1  26345  emcllem2  26346  emcllem5  26349  emcllem6  26350  harmonicbnd4  26360  fsumharmonic  26361  lgamgulmlem2  26379  lgamgulmlem3  26380  lgamucov  26387  relgamcl  26411  ftalem2  26423  ftalem5  26426  chpub  26568  logfaclbnd  26570  logfacbnd3  26571  logexprlim  26573  bposlem1  26632  bposlem9  26640  gausslemma2dlem1a  26713  lgseisenlem1  26723  lgsquadlem1  26728  2sqmod  26784  chtppilimlem1  26821  vmadivsum  26830  vmadivsumb  26831  rplogsumlem1  26832  rplogsumlem2  26833  rpvmasumlem  26835  dchrisumlem2  26838  dchrisum0re  26861  rplogsum  26875  mulogsumlem  26879  mulog2sumlem1  26882  vmalogdivsum2  26886  vmalogdivsum  26887  2vmadivsumlem  26888  log2sumbnd  26892  selbergb  26897  selberg2lem  26898  selberg2b  26900  chpdifbndlem1  26901  selberg3lem1  26905  selberg3lem2  26906  selberg3  26907  selberg4lem1  26908  selberg4  26909  pntrf  26911  pntrmax  26912  pntrsumo1  26913  selberg3r  26917  selberg4r  26918  selberg34r  26919  pntrlog2bndlem1  26925  pntrlog2bndlem2  26926  pntrlog2bndlem3  26927  pntrlog2bndlem4  26928  pntrlog2bndlem5  26929  pntrlog2bndlem6  26931  pntrlog2bnd  26932  pntpbnd1a  26933  pntpbnd2  26935  pntibndlem2  26939  pntlemg  26946  pntlemn  26948  pntlemj  26951  pntlemf  26953  pntlemo  26955  pntlem3  26957  pntleml  26959  ttgcontlem1  27833  eqeelen  27853  brbtwn2  27854  colinearalg  27859  axcgrid  27865  axsegconlem1  27866  axsegconlem3  27868  axsegconlem8  27873  axsegconlem9  27874  axsegconlem10  27875  ax5seglem3a  27879  ax5seg  27887  axpaschlem  27889  axcontlem8  27920  nbusgrvtxm1  28327  crctcshwlkn0lem3  28757  crctcshwlkn0lem5  28759  crctcsh  28769  clwlkclwwlklem2fv2  28940  clwlkclwwlklem2a4  28941  clwlkclwwlklem2a  28942  nvabs  29614  dipcj  29656  minvecolem4  29822  lt2addrd  31656  xlt2addrd  31663  fzsplit3  31697  bcm1n  31698  submateqlem1  32388  cnre2csqlem  32491  tpr2rico  32493  dya2ub  32870  dya2icoseg  32877  ballotlemfcc  33093  ballotlemfrcn0  33129  sgnsub  33144  signslema  33174  ftc2re  33211  subfacval3  33783  dnibndlem8  34948  dnibndlem10  34950  dnibndlem11  34951  dnibndlem12  34952  dnicn  34955  knoppcnlem4  34959  unblimceq0  34970  unbdqndv2lem2  34973  knoppndvlem11  34985  knoppndvlem14  34988  knoppndvlem15  34989  knoppndvlem17  34991  knoppndvlem20  34994  irrdifflemf  35796  poimirlem29  36107  broucube  36112  opnmbllem0  36114  mblfinlem3  36117  mblfinlem4  36118  itg2addnclem  36129  itg2addnclem3  36131  itg2gt0cn  36133  ftc1cnnclem  36149  areacirclem1  36166  areacirclem2  36167  areacirclem4  36169  areacirclem5  36170  areacirc  36171  cntotbnd  36255  rrnmet  36288  rrndstprj1  36289  rrndstprj2  36290  lcmineqlem23  40508  intlewftc  40518  aks4d1p1p2  40527  aks4d1p1p4  40528  dvle2  40529  aks4d1p1  40533  sticksstones10  40563  sticksstones12a  40565  sticksstones12  40566  metakunt1  40577  metakunt7  40583  metakunt16  40592  metakunt18  40594  metakunt28  40604  metakunt29  40605  metakunt30  40606  frlmvscadiccat  40680  fltnlta  40987  3cubeslem2  40994  3cubeslem4  40998  irrapxlem2  41132  irrapxlem3  41133  irrapxlem4  41134  irrapxlem5  41135  pellexlem2  41139  pellexlem6  41143  pell1qrgaplem  41182  rmspecsqrtnq  41215  rmspecfund  41218  rmspecpos  41226  jm2.24nn  41269  jm2.17c  41272  fzmaxdif  41291  acongeq  41293  modabsdifz  41296  jm3.1lem2  41328  areaquad  41536  sqrtcvallem2  41899  sqrtcvallem3  41900  sqrtcval  41903  imo72b2lem0  42428  cvgdvgrat  42583  hashnzfzclim  42592  binomcxplemdvbinom  42623  oddfl  43501  lefldiveq  43516  fperiodmul  43528  fzdifsuc2  43534  suprltrp  43552  supxrgere  43557  supxrgelem  43561  suplesup  43563  infleinflem2  43595  infleinf  43596  xrralrecnnge  43615  iccshift  43746  iooshift  43750  iooiinicc  43770  fmul01lt1lem2  43816  climinf  43837  sumnnodd  43861  ltmod  43869  lptre2pt  43871  climleltrp  43907  limsupgtlem  44008  liminflimsupclim  44038  fperdvper  44150  dvbdfbdioolem1  44159  dvbdfbdioolem2  44160  dvbdfbdioo  44161  ioodvbdlimc1lem1  44162  ioodvbdlimc1lem2  44163  ioodvbdlimc2lem  44165  dvnmul  44174  iblspltprt  44204  itgspltprt  44210  itgiccshift  44211  itgperiod  44212  itgsbtaddcnst  44213  sublevolico  44215  stoweidlem1  44232  stoweidlem11  44242  stoweidlem12  44243  stoweidlem13  44244  stoweidlem14  44245  stoweidlem23  44254  stoweidlem24  44255  stoweidlem25  44256  stoweidlem26  44257  stoweidlem34  44265  stoweidlem40  44271  stoweidlem41  44272  stoweidlem42  44273  stoweidlem45  44276  stoweidlem60  44291  stoweidlem62  44293  wallispilem3  44298  wallispilem4  44299  wallispi  44301  wallispi2lem1  44302  stirlinglem5  44309  stirlinglem11  44315  stirlinglem12  44316  dirkercncflem1  44334  fourierdlem4  44342  fourierdlem6  44344  fourierdlem7  44345  fourierdlem9  44347  fourierdlem13  44351  fourierdlem14  44352  fourierdlem15  44353  fourierdlem19  44357  fourierdlem26  44364  fourierdlem35  44373  fourierdlem39  44377  fourierdlem40  44378  fourierdlem41  44379  fourierdlem42  44380  fourierdlem48  44385  fourierdlem49  44386  fourierdlem50  44387  fourierdlem51  44388  fourierdlem56  44393  fourierdlem57  44394  fourierdlem59  44396  fourierdlem60  44397  fourierdlem61  44398  fourierdlem63  44400  fourierdlem64  44401  fourierdlem65  44402  fourierdlem66  44403  fourierdlem68  44405  fourierdlem71  44408  fourierdlem72  44409  fourierdlem73  44410  fourierdlem74  44411  fourierdlem75  44412  fourierdlem76  44413  fourierdlem78  44415  fourierdlem79  44416  fourierdlem81  44418  fourierdlem82  44419  fourierdlem83  44420  fourierdlem84  44421  fourierdlem88  44425  fourierdlem89  44426  fourierdlem90  44427  fourierdlem91  44428  fourierdlem92  44429  fourierdlem93  44430  fourierdlem95  44432  fourierdlem97  44434  fourierdlem101  44438  fourierdlem103  44440  fourierdlem104  44441  fourierdlem107  44444  fourierdlem109  44446  fourierdlem111  44448  fouriersw  44462  elaa2lem  44464  etransclem23  44488  rrxtopnfi  44518  rrndistlt  44521  ioorrnopnlem  44535  ioorrnopnxrlem  44537  sge0gtfsumgt  44674  iundjiun  44691  volicorecl  44777  hoiprodcl  44778  hoiprodcl3  44811  volicore  44812  hoidmvcl  44813  hoidmv1lelem2  44823  hoidmv1lelem3  44824  hoidmv1le  44825  hoidmvlelem1  44826  hoidmvlelem2  44827  hoiqssbllem1  44853  hoiqssbllem2  44854  hoiqssbllem3  44855  hspmbllem1  44857  ovolval5lem1  44883  ovolval5lem2  44884  iunhoiioolem  44906  iccvonmbllem  44909  vonicclem1  44914  preimageiingt  44951  salpreimagtge  44956  smfaddlem1  44994  smflimlem4  45005  smfmullem1  45022  smfmullem2  45023  smfmullem3  45024  ltsubsubaddltsub  45523  2elfz2melfz  45540  requad01  45803  requad1  45804  requad2  45805  bgoldbtbndlem2  45988  bgoldbtbndlem3  45989  bgoldbtbndlem4  45990  bgoldbtbnd  45991  ply1mulgsumlem2  46458  difmodm1lt  46598  nnpw2pmod  46659  dignn0flhalflem1  46691  affinecomb1  46778  rrxlinesc  46811  rrxlinec  46812  eenglngeehlnmlem1  46813  eenglngeehlnmlem2  46814  rrx2vlinest  46817  rrx2linest2  46820  2sphere  46825  line2  46828  itsclc0lem2  46833  itsclc0lem3  46834  itscnhlc0yqe  46835  itsclc0yqsollem2  46839  itsclc0yqsol  46840  itscnhlc0xyqsol  46841  itsclinecirc0  46849  itsclinecirc0b  46850  itsclinecirc0in  46851  itsclquadb  46852  2itscp  46857  itscnhlinecirc02plem1  46858  itscnhlinecirc02p  46861  inlinecirc02plem  46862  amgmwlem  47239
  Copyright terms: Public domain W3C validator