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

Theorem resubcld 9227
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 9127 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  -  B
)  e.  RR )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A  -  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696  (class class class)co 5874   RRcr 8752    - cmin 9053
This theorem is referenced by:  ltsubadd  9260  lesubadd  9262  lesub1  9284  lesub2  9285  ltsub1  9286  ltsub2  9287  lt2sub  9288  le2sub  9289  ltmul1a  9621  cru  9754  qbtwnre  10542  lincmb01cmp  10793  iccf1o  10794  xov1plusxeqvd  10796  intfracq  10979  fldiv  10980  modlt  10997  modsubdir  11024  serle  11117  expmulnbnd  11249  discr  11254  fzsdom2  11398  crre  11615  remullem  11629  sqrlem7  11750  absrdbnd  11841  fzomaxdiflem  11842  caubnd2  11857  amgm2  11869  mulcn2  12085  reccn2  12086  rlimo1  12106  climle  12129  climsqz  12130  climsqz2  12131  rlimle  12137  isercolllem1  12154  climsup  12159  caucvgrlem  12161  caucvgrlem2  12163  iseraltlem2  12171  iseraltlem3  12172  iseralt  12173  fsumle  12273  cvgcmp  12290  cvgcmpce  12292  eflt  12413  resinhcl  12452  tanhlt1  12456  sin01bnd  12481  sin01gt0  12486  moddvds  12554  bitscmp  12645  bitsinv1lem  12648  smueqlem  12697  pcbc  12964  4sqlem15  13022  blss2  17975  blss  17988  nm2dif  18162  nlmvscnlem2  18212  nrginvrcnlem  18217  iccntr  18342  icccmplem2  18344  metdstri  18371  cnllycmp  18470  evth  18473  lebnumii  18480  ipcnlem2  18687  cncmet  18760  minveclem3b  18808  minveclem4  18812  ivthlem2  18828  ivthlem3  18829  ovollb2lem  18863  ovoliunlem1  18877  ovolscalem1  18888  ovolicc1  18891  ovolicc2lem4  18895  ovolicc2  18897  ovolicc  18898  voliunlem2  18924  ovolioo  18941  ioorcl2  18943  uniioovol  18950  uniioombllem2  18954  uniioombllem3a  18955  uniioombllem3  18956  uniioombllem4  18957  uniioombllem6  18959  opnmbllem  18972  volcn  18977  vitalilem2  18980  ismbf3d  19025  mbfaddlem  19031  i1fadd  19066  itg1addlem4  19070  mbfi1fseqlem6  19091  itg2seq  19113  itg2split  19120  itg2cnlem2  19133  itg2cn  19134  itgrevallem1  19165  dvcjbr  19314  dvferm1lem  19347  dvferm2lem  19349  cmvth  19354  mvth  19355  dvlip  19356  dvlip2  19358  c1liplem1  19359  dvgt0  19367  dvlt0  19368  dvge0  19369  dvle  19370  dvivthlem1  19371  lhop1lem  19376  lhop  19379  dvcnvrelem1  19380  dvcnvrelem2  19381  dvcnvre  19382  dvcvx  19383  dvfsumle  19384  dvfsumge  19385  dvfsumrlimf  19388  dvfsumlem2  19390  dvfsumlem3  19391  dvfsumlem4  19392  dvfsum2  19397  ftc1a  19400  ftc1lem4  19402  coe1mul3  19501  ply1divex  19538  plydivex  19693  aalioulem2  19729  aalioulem3  19730  aalioulem4  19731  aalioulem5  19732  aalioulem6  19733  aaliou3lem7  19745  taylthlem2  19769  mtest  19797  pilem2  19844  tangtx  19889  cosordlem  19909  efif1olem2  19921  logcnlem3  20007  logcnlem4  20008  isosctrlem2  20135  chordthmlem2  20146  chordthmlem4  20148  atanlogsublem  20227  atantan  20235  birthdaylem3  20264  logdifbnd  20304  emcllem1  20305  emcllem2  20306  emcllem5  20309  emcllem6  20310  harmonicbnd4  20320  fsumharmonic  20321  ftalem2  20327  ftalem5  20330  chpub  20475  logfaclbnd  20477  logfacbnd3  20478  logexprlim  20480  bposlem1  20539  bposlem9  20547  lgseisenlem1  20604  lgsquadlem1  20609  chtppilimlem1  20638  vmadivsum  20647  vmadivsumb  20648  rplogsumlem1  20649  rplogsumlem2  20650  rpvmasumlem  20652  dchrisumlem2  20655  dchrisum0re  20678  rplogsum  20692  mulogsumlem  20696  mulog2sumlem1  20699  vmalogdivsum2  20703  vmalogdivsum  20704  2vmadivsumlem  20705  log2sumbnd  20709  selbergb  20714  selberg2lem  20715  selberg2b  20717  chpdifbndlem1  20718  selberg3lem1  20722  selberg3lem2  20723  selberg3  20724  selberg4lem1  20725  selberg4  20726  pntrf  20728  pntrmax  20729  pntrsumo1  20730  selberg3r  20734  selberg4r  20735  selberg34r  20736  pntrlog2bndlem1  20742  pntrlog2bndlem2  20743  pntrlog2bndlem3  20744  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntrlog2bnd  20749  pntpbnd1a  20750  pntpbnd2  20752  pntibndlem2  20756  pntlemg  20763  pntlemn  20765  pntlemj  20768  pntlemf  20770  pntlemo  20772  pntlem3  20774  pntleml  20776  nvabs  21255  dipcj  21306  minvecolem4  21475  fzsplit3  23047  bcm1n  23048  ballotlemfcc  23068  ballotlemfrcn0  23104  lt2addrd  23264  xlt2addrd  23268  cnre2csqlem  23309  cnre2csqima  23310  tpr2rico  23311  dya2ub  23590  dya2iocseg  23594  subfacval3  23735  faclimlem5  24121  eqeelen  24604  brbtwn2  24605  colinearalg  24610  axcgrid  24616  axsegconlem1  24617  axsegconlem3  24619  axsegconlem8  24624  axsegconlem9  24625  axsegconlem10  24626  ax5seglem3a  24630  ax5seg  24638  axpaschlem  24640  axcontlem8  24671  bpoly4  24866  supaddc  24995  itg2addnclem  25003  itg2addnc  25005  itg2gt0cn  25006  ftc1cnnclem  25024  dvreasin  25026  areacirclem2  25028  areacirclem3  25029  areacirclem4  25030  areacirclem5  25032  areacirclem6  25033  areacirc  25034  altretop  25703  msr3  25708  lvsovso  25729  subclrvd  25777  cntotbnd  26623  rrnmet  26656  rrndstprj1  26657  rrndstprj2  26658  icodiamlt  27008  irrapxlem2  27011  irrapxlem3  27012  irrapxlem4  27013  irrapxlem5  27014  pellexlem2  27018  pellexlem6  27022  pell1qrgaplem  27061  rmspecfund  27097  rmspecpos  27104  jm2.24nn  27149  jm2.17c  27152  fzmaxdif  27171  acongeq  27173  modabsdifz  27181  jm3.1lem2  27214  climinf  27835  stoweidlem12  27864  wallispilem3  27919  wallispilem4  27920  wallispi  27922  wallispi2lem1  27923  stirlinglem5  27930  stirlinglem11  27936  stirlinglem12  27937
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-po 4330  df-so 4331  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-riota 6320  df-er 6676  df-en 6880  df-dom 6881  df-sdom 6882  df-pnf 8885  df-mnf 8886  df-ltxr 8888  df-sub 9055  df-neg 9056
  Copyright terms: Public domain W3C validator