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

Theorem resubcld 9399
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 9299 . 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 1717  (class class class)co 6022   RRcr 8924    - cmin 9225
This theorem is referenced by:  ltsubadd  9432  lesubadd  9434  lesub1  9456  lesub2  9457  ltsub1  9458  ltsub2  9459  lt2sub  9460  le2sub  9461  ltmul1a  9793  cru  9926  qbtwnre  10719  lincmb01cmp  10972  iccf1o  10973  xov1plusxeqvd  10975  intfracq  11169  fldiv  11170  modlt  11187  modsubdir  11214  serle  11307  expmulnbnd  11440  discr  11445  fzsdom2  11622  crre  11848  remullem  11862  sqrlem7  11983  absrdbnd  12074  fzomaxdiflem  12075  caubnd2  12090  amgm2  12102  mulcn2  12318  reccn2  12319  rlimo1  12339  climle  12362  climsqz  12363  climsqz2  12364  rlimle  12370  isercolllem1  12387  climsup  12392  caucvgrlem  12395  caucvgrlem2  12397  iseraltlem2  12405  iseraltlem3  12406  iseralt  12407  fsumle  12507  cvgcmp  12524  cvgcmpce  12526  eflt  12647  resinhcl  12686  tanhlt1  12690  sin01bnd  12715  sin01gt0  12720  moddvds  12788  bitscmp  12879  bitsinv1lem  12882  smueqlem  12931  pcbc  13198  4sqlem15  13256  blss2  18335  blss  18348  nm2dif  18544  nlmvscnlem2  18594  nrginvrcnlem  18599  iccntr  18725  icccmplem2  18727  metdstri  18754  cnllycmp  18854  evth  18857  lebnumii  18864  ipcnlem2  19071  cncmet  19146  minveclem3b  19198  minveclem4  19202  ivthlem2  19218  ivthlem3  19219  ovollb2lem  19253  ovoliunlem1  19267  ovolscalem1  19278  ovolicc1  19281  ovolicc2lem4  19285  ovolicc2  19287  ovolicc  19288  voliunlem2  19314  ovolioo  19331  ioorcl2  19333  uniioovol  19340  uniioombllem2  19344  uniioombllem3a  19345  uniioombllem3  19346  uniioombllem4  19347  uniioombllem6  19349  opnmbllem  19362  volcn  19367  vitalilem2  19370  ismbf3d  19415  mbfaddlem  19421  i1fadd  19456  itg1addlem4  19460  mbfi1fseqlem6  19481  itg2seq  19503  itg2split  19510  itg2cnlem2  19523  itg2cn  19524  itgrevallem1  19555  dvcjbr  19704  dvferm1lem  19737  dvferm2lem  19739  cmvth  19744  mvth  19745  dvlip  19746  dvlip2  19748  c1liplem1  19749  dvgt0  19757  dvlt0  19758  dvge0  19759  dvle  19760  dvivthlem1  19761  lhop1lem  19766  lhop  19769  dvcnvrelem1  19770  dvcnvrelem2  19771  dvcnvre  19772  dvcvx  19773  dvfsumle  19774  dvfsumge  19775  dvfsumrlimf  19778  dvfsumlem2  19780  dvfsumlem3  19781  dvfsumlem4  19782  dvfsum2  19787  ftc1a  19790  ftc1lem4  19792  coe1mul3  19891  ply1divex  19928  plydivex  20083  aalioulem2  20119  aalioulem3  20120  aalioulem4  20121  aalioulem5  20122  aalioulem6  20123  aaliou3lem7  20135  taylthlem2  20159  mtest  20189  pilem2  20237  tangtx  20282  cosordlem  20302  efif1olem2  20314  logcnlem3  20404  logcnlem4  20405  isosctrlem2  20532  chordthmlem2  20543  chordthmlem4  20545  atanlogsublem  20624  atantan  20632  birthdaylem3  20661  logdifbnd  20701  emcllem1  20703  emcllem2  20704  emcllem5  20707  emcllem6  20708  harmonicbnd4  20718  fsumharmonic  20719  ftalem2  20725  ftalem5  20728  chpub  20873  logfaclbnd  20875  logfacbnd3  20876  logexprlim  20878  bposlem1  20937  bposlem9  20945  lgseisenlem1  21002  lgsquadlem1  21007  chtppilimlem1  21036  vmadivsum  21045  vmadivsumb  21046  rplogsumlem1  21047  rplogsumlem2  21048  rpvmasumlem  21050  dchrisumlem2  21053  dchrisum0re  21076  rplogsum  21090  mulogsumlem  21094  mulog2sumlem1  21097  vmalogdivsum2  21101  vmalogdivsum  21102  2vmadivsumlem  21103  log2sumbnd  21107  selbergb  21112  selberg2lem  21113  selberg2b  21115  chpdifbndlem1  21116  selberg3lem1  21120  selberg3lem2  21121  selberg3  21122  selberg4lem1  21123  selberg4  21124  pntrf  21126  pntrmax  21127  pntrsumo1  21128  selberg3r  21132  selberg4r  21133  selberg34r  21134  pntrlog2bndlem1  21140  pntrlog2bndlem2  21141  pntrlog2bndlem3  21142  pntrlog2bndlem4  21143  pntrlog2bndlem5  21144  pntrlog2bndlem6  21146  pntrlog2bnd  21147  pntpbnd1a  21148  pntpbnd2  21150  pntibndlem2  21154  pntlemg  21161  pntlemn  21163  pntlemj  21166  pntlemf  21168  pntlemo  21170  pntlem3  21172  pntleml  21174  nvabs  22012  dipcj  22063  minvecolem4  22232  lt2addrd  23958  xlt2addrd  23962  fzsplit3  23988  bcm1n  23989  cnre2csqlem  24114  tpr2rico  24116  dya2ub  24416  dya2icoseg  24423  ballotlemfcc  24532  ballotlemfrcn0  24568  lgamgulmlem2  24595  lgamgulmlem3  24596  lgamucov  24603  relgamcl  24627  subfacval3  24656  eqeelen  25559  brbtwn2  25560  colinearalg  25565  axcgrid  25571  axsegconlem1  25572  axsegconlem3  25574  axsegconlem8  25579  axsegconlem9  25580  axsegconlem10  25581  ax5seglem3a  25585  ax5seg  25593  axpaschlem  25595  axcontlem8  25626  bpoly4  25821  supaddc  25949  itg2addnclem  25959  itg2addnc  25961  itg2gt0cn  25962  ftc1cnnclem  25980  dvreasin  25982  areacirclem2  25984  areacirclem3  25985  areacirclem4  25986  areacirclem5  25988  areacirclem6  25989  areacirc  25990  cntotbnd  26198  rrnmet  26231  rrndstprj1  26232  rrndstprj2  26233  icodiamlt  26576  irrapxlem2  26579  irrapxlem3  26580  irrapxlem4  26581  irrapxlem5  26582  pellexlem2  26586  pellexlem6  26590  pell1qrgaplem  26629  rmspecfund  26665  rmspecpos  26672  jm2.24nn  26717  jm2.17c  26720  fzmaxdif  26739  acongeq  26741  modabsdifz  26749  jm3.1lem2  26782  fmul01lt1lem2  27385  climinf  27402  stoweidlem1  27420  stoweidlem11  27430  stoweidlem12  27431  stoweidlem13  27432  stoweidlem14  27433  stoweidlem23  27442  stoweidlem24  27443  stoweidlem25  27444  stoweidlem26  27445  stoweidlem34  27453  stoweidlem40  27459  stoweidlem41  27460  stoweidlem42  27461  stoweidlem45  27464  stoweidlem60  27479  stoweidlem62  27481  wallispilem3  27486  wallispilem4  27487  wallispi  27489  wallispi2lem1  27490  stirlinglem5  27497  stirlinglem11  27503  stirlinglem12  27504
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643  ax-resscn 8982  ax-1cn 8983  ax-icn 8984  ax-addcl 8985  ax-addrcl 8986  ax-mulcl 8987  ax-mulrcl 8988  ax-mulcom 8989  ax-addass 8990  ax-mulass 8991  ax-distr 8992  ax-i2m1 8993  ax-1ne0 8994  ax-1rid 8995  ax-rnegex 8996  ax-rrecex 8997  ax-cnre 8998  ax-pre-lttri 8999  ax-pre-lttrn 9000  ax-pre-ltadd 9001
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-nel 2555  df-ral 2656  df-rex 2657  df-reu 2658  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-mpt 4211  df-id 4441  df-po 4446  df-so 4447  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-ov 6025  df-oprab 6026  df-mpt2 6027  df-riota 6487  df-er 6843  df-en 7048  df-dom 7049  df-sdom 7050  df-pnf 9057  df-mnf 9058  df-ltxr 9060  df-sub 9227  df-neg 9228
  Copyright terms: Public domain W3C validator