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

Theorem resubcld 9470
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 9370 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  -  B
)  e.  RR )
41, 2, 3syl2anc 644 1  |-  ( ph  ->  ( A  -  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726  (class class class)co 6084   RRcr 8994    - cmin 9296
This theorem is referenced by:  ltsubadd  9503  lesubadd  9505  lesub1  9527  lesub2  9528  ltsub1  9529  ltsub2  9530  lt2sub  9531  le2sub  9532  ltmul1a  9864  cru  9997  qbtwnre  10790  lincmb01cmp  11043  iccf1o  11044  xov1plusxeqvd  11046  intfracq  11245  fldiv  11246  modlt  11263  modsubdir  11290  serle  11383  expmulnbnd  11516  discr  11521  fzsdom2  11698  crre  11924  remullem  11938  sqrlem7  12059  absrdbnd  12150  fzomaxdiflem  12151  caubnd2  12166  amgm2  12178  mulcn2  12394  reccn2  12395  rlimo1  12415  climle  12438  climsqz  12439  climsqz2  12440  rlimle  12446  isercolllem1  12463  climsup  12468  caucvgrlem  12471  caucvgrlem2  12473  iseraltlem2  12481  iseraltlem3  12482  iseralt  12483  fsumle  12583  cvgcmp  12600  cvgcmpce  12602  eflt  12723  resinhcl  12762  tanhlt1  12766  sin01bnd  12791  sin01gt0  12796  moddvds  12864  bitscmp  12955  bitsinv1lem  12958  smueqlem  13007  pcbc  13274  4sqlem15  13332  blss2ps  18438  blss2  18439  blssps  18459  blss  18460  nm2dif  18676  nlmvscnlem2  18726  nrginvrcnlem  18731  iccntr  18857  icccmplem2  18859  metdstri  18886  cnllycmp  18986  evth  18989  lebnumii  18996  ipcnlem2  19203  cncmet  19280  minveclem3b  19334  minveclem4  19338  ivthlem2  19354  ivthlem3  19355  ovollb2lem  19389  ovoliunlem1  19403  ovolscalem1  19414  ovolicc1  19417  ovolicc2lem4  19421  ovolicc2  19423  ovolicc  19424  voliunlem2  19450  ovolioo  19467  ioorcl2  19469  uniioovol  19476  uniioombllem2  19480  uniioombllem3a  19481  uniioombllem3  19482  uniioombllem4  19483  uniioombllem6  19485  opnmbllem  19498  volcn  19503  vitalilem2  19506  ismbf3d  19549  mbfaddlem  19555  i1fadd  19590  itg1addlem4  19594  mbfi1fseqlem6  19615  itg2seq  19637  itg2split  19644  itg2cnlem2  19657  itg2cn  19658  itgrevallem1  19689  dvcjbr  19840  dvferm1lem  19873  dvferm2lem  19875  cmvth  19880  mvth  19881  dvlip  19882  dvlip2  19884  c1liplem1  19885  dvgt0  19893  dvlt0  19894  dvge0  19895  dvle  19896  dvivthlem1  19897  lhop1lem  19902  lhop  19905  dvcnvrelem1  19906  dvcnvrelem2  19907  dvcnvre  19908  dvcvx  19909  dvfsumle  19910  dvfsumge  19911  dvfsumrlimf  19914  dvfsumlem2  19916  dvfsumlem3  19917  dvfsumlem4  19918  dvfsum2  19923  ftc1a  19926  ftc1lem4  19928  coe1mul3  20027  ply1divex  20064  plydivex  20219  aalioulem2  20255  aalioulem3  20256  aalioulem4  20257  aalioulem5  20258  aalioulem6  20259  aaliou3lem7  20271  taylthlem2  20295  mtest  20325  pilem2  20373  tangtx  20418  cosordlem  20438  efif1olem2  20450  logcnlem3  20540  logcnlem4  20541  isosctrlem2  20668  chordthmlem2  20679  chordthmlem4  20681  atanlogsublem  20760  atantan  20768  birthdaylem3  20797  logdifbnd  20837  emcllem1  20839  emcllem2  20840  emcllem5  20843  emcllem6  20844  harmonicbnd4  20854  fsumharmonic  20855  ftalem2  20861  ftalem5  20864  chpub  21009  logfaclbnd  21011  logfacbnd3  21012  logexprlim  21014  bposlem1  21073  bposlem9  21081  lgseisenlem1  21138  lgsquadlem1  21143  chtppilimlem1  21172  vmadivsum  21181  vmadivsumb  21182  rplogsumlem1  21183  rplogsumlem2  21184  rpvmasumlem  21186  dchrisumlem2  21189  dchrisum0re  21212  rplogsum  21226  mulogsumlem  21230  mulog2sumlem1  21233  vmalogdivsum2  21237  vmalogdivsum  21238  2vmadivsumlem  21239  log2sumbnd  21243  selbergb  21248  selberg2lem  21249  selberg2b  21251  chpdifbndlem1  21252  selberg3lem1  21256  selberg3lem2  21257  selberg3  21258  selberg4lem1  21259  selberg4  21260  pntrf  21262  pntrmax  21263  pntrsumo1  21264  selberg3r  21268  selberg4r  21269  selberg34r  21270  pntrlog2bndlem1  21276  pntrlog2bndlem2  21277  pntrlog2bndlem3  21278  pntrlog2bndlem4  21279  pntrlog2bndlem5  21280  pntrlog2bndlem6  21282  pntrlog2bnd  21283  pntpbnd1a  21284  pntpbnd2  21286  pntibndlem2  21290  pntlemg  21297  pntlemn  21299  pntlemj  21302  pntlemf  21304  pntlemo  21306  pntlem3  21308  pntleml  21310  nvabs  22167  dipcj  22218  minvecolem4  22387  lt2addrd  24120  xlt2addrd  24129  fzsplit3  24155  bcm1n  24156  cnre2csqlem  24313  tpr2rico  24315  dya2ub  24625  dya2icoseg  24632  ballotlemfcc  24756  ballotlemfrcn0  24792  lgamgulmlem2  24819  lgamgulmlem3  24820  lgamucov  24827  relgamcl  24851  subfacval3  24880  eqeelen  25848  brbtwn2  25849  colinearalg  25854  axcgrid  25860  axsegconlem1  25861  axsegconlem3  25863  axsegconlem8  25868  axsegconlem9  25869  axsegconlem10  25870  ax5seglem3a  25874  ax5seg  25882  axpaschlem  25884  axcontlem8  25915  bpoly4  26110  supaddc  26245  opnmbllem0  26254  mblfinlem3  26257  mblfinlem4  26258  itg2addnclem  26270  itg2addnclem3  26272  itg2gt0cn  26274  ftc1cnnclem  26292  dvreasin  26304  areacirclem1  26306  areacirclem2  26307  areacirclem4  26309  areacirclem5  26310  areacirc  26311  cntotbnd  26519  rrnmet  26552  rrndstprj1  26553  rrndstprj2  26554  icodiamlt  26897  irrapxlem2  26900  irrapxlem3  26901  irrapxlem4  26902  irrapxlem5  26903  pellexlem2  26907  pellexlem6  26911  pell1qrgaplem  26950  rmspecfund  26986  rmspecpos  26993  jm2.24nn  27038  jm2.17c  27041  fzmaxdif  27060  acongeq  27062  modabsdifz  27070  jm3.1lem2  27103  fmul01lt1lem2  27705  climinf  27722  stoweidlem1  27740  stoweidlem11  27750  stoweidlem12  27751  stoweidlem13  27752  stoweidlem14  27753  stoweidlem23  27762  stoweidlem24  27763  stoweidlem25  27764  stoweidlem26  27765  stoweidlem34  27773  stoweidlem40  27779  stoweidlem41  27780  stoweidlem42  27781  stoweidlem45  27784  stoweidlem60  27799  stoweidlem62  27801  wallispilem3  27806  wallispilem4  27807  wallispi  27809  wallispi2lem1  27810  stirlinglem5  27817  stirlinglem11  27823  stirlinglem12  27824  2elfz2melfz  28140  modprm0  28262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-po 4506  df-so 4507  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-riota 6552  df-er 6908  df-en 7113  df-dom 7114  df-sdom 7115  df-pnf 9127  df-mnf 9128  df-ltxr 9130  df-sub 9298  df-neg 9299
  Copyright terms: Public domain W3C validator