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

Theorem resubcld 9455
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 9355 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  -  B
)  e.  RR )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  -  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725  (class class class)co 6073   RRcr 8979    - cmin 9281
This theorem is referenced by:  ltsubadd  9488  lesubadd  9490  lesub1  9512  lesub2  9513  ltsub1  9514  ltsub2  9515  lt2sub  9516  le2sub  9517  ltmul1a  9849  cru  9982  qbtwnre  10775  lincmb01cmp  11028  iccf1o  11029  xov1plusxeqvd  11031  intfracq  11230  fldiv  11231  modlt  11248  modsubdir  11275  serle  11368  expmulnbnd  11501  discr  11506  fzsdom2  11683  crre  11909  remullem  11923  sqrlem7  12044  absrdbnd  12135  fzomaxdiflem  12136  caubnd2  12151  amgm2  12163  mulcn2  12379  reccn2  12380  rlimo1  12400  climle  12423  climsqz  12424  climsqz2  12425  rlimle  12431  isercolllem1  12448  climsup  12453  caucvgrlem  12456  caucvgrlem2  12458  iseraltlem2  12466  iseraltlem3  12467  iseralt  12468  fsumle  12568  cvgcmp  12585  cvgcmpce  12587  eflt  12708  resinhcl  12747  tanhlt1  12751  sin01bnd  12776  sin01gt0  12781  moddvds  12849  bitscmp  12940  bitsinv1lem  12943  smueqlem  12992  pcbc  13259  4sqlem15  13317  blss2ps  18423  blss2  18424  blssps  18444  blss  18445  nm2dif  18661  nlmvscnlem2  18711  nrginvrcnlem  18716  iccntr  18842  icccmplem2  18844  metdstri  18871  cnllycmp  18971  evth  18974  lebnumii  18981  ipcnlem2  19188  cncmet  19265  minveclem3b  19319  minveclem4  19323  ivthlem2  19339  ivthlem3  19340  ovollb2lem  19374  ovoliunlem1  19388  ovolscalem1  19399  ovolicc1  19402  ovolicc2lem4  19406  ovolicc2  19408  ovolicc  19409  voliunlem2  19435  ovolioo  19452  ioorcl2  19454  uniioovol  19461  uniioombllem2  19465  uniioombllem3a  19466  uniioombllem3  19467  uniioombllem4  19468  uniioombllem6  19470  opnmbllem  19483  volcn  19488  vitalilem2  19491  ismbf3d  19536  mbfaddlem  19542  i1fadd  19577  itg1addlem4  19581  mbfi1fseqlem6  19602  itg2seq  19624  itg2split  19631  itg2cnlem2  19644  itg2cn  19645  itgrevallem1  19676  dvcjbr  19825  dvferm1lem  19858  dvferm2lem  19860  cmvth  19865  mvth  19866  dvlip  19867  dvlip2  19869  c1liplem1  19870  dvgt0  19878  dvlt0  19879  dvge0  19880  dvle  19881  dvivthlem1  19882  lhop1lem  19887  lhop  19890  dvcnvrelem1  19891  dvcnvrelem2  19892  dvcnvre  19893  dvcvx  19894  dvfsumle  19895  dvfsumge  19896  dvfsumrlimf  19899  dvfsumlem2  19901  dvfsumlem3  19902  dvfsumlem4  19903  dvfsum2  19908  ftc1a  19911  ftc1lem4  19913  coe1mul3  20012  ply1divex  20049  plydivex  20204  aalioulem2  20240  aalioulem3  20241  aalioulem4  20242  aalioulem5  20243  aalioulem6  20244  aaliou3lem7  20256  taylthlem2  20280  mtest  20310  pilem2  20358  tangtx  20403  cosordlem  20423  efif1olem2  20435  logcnlem3  20525  logcnlem4  20526  isosctrlem2  20653  chordthmlem2  20664  chordthmlem4  20666  atanlogsublem  20745  atantan  20753  birthdaylem3  20782  logdifbnd  20822  emcllem1  20824  emcllem2  20825  emcllem5  20828  emcllem6  20829  harmonicbnd4  20839  fsumharmonic  20840  ftalem2  20846  ftalem5  20849  chpub  20994  logfaclbnd  20996  logfacbnd3  20997  logexprlim  20999  bposlem1  21058  bposlem9  21066  lgseisenlem1  21123  lgsquadlem1  21128  chtppilimlem1  21157  vmadivsum  21166  vmadivsumb  21167  rplogsumlem1  21168  rplogsumlem2  21169  rpvmasumlem  21171  dchrisumlem2  21174  dchrisum0re  21197  rplogsum  21211  mulogsumlem  21215  mulog2sumlem1  21218  vmalogdivsum2  21222  vmalogdivsum  21223  2vmadivsumlem  21224  log2sumbnd  21228  selbergb  21233  selberg2lem  21234  selberg2b  21236  chpdifbndlem1  21237  selberg3lem1  21241  selberg3lem2  21242  selberg3  21243  selberg4lem1  21244  selberg4  21245  pntrf  21247  pntrmax  21248  pntrsumo1  21249  selberg3r  21253  selberg4r  21254  selberg34r  21255  pntrlog2bndlem1  21261  pntrlog2bndlem2  21262  pntrlog2bndlem3  21263  pntrlog2bndlem4  21264  pntrlog2bndlem5  21265  pntrlog2bndlem6  21267  pntrlog2bnd  21268  pntpbnd1a  21269  pntpbnd2  21271  pntibndlem2  21275  pntlemg  21282  pntlemn  21284  pntlemj  21287  pntlemf  21289  pntlemo  21291  pntlem3  21293  pntleml  21295  nvabs  22152  dipcj  22203  minvecolem4  22372  lt2addrd  24105  xlt2addrd  24114  fzsplit3  24140  bcm1n  24141  cnre2csqlem  24298  tpr2rico  24300  dya2ub  24610  dya2icoseg  24617  ballotlemfcc  24741  ballotlemfrcn0  24777  lgamgulmlem2  24804  lgamgulmlem3  24805  lgamucov  24812  relgamcl  24836  subfacval3  24865  eqeelen  25808  brbtwn2  25809  colinearalg  25814  axcgrid  25820  axsegconlem1  25821  axsegconlem3  25823  axsegconlem8  25828  axsegconlem9  25829  axsegconlem10  25830  ax5seglem3a  25834  ax5seg  25842  axpaschlem  25844  axcontlem8  25875  bpoly4  26070  supaddc  26201  mblfinlem  26207  mblfinlem2  26208  mblfinlem3  26209  itg2addnclem  26219  itg2addnclem3  26221  itg2gt0cn  26223  ftc1cnnclem  26241  dvreasin  26243  areacirclem2  26245  areacirclem3  26246  areacirclem4  26247  areacirclem5  26249  areacirclem6  26250  areacirc  26251  cntotbnd  26459  rrnmet  26492  rrndstprj1  26493  rrndstprj2  26494  icodiamlt  26837  irrapxlem2  26840  irrapxlem3  26841  irrapxlem4  26842  irrapxlem5  26843  pellexlem2  26847  pellexlem6  26851  pell1qrgaplem  26890  rmspecfund  26926  rmspecpos  26933  jm2.24nn  26978  jm2.17c  26981  fzmaxdif  27000  acongeq  27002  modabsdifz  27010  jm3.1lem2  27043  fmul01lt1lem2  27646  climinf  27663  stoweidlem1  27681  stoweidlem11  27691  stoweidlem12  27692  stoweidlem13  27693  stoweidlem14  27694  stoweidlem23  27703  stoweidlem24  27704  stoweidlem25  27705  stoweidlem26  27706  stoweidlem34  27714  stoweidlem40  27720  stoweidlem41  27721  stoweidlem42  27722  stoweidlem45  27725  stoweidlem60  27740  stoweidlem62  27742  wallispilem3  27747  wallispilem4  27748  wallispi  27750  wallispi2lem1  27751  stirlinglem5  27758  stirlinglem11  27764  stirlinglem12  27765  2elfz2melfz  28065  modprm0  28158
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-resscn 9037  ax-1cn 9038  ax-icn 9039  ax-addcl 9040  ax-addrcl 9041  ax-mulcl 9042  ax-mulrcl 9043  ax-mulcom 9044  ax-addass 9045  ax-mulass 9046  ax-distr 9047  ax-i2m1 9048  ax-1ne0 9049  ax-1rid 9050  ax-rnegex 9051  ax-rrecex 9052  ax-cnre 9053  ax-pre-lttri 9054  ax-pre-lttrn 9055  ax-pre-ltadd 9056
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-po 4495  df-so 4496  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-riota 6541  df-er 6897  df-en 7102  df-dom 7103  df-sdom 7104  df-pnf 9112  df-mnf 9113  df-ltxr 9115  df-sub 9283  df-neg 9284
  Copyright terms: Public domain W3C validator