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

Theorem 1rp 11096
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 9486 . 2  |-  1  e.  RR
2 0lt1 9963 . 2  |-  0  <  1
31, 2elrpii 11095 1  |-  1  e.  RR+
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758   1c1 9384   RR+crp 11092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459  ax-pre-mulgt0 9460
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-po 4739  df-so 4740  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-riota 6151  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-er 7201  df-en 7411  df-dom 7412  df-sdom 7413  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525  df-sub 9698  df-neg 9699  df-rp 11093
This theorem is referenced by:  rpreccl  11115  xov1plusxeqvd  11532  modfrac  11822  rpexpcl  11985  caubnd2  12947  reccn2  13176  rlimo1  13196  rlimno1  13233  caurcvgr  13253  caurcvg  13256  caurcvg2  13257  caucvg  13258  caucvgb  13259  isprm6  13897  rpmsubg  17985  unirnblps  20110  unirnbl  20111  mopnex  20210  metustfbasOLD  20256  metustfbas  20257  dscopn  20282  nrginvrcnlem  20387  nrginvrcn  20388  tgioo  20489  xrsmopn  20505  zdis  20509  lebnumlem3  20651  lebnum  20652  xlebnum  20653  nmhmcn  20791  caun0  20908  cmetcaulem  20915  iscmet3lem3  20917  iscmet3lem1  20918  iscmet3lem2  20919  iscmet3  20920  cmpcmet  20944  cncmet  20949  minveclem3b  21031  nulmbl2  21134  dveflem  21567  aalioulem2  21915  aalioulem3  21916  aalioulem5  21918  aaliou2b  21923  aaliou3lem3  21926  ulmbdd  21979  iblulm  21988  radcnvlem1  21994  abelthlem2  22013  abelthlem5  22016  abelthlem7  22019  log1  22150  logm1  22153  rplogcl  22169  logge0  22170  divlogrlim  22196  logno1  22197  logcnlem2  22204  logcnlem3  22205  logcnlem4  22206  dvlog2  22214  logtayl  22221  logtayl2  22223  cxpcn3lem  22301  resqrcn  22303  loglesqr  22312  ang180lem2  22322  isosctrlem2  22333  angpined  22341  efrlim  22479  sqrlim  22482  cxp2limlem  22485  logdifbnd  22503  emcllem4  22508  emcllem5  22509  emcllem6  22510  ftalem4  22529  vmalelog  22660  logfacubnd  22676  logfacbnd3  22678  logfacrlim  22679  logexprlim  22680  chpchtlim  22844  vmadivsumb  22848  rpvmasumlem  22852  dchrvmasumlem2  22863  dchrvmasumlema  22865  dchrvmasumiflem1  22866  dchrisum0fno1  22876  dchrisum0re  22878  dirith2  22893  logdivsum  22898  mulog2sumlem2  22900  vmalogdivsum2  22903  vmalogdivsum  22904  2vmadivsumlem  22905  log2sumbnd  22909  selbergb  22914  selberg2lem  22915  selberg2b  22917  chpdifbndlem1  22918  chpdifbndlem2  22919  logdivbnd  22921  selberg3lem1  22922  selberg3lem2  22923  selberg3  22924  selberg4lem1  22925  selberg4  22926  selberg3r  22934  selberg4r  22935  selberg34r  22936  pntrlog2bndlem1  22942  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntrlog2bndlem6a  22947  pntrlog2bndlem6  22948  pntrlog2bnd  22949  pntpbnd1a  22950  pntibndlem3  22957  pntlemd  22959  pntlemn  22965  pntlemq  22966  pntlemr  22967  pntlemj  22968  pntlemk  22971  pntlem3  22974  pntleml  22976  ostth3  23003  smcnlem  24227  blocnilem  24339  0cnop  25518  0cnfn  25519  nmcopexi  25566  nmcfnexi  25590  xrnarchi  26335  xrge0iifcnv  26497  lgamgulmlem5  27153  lgambdd  27157  lgamcvg2  27175  relgamcl  27182  sinccvg  27452  fprodrpcl  27603  iprodgam  27640  rprisefaccl  27660  faclimlem1  27683  faclimlem3  27685  faclim  27686  iprodfac  27687  mblfinlem4  28569  ftc1anc  28613  opnrebl2  28654  totbndbnd  28826  rrntotbnd  28873  rencldnfi  29298  irrapxlem1  29301  irrapxlem2  29302  irrapxlem3  29303  pell1qrgaplem  29352  pell14qrgapw  29355  reglogltb  29370  reglogleb  29371  pellfund14  29377  wallispi  30003  stirlinglem5  30011  stirlinglem6  30012  stirlinglem10  30016
  Copyright terms: Public domain W3C validator