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

Theorem resubcld 9988
Description: Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
renegcld.1  |-  ( ph  ->  A  e.  RR )
resubcld.2  |-  ( ph  ->  B  e.  RR )
Assertion
Ref Expression
resubcld  |-  ( ph  ->  ( A  -  B
)  e.  RR )

Proof of Theorem resubcld
StepHypRef Expression
1 renegcld.1 . 2  |-  ( ph  ->  A  e.  RR )
2 resubcld.2 . 2  |-  ( ph  ->  B  e.  RR )
3 resubcl 9883 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  -  B
)  e.  RR )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  -  B
)  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802  (class class class)co 6277   RRcr 9489    - cmin 9805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-po 4786  df-so 4787  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-er 7309  df-en 7515  df-dom 7516  df-sdom 7517  df-pnf 9628  df-mnf 9629  df-ltxr 9631  df-sub 9807  df-neg 9808
This theorem is referenced by:  ltsubadd  10023  lesubadd  10025  lesub1  10047  lesub2  10048  ltsub1  10049  ltsub2  10050  lt2sub  10051  le2sub  10052  ltmul1a  10392  cru  10529  qbtwnre  11402  lincmb01cmp  11667  iccf1o  11668  xov1plusxeqvd  11670  intfracq  11960  fldiv  11961  modlt  11980  modsubdir  12029  serle  12136  expmulnbnd  12272  discr  12277  fzsdom2  12460  cshwidxmod  12748  crre  12921  remullem  12935  sqrlem7  13056  absrdbnd  13148  fzomaxdiflem  13149  caubnd2  13164  amgm2  13176  mulcn2  13392  reccn2  13393  rlimo1  13413  climle  13436  climsqz  13437  climsqz2  13438  rlimle  13444  isercolllem1  13461  climsup  13466  caucvgrlem  13469  caucvgrlem2  13471  iseraltlem2  13479  iseraltlem3  13480  iseralt  13481  fsumle  13587  cvgcmp  13604  cvgcmpce  13606  eflt  13724  resinhcl  13763  tanhlt1  13767  sin01bnd  13792  sin01gt0  13797  moddvds  13865  bitscmp  13960  bitsinv1lem  13963  smueqlem  14012  modprm0  14202  pcbc  14291  4sqlem15  14349  blss2ps  20772  blss2  20773  blssps  20793  blss  20794  nm2dif  21010  nlmvscnlem2  21060  nrginvrcnlem  21065  iccntr  21192  icccmplem2  21194  metdstri  21221  cnllycmp  21322  evth  21325  lebnumii  21332  ipcnlem2  21550  cncmet  21627  rrxds  21691  rrxmval  21698  rrxmet  21701  rrxdstprj1  21702  minveclem3b  21709  minveclem4  21713  ivthlem2  21730  ivthlem3  21731  ovollb2lem  21765  ovoliunlem1  21779  ovolscalem1  21790  ovolicc1  21793  ovolicc2lem4  21797  ovolicc2  21799  ovolicc  21800  voliunlem2  21827  ovolioo  21844  ioorcl2  21847  uniioovol  21854  uniioombllem2  21858  uniioombllem3a  21859  uniioombllem3  21860  uniioombllem4  21861  uniioombllem6  21863  opnmbllem  21876  volcn  21881  vitalilem2  21884  ismbf3d  21927  mbfaddlem  21933  i1fadd  21968  itg1addlem4  21972  mbfi1fseqlem6  21993  itg2seq  22015  itg2split  22022  itg2cnlem2  22035  itg2cn  22036  itgrevallem1  22067  dvcjbr  22218  dvferm1lem  22251  dvferm2lem  22253  cmvth  22258  mvth  22259  dvlip  22260  dvlip2  22262  c1liplem1  22263  dvgt0  22271  dvlt0  22272  dvge0  22273  dvle  22274  dvivthlem1  22275  lhop1lem  22280  lhop  22283  dvcnvrelem1  22284  dvcnvrelem2  22285  dvcnvre  22286  dvcvx  22287  dvfsumle  22288  dvfsumge  22289  dvfsumrlimf  22292  dvfsumlem2  22294  dvfsumlem3  22295  dvfsumlem4  22296  dvfsum2  22301  ftc1a  22304  ftc1lem4  22306  coe1mul3  22366  ply1divex  22403  plydivex  22558  aalioulem2  22594  aalioulem3  22595  aalioulem4  22596  aalioulem5  22597  aalioulem6  22598  aaliou3lem7  22610  taylthlem2  22634  mtest  22664  pilem2  22712  tangtx  22763  cosordlem  22783  efif1olem2  22795  logcnlem3  22890  logcnlem4  22891  isosctrlem2  23018  chordthmlem2  23029  chordthmlem4  23031  heron  23034  atanlogsublem  23111  atantan  23119  birthdaylem3  23148  logdifbnd  23188  emcllem1  23190  emcllem2  23191  emcllem5  23194  emcllem6  23195  harmonicbnd4  23205  fsumharmonic  23206  ftalem2  23212  ftalem5  23215  chpub  23360  logfaclbnd  23362  logfacbnd3  23363  logexprlim  23365  bposlem1  23424  bposlem9  23432  lgseisenlem1  23489  lgsquadlem1  23494  chtppilimlem1  23523  vmadivsum  23532  vmadivsumb  23533  rplogsumlem1  23534  rplogsumlem2  23535  rpvmasumlem  23537  dchrisumlem2  23540  dchrisum0re  23563  rplogsum  23577  mulogsumlem  23581  mulog2sumlem1  23584  vmalogdivsum2  23588  vmalogdivsum  23589  2vmadivsumlem  23590  log2sumbnd  23594  selbergb  23599  selberg2lem  23600  selberg2b  23602  chpdifbndlem1  23603  selberg3lem1  23607  selberg3lem2  23608  selberg3  23609  selberg4lem1  23610  selberg4  23611  pntrf  23613  pntrmax  23614  pntrsumo1  23615  selberg3r  23619  selberg4r  23620  selberg34r  23621  pntrlog2bndlem1  23627  pntrlog2bndlem2  23628  pntrlog2bndlem3  23629  pntrlog2bndlem4  23630  pntrlog2bndlem5  23631  pntrlog2bndlem6  23633  pntrlog2bnd  23634  pntpbnd1a  23635  pntpbnd2  23637  pntibndlem2  23641  pntlemg  23648  pntlemn  23650  pntlemj  23653  pntlemf  23655  pntlemo  23657  pntlem3  23659  pntleml  23661  ttgcontlem1  24053  eqeelen  24072  brbtwn2  24073  colinearalg  24078  axcgrid  24084  axsegconlem1  24085  axsegconlem3  24087  axsegconlem8  24092  axsegconlem9  24093  axsegconlem10  24094  ax5seglem3a  24098  ax5seg  24106  axpaschlem  24108  axcontlem8  24139  clwlkisclwwlklem2fv2  24648  clwlkisclwwlklem2a4  24649  clwlkisclwwlklem2a  24650  extwwlkfablem2  24943  nvabs  25441  dipcj  25492  minvecolem4  25661  lt2addrd  27428  xlt2addrd  27443  fzsplit3  27464  bcm1n  27465  bhmafibid1  27498  2sqmod  27502  cnre2csqlem  27758  tpr2rico  27760  dya2ub  28107  dya2icoseg  28114  ballotlemfcc  28298  ballotlemfrcn0  28334  sgnsub  28349  signslema  28385  lgamgulmlem2  28438  lgamgulmlem3  28439  lgamucov  28446  relgamcl  28470  subfacval3  28499  bpoly4  29789  supaddc  30009  opnmbllem0  30018  mblfinlem3  30021  mblfinlem4  30022  itg2addnclem  30034  itg2addnclem3  30036  itg2gt0cn  30038  ftc1cnnclem  30056  areacirclem1  30075  areacirclem2  30076  areacirclem4  30078  areacirclem5  30079  areacirc  30080  cntotbnd  30260  rrnmet  30293  rrndstprj1  30294  rrndstprj2  30295  icodiamlt  30724  irrapxlem2  30727  irrapxlem3  30728  irrapxlem4  30729  irrapxlem5  30730  pellexlem2  30734  pellexlem6  30738  pell1qrgaplem  30777  rmspecfund  30813  rmspecpos  30820  jm2.24nn  30865  jm2.17c  30868  fzmaxdif  30887  acongeq  30889  modabsdifz  30895  jm3.1lem2  30928  areaquad  31153  cvgdvgrat  31163  hashnzfzclim  31196  oddfl  31404  lefldiveq  31427  fperiodmul  31449  iccshift  31490  iooshift  31494  fmul01lt1lem2  31503  climinf  31516  sumnnodd  31540  ltmod  31548  lptre2pt  31550  fperdvper  31615  dvbdfbdioolem1  31625  dvbdfbdioolem2  31626  dvbdfbdioo  31627  ioodvbdlimc1lem1  31628  ioodvbdlimc1lem2  31629  ioodvbdlimc2lem  31631  iblspltprt  31658  itgspltprt  31664  itgiccshift  31665  itgperiod  31666  itgsbtaddcnst  31667  stoweidlem1  31668  stoweidlem11  31678  stoweidlem12  31679  stoweidlem13  31680  stoweidlem14  31681  stoweidlem23  31690  stoweidlem24  31691  stoweidlem25  31692  stoweidlem26  31693  stoweidlem34  31701  stoweidlem40  31707  stoweidlem41  31708  stoweidlem42  31709  stoweidlem45  31712  stoweidlem60  31727  stoweidlem62  31729  wallispilem3  31734  wallispilem4  31735  wallispi  31737  wallispi2lem1  31738  stirlinglem5  31745  stirlinglem11  31751  stirlinglem12  31752  dirkercncflem1  31770  fourierdlem4  31778  fourierdlem6  31780  fourierdlem7  31781  fourierdlem9  31783  fourierdlem13  31787  fourierdlem14  31788  fourierdlem15  31789  fourierdlem19  31793  fourierdlem26  31800  fourierdlem35  31809  fourierdlem39  31813  fourierdlem40  31814  fourierdlem41  31815  fourierdlem42  31816  fourierdlem48  31822  fourierdlem49  31823  fourierdlem50  31824  fourierdlem51  31825  fourierdlem56  31830  fourierdlem57  31831  fourierdlem59  31833  fourierdlem60  31834  fourierdlem61  31835  fourierdlem63  31837  fourierdlem64  31838  fourierdlem65  31839  fourierdlem66  31840  fourierdlem68  31842  fourierdlem71  31845  fourierdlem72  31846  fourierdlem73  31847  fourierdlem74  31848  fourierdlem75  31849  fourierdlem76  31850  fourierdlem78  31852  fourierdlem79  31853  fourierdlem81  31855  fourierdlem82  31856  fourierdlem83  31857  fourierdlem84  31858  fourierdlem88  31862  fourierdlem89  31863  fourierdlem90  31864  fourierdlem91  31865  fourierdlem92  31866  fourierdlem93  31867  fourierdlem95  31869  fourierdlem97  31871  fourierdlem101  31875  fourierdlem103  31877  fourierdlem104  31878  fourierdlem107  31881  fourierdlem109  31883  fourierdlem111  31885  fouriersw  31899  ltsubsubaddltsub  32158  2elfz2melfz  32168  ply1mulgsumlem2  32697  imo72b2lem0  37587
  Copyright terms: Public domain W3C validator