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

Theorem resubcld 11057
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 10939 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵) ∈ ℝ)
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  (class class class)co 7145  cr 10525  cmin 10859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-po 5468  df-so 5469  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-ltxr 10669  df-sub 10861  df-neg 10862
This theorem is referenced by:  ltsubadd  11099  lesubadd  11101  lesub1  11123  lesub2  11124  ltsub1  11125  ltsub2  11126  lt2sub  11127  le2sub  11128  ltmul1a  11478  supaddc  11597  cru  11619  qbtwnre  12582  lincmb01cmp  12871  iccf1o  12872  xov1plusxeqvd  12874  intfracq  13217  fldiv  13218  modlt  13238  modsubdir  13298  modsumfzodifsn  13302  serle  13415  expmulnbnd  13586  discr  13591  fzsdom2  13779  cshwidxmod  14155  crre  14463  remullem  14477  sqrlem7  14598  absrdbnd  14691  fzomaxdiflem  14692  caubnd2  14707  amgm2  14719  icodiamlt  14785  bhmafibid1  14815  mulcn2  14942  reccn2  14943  rlimo1  14963  climle  14986  climsqz  14987  climsqz2  14988  rlimle  14994  isercolllem1  15011  climsup  15016  caucvgrlem  15019  caucvgrlem2  15021  iseraltlem2  15029  iseraltlem3  15030  iseralt  15031  fsumle  15144  cvgcmp  15161  cvgcmpce  15163  bpoly4  15403  eflt  15460  resinhcl  15499  tanhlt1  15503  sin01bnd  15528  sin01gt0  15533  moddvds  15608  bitscmp  15777  bitsinv1lem  15780  smueqlem  15829  modprm0  16132  pcbc  16226  4sqlem15  16285  blss2ps  22942  blss2  22943  blssps  22963  blss  22964  nm2dif  23163  nlmvscnlem2  23223  nrginvrcnlem  23229  iccntr  23358  icccmplem2  23360  metdstri  23388  cnllycmp  23489  evth  23492  lebnumii  23499  ipcnlem2  23776  cncmet  23854  rrxds  23925  rrxmval  23937  rrxmet  23940  rrxdstprj1  23941  rrxdsfi  23943  ehl1eudis  23952  ehl2eudis  23954  minveclem3b  23960  minveclem4  23964  ivthlem2  23982  ivthlem3  23983  ovollb2lem  24018  ovoliunlem1  24032  ovolscalem1  24043  ovolicc1  24046  ovolicc2lem4  24050  ovolicc2  24052  ovolicc  24053  voliunlem2  24081  ovolioo  24098  ioorcl2  24102  uniioovol  24109  uniioombllem2  24113  uniioombllem3a  24114  uniioombllem3  24115  uniioombllem4  24116  uniioombllem6  24118  opnmbllem  24131  volcn  24136  vitalilem2  24139  ismbf3d  24184  mbfaddlem  24190  i1fadd  24225  itg1addlem4  24229  mbfi1fseqlem6  24250  itg2seq  24272  itg2split  24279  itg2cnlem2  24292  itg2cn  24293  itgrevallem1  24324  dvcjbr  24475  dvferm1lem  24510  dvferm2lem  24512  cmvth  24517  mvth  24518  dvlip  24519  dvlip2  24521  c1liplem1  24522  dvgt0  24530  dvlt0  24531  dvge0  24532  dvle  24533  dvivthlem1  24534  lhop1lem  24539  lhop  24542  dvcnvrelem1  24543  dvcnvrelem2  24544  dvcnvre  24545  dvcvx  24546  dvfsumle  24547  dvfsumge  24548  dvfsumrlimf  24551  dvfsumlem2  24553  dvfsumlem3  24554  dvfsumlem4  24555  dvfsum2  24560  ftc1a  24563  ftc1lem4  24565  coe1mul3  24622  ply1divex  24659  plydivex  24815  aalioulem2  24851  aalioulem3  24852  aalioulem4  24853  aalioulem5  24854  aalioulem6  24855  aaliou3lem7  24867  taylthlem2  24891  mtest  24921  pilem2  24969  tangtx  25020  cosordlem  25042  efif1olem2  25054  logcnlem3  25154  logcnlem4  25155  isosctrlem2  25324  chordthmlem2  25338  chordthmlem4  25340  heron  25343  atanlogsublem  25420  atantan  25428  birthdaylem3  25459  logdifbnd  25499  emcllem1  25501  emcllem2  25502  emcllem5  25505  emcllem6  25506  harmonicbnd4  25516  fsumharmonic  25517  lgamgulmlem2  25535  lgamgulmlem3  25536  lgamucov  25543  relgamcl  25567  ftalem2  25579  ftalem5  25582  chpub  25724  logfaclbnd  25726  logfacbnd3  25727  logexprlim  25729  bposlem1  25788  bposlem9  25796  gausslemma2dlem1a  25869  lgseisenlem1  25879  lgsquadlem1  25884  2sqmod  25940  chtppilimlem1  25977  vmadivsum  25986  vmadivsumb  25987  rplogsumlem1  25988  rplogsumlem2  25989  rpvmasumlem  25991  dchrisumlem2  25994  dchrisum0re  26017  rplogsum  26031  mulogsumlem  26035  mulog2sumlem1  26038  vmalogdivsum2  26042  vmalogdivsum  26043  2vmadivsumlem  26044  log2sumbnd  26048  selbergb  26053  selberg2lem  26054  selberg2b  26056  chpdifbndlem1  26057  selberg3lem1  26061  selberg3lem2  26062  selberg3  26063  selberg4lem1  26064  selberg4  26065  pntrf  26067  pntrmax  26068  pntrsumo1  26069  selberg3r  26073  selberg4r  26074  selberg34r  26075  pntrlog2bndlem1  26081  pntrlog2bndlem2  26082  pntrlog2bndlem3  26083  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntrlog2bnd  26088  pntpbnd1a  26089  pntpbnd2  26091  pntibndlem2  26095  pntlemg  26102  pntlemn  26104  pntlemj  26107  pntlemf  26109  pntlemo  26111  pntlem3  26113  pntleml  26115  ttgcontlem1  26599  eqeelen  26618  brbtwn2  26619  colinearalg  26624  axcgrid  26630  axsegconlem1  26631  axsegconlem3  26633  axsegconlem8  26638  axsegconlem9  26639  axsegconlem10  26640  ax5seglem3a  26644  ax5seg  26652  axpaschlem  26654  axcontlem8  26685  nbusgrvtxm1  27089  crctcshwlkn0lem3  27518  crctcshwlkn0lem5  27520  crctcsh  27530  clwlkclwwlklem2fv2  27702  clwlkclwwlklem2a4  27703  clwlkclwwlklem2a  27704  nvabs  28377  dipcj  28419  minvecolem4  28585  lt2addrd  30402  xlt2addrd  30409  fzsplit3  30444  bcm1n  30445  submateqlem1  30972  cnre2csqlem  31053  tpr2rico  31055  dya2ub  31428  dya2icoseg  31435  ballotlemfcc  31651  ballotlemfrcn0  31687  sgnsub  31702  signslema  31732  ftc2re  31769  subfacval3  32334  dnibndlem8  33722  dnibndlem10  33724  dnibndlem11  33725  dnibndlem12  33726  dnicn  33729  knoppcnlem4  33733  unblimceq0  33744  unbdqndv2lem2  33747  knoppndvlem11  33759  knoppndvlem14  33762  knoppndvlem15  33763  knoppndvlem17  33765  knoppndvlem20  33768  poimirlem29  34803  broucube  34808  opnmbllem0  34810  mblfinlem3  34813  mblfinlem4  34814  itg2addnclem  34825  itg2addnclem3  34827  itg2gt0cn  34829  ftc1cnnclem  34847  areacirclem1  34864  areacirclem2  34865  areacirclem4  34867  areacirclem5  34868  areacirc  34869  cntotbnd  34957  rrnmet  34990  rrndstprj1  34991  rrndstprj2  34992  frlmvscadiccat  39025  fltnlta  39155  3cubeslem2  39162  3cubeslem4  39166  irrapxlem2  39300  irrapxlem3  39301  irrapxlem4  39302  irrapxlem5  39303  pellexlem2  39307  pellexlem6  39311  pell1qrgaplem  39350  rmspecsqrtnq  39383  rmspecfund  39386  rmspecpos  39393  jm2.24nn  39436  jm2.17c  39439  fzmaxdif  39458  acongeq  39460  modabsdifz  39463  jm3.1lem2  39495  areaquad  39703  imo72b2lem0  40396  cvgdvgrat  40525  hashnzfzclim  40534  binomcxplemdvbinom  40565  oddfl  41423  lefldiveq  41439  fperiodmul  41451  fzdifsuc2  41457  suprltrp  41476  supxrgere  41481  supxrgelem  41485  suplesup  41487  infleinflem2  41519  infleinf  41520  xrralrecnnge  41542  iccshift  41674  iooshift  41678  iooiinicc  41698  fmul01lt1lem2  41746  climinf  41767  sumnnodd  41791  ltmod  41799  lptre2pt  41801  climleltrp  41837  limsupgtlem  41938  liminflimsupclim  41968  fperdvper  42083  dvbdfbdioolem1  42093  dvbdfbdioolem2  42094  dvbdfbdioo  42095  ioodvbdlimc1lem1  42096  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvnmul  42108  iblspltprt  42138  itgspltprt  42144  itgiccshift  42145  itgperiod  42146  itgsbtaddcnst  42147  sublevolico  42150  stoweidlem1  42167  stoweidlem11  42177  stoweidlem12  42178  stoweidlem13  42179  stoweidlem14  42180  stoweidlem23  42189  stoweidlem24  42190  stoweidlem25  42191  stoweidlem26  42192  stoweidlem34  42200  stoweidlem40  42206  stoweidlem41  42207  stoweidlem42  42208  stoweidlem45  42211  stoweidlem60  42226  stoweidlem62  42228  wallispilem3  42233  wallispilem4  42234  wallispi  42236  wallispi2lem1  42237  stirlinglem5  42244  stirlinglem11  42250  stirlinglem12  42251  dirkercncflem1  42269  fourierdlem4  42277  fourierdlem6  42279  fourierdlem7  42280  fourierdlem9  42282  fourierdlem13  42286  fourierdlem14  42287  fourierdlem15  42288  fourierdlem19  42292  fourierdlem26  42299  fourierdlem35  42308  fourierdlem39  42312  fourierdlem40  42313  fourierdlem41  42314  fourierdlem42  42315  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  fourierdlem51  42323  fourierdlem56  42328  fourierdlem57  42329  fourierdlem59  42331  fourierdlem60  42332  fourierdlem61  42333  fourierdlem63  42335  fourierdlem64  42336  fourierdlem65  42337  fourierdlem66  42338  fourierdlem68  42340  fourierdlem71  42343  fourierdlem72  42344  fourierdlem73  42345  fourierdlem74  42346  fourierdlem75  42347  fourierdlem76  42348  fourierdlem78  42350  fourierdlem79  42351  fourierdlem81  42353  fourierdlem82  42354  fourierdlem83  42355  fourierdlem84  42356  fourierdlem88  42360  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem92  42364  fourierdlem93  42365  fourierdlem95  42367  fourierdlem97  42369  fourierdlem101  42373  fourierdlem103  42375  fourierdlem104  42376  fourierdlem107  42379  fourierdlem109  42381  fourierdlem111  42383  fouriersw  42397  elaa2lem  42399  etransclem23  42423  rrxtopnfi  42453  rrndistlt  42456  ioorrnopnlem  42470  ioorrnopnxrlem  42472  sge0gtfsumgt  42606  iundjiun  42623  volicorecl  42709  hoiprodcl  42710  hoiprodcl3  42743  volicore  42744  hoidmvcl  42745  hoidmv1lelem2  42755  hoidmv1lelem3  42756  hoidmv1le  42757  hoidmvlelem1  42758  hoidmvlelem2  42759  hoiqssbllem1  42785  hoiqssbllem2  42786  hoiqssbllem3  42787  hspmbllem1  42789  ovolval5lem1  42815  ovolval5lem2  42816  iunhoiioolem  42838  iccvonmbllem  42841  vonicclem1  42846  preimageiingt  42879  salpreimagtge  42883  smfaddlem1  42920  smflimlem4  42931  smfmullem1  42947  smfmullem2  42948  smfmullem3  42949  ltsubsubaddltsub  43382  2elfz2melfz  43399  requad01  43633  requad1  43634  requad2  43635  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  bgoldbtbndlem4  43820  bgoldbtbnd  43821  ply1mulgsumlem2  44339  difmodm1lt  44480  nnpw2pmod  44541  dignn0flhalflem1  44573  affinecomb1  44587  rrxlinesc  44620  rrxlinec  44621  eenglngeehlnmlem1  44622  eenglngeehlnmlem2  44623  rrx2vlinest  44626  rrx2linest2  44629  2sphere  44634  line2  44637  itsclc0lem2  44642  itsclc0lem3  44643  itscnhlc0yqe  44644  itsclc0yqsollem2  44648  itsclc0yqsol  44649  itscnhlc0xyqsol  44650  itsclinecirc0  44658  itsclinecirc0b  44659  itsclinecirc0in  44660  itsclquadb  44661  2itscp  44666  itscnhlinecirc02plem1  44667  itscnhlinecirc02p  44670  inlinecirc02plem  44671  amgmwlem  44801
  Copyright terms: Public domain W3C validator