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

Theorem 1rp 11313
Description: 1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
Assertion
Ref Expression
1rp  |-  1  e.  RR+

Proof of Theorem 1rp
StepHypRef Expression
1 1re 9649 . 2  |-  1  e.  RR
2 0lt1 10143 . 2  |-  0  <  1
31, 2elrpii 11312 1  |-  1  e.  RR+
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872   1c1 9547   RR+crp 11309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-er 7374  df-en 7581  df-dom 7582  df-sdom 7583  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-rp 11310
This theorem is referenced by:  rpreccl  11333  xov1plusxeqvd  11785  modfrac  12116  rpexpcl  12297  caubnd2  13420  reccn2  13659  rlimo1  13679  rlimno1  13716  caurcvgr  13737  caurcvgrOLD  13738  caurcvg  13741  caurcvgOLD  13742  caurcvg2  13743  caucvg  13744  caucvgb  13745  fprodrpcl  14009  rprisefaccl  14075  isprm6  14665  rpmsubg  19030  unirnblps  21432  unirnbl  21433  mopnex  21532  metustfbas  21570  dscopn  21586  nrginvrcnlem  21691  nrginvrcn  21692  tgioo  21812  xrsmopn  21828  zdis  21832  lebnumlem3  21989  lebnumlem3OLD  21992  lebnum  21993  xlebnum  21994  nmhmcn  22132  caun0  22249  cmetcaulem  22256  iscmet3lem3  22258  iscmet3lem1  22259  iscmet3lem2  22260  iscmet3  22261  cmpcmet  22285  cncmet  22288  minveclem3b  22368  minveclem3bOLD  22380  nulmbl2  22488  dveflem  22929  aalioulem2  23287  aalioulem3  23288  aalioulem5  23290  aaliou2b  23295  aaliou3lem3  23298  ulmbdd  23351  iblulm  23360  radcnvlem1  23366  abelthlem2  23385  abelthlem5  23388  abelthlem7  23391  log1  23533  logm1  23536  rplogcl  23551  logge0  23552  divlogrlim  23578  logno1  23579  logcnlem2  23586  logcnlem3  23587  logcnlem4  23588  dvlog2  23596  logtayl  23603  logtayl2  23605  cxpcn3lem  23685  resqrtcn  23687  loglesqrt  23696  ang180lem2  23737  isosctrlem2  23746  angpined  23754  efrlim  23893  sqrtlim  23896  cxp2limlem  23899  logdifbnd  23917  emcllem4  23922  emcllem5  23923  emcllem6  23924  lgamgulmlem5  23956  lgambdd  23960  lgamcvg2  23978  relgamcl  23985  ftalem4  23998  ftalem4OLD  24000  vmalelog  24131  logfacubnd  24147  logfacbnd3  24149  logfacrlim  24150  logexprlim  24151  chpchtlim  24315  vmadivsumb  24319  rpvmasumlem  24323  dchrvmasumlem2  24334  dchrvmasumlema  24336  dchrvmasumiflem1  24337  dchrisum0fno1  24347  dchrisum0re  24349  dirith2  24364  logdivsum  24369  mulog2sumlem2  24371  vmalogdivsum2  24374  vmalogdivsum  24375  2vmadivsumlem  24376  log2sumbnd  24380  selbergb  24385  selberg2lem  24386  selberg2b  24388  chpdifbndlem1  24389  chpdifbndlem2  24390  logdivbnd  24392  selberg3lem1  24393  selberg3lem2  24394  selberg3  24395  selberg4lem1  24396  selberg4  24397  selberg3r  24405  selberg4r  24406  selberg34r  24407  pntrlog2bndlem1  24413  pntrlog2bndlem2  24414  pntrlog2bndlem3  24415  pntrlog2bndlem4  24416  pntrlog2bndlem5  24417  pntrlog2bndlem6a  24418  pntrlog2bndlem6  24419  pntrlog2bnd  24420  pntpbnd1a  24421  pntibndlem3  24428  pntlemd  24430  pntlemn  24436  pntlemq  24437  pntlemr  24438  pntlemj  24439  pntlemk  24442  pntlem3  24445  pntleml  24447  ostth3  24474  smcnlem  26331  blocnilem  26443  0cnop  27630  0cnfn  27631  nmcopexi  27678  nmcfnexi  27702  xrnarchi  28508  xrge0iifcnv  28747  omssubadd  29136  omssubaddOLD  29140  sinccvg  30325  iprodgam  30385  faclimlem1  30386  faclimlem3  30388  faclim  30389  iprodfac  30390  opnrebl2  30982  ptrecube  31904  mblfinlem4  31944  ftc1anc  31989  totbndbnd  32085  rrntotbnd  32132  rencldnfi  35633  irrapxlem1  35636  irrapxlem2  35637  irrapxlem3  35638  pell1qrgaplem  35689  pell14qrgapw  35692  reglogltb  35709  reglogleb  35710  pellfund14  35716  binomcxplemnotnn0  36675  supxrgere  37510  supxrgelem  37514  suplesup  37516  xrlexaddrp  37529  xralrple2  37531  ltdivgt1  37533  limcdm0  37638  constlimc  37644  0ellimcdiv  37670  sinaover2ne0  37683  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  wallispi  37872  stirlinglem5  37880  stirlinglem6  37881  stirlinglem10  37885  fourierdlem30  37939  etransclem48OLD  38087  etransclem48  38088  hoicvrrex  38282  hoidmvlelem3  38323  perfectALTVlem2  38714  logge0b  39963  loggt0b  39964  regt1loggt0  39968
  Copyright terms: Public domain W3C validator