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

Theorem 1rp 11296
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 9629 . 2  |-  1  e.  RR
2 0lt1 10125 . 2  |-  0  <  1
31, 2elrpii 11295 1  |-  1  e.  RR+
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1891   1c1 9527   RR+crp 11292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571  ax-resscn 9583  ax-1cn 9584  ax-icn 9585  ax-addcl 9586  ax-addrcl 9587  ax-mulcl 9588  ax-mulrcl 9589  ax-mulcom 9590  ax-addass 9591  ax-mulass 9592  ax-distr 9593  ax-i2m1 9594  ax-1ne0 9595  ax-1rid 9596  ax-rnegex 9597  ax-rrecex 9598  ax-cnre 9599  ax-pre-lttri 9600  ax-pre-lttrn 9601  ax-pre-ltadd 9602  ax-pre-mulgt0 9603
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-br 4375  df-opab 4434  df-mpt 4435  df-id 4727  df-po 4733  df-so 4734  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-riota 6238  df-ov 6279  df-oprab 6280  df-mpt2 6281  df-er 7350  df-en 7557  df-dom 7558  df-sdom 7559  df-pnf 9664  df-mnf 9665  df-xr 9666  df-ltxr 9667  df-le 9668  df-sub 9849  df-neg 9850  df-rp 11293
This theorem is referenced by:  rpreccl  11316  xov1plusxeqvd  11769  modfrac  12104  rpexpcl  12285  caubnd2  13431  reccn2  13671  rlimo1  13691  rlimno1  13728  caurcvgr  13749  caurcvgrOLD  13750  caurcvg  13753  caurcvgOLD  13754  caurcvg2  13755  caucvg  13756  caucvgb  13757  fprodrpcl  14021  rprisefaccl  14087  isprm6  14677  rpmsubg  19042  unirnblps  21445  unirnbl  21446  mopnex  21545  metustfbas  21583  dscopn  21599  nrginvrcnlem  21704  nrginvrcn  21705  tgioo  21825  xrsmopn  21841  zdis  21845  lebnumlem3  22002  lebnumlem3OLD  22005  lebnum  22006  xlebnum  22007  nmhmcn  22145  caun0  22262  cmetcaulem  22269  iscmet3lem3  22271  iscmet3lem1  22272  iscmet3lem2  22273  iscmet3  22274  cmpcmet  22298  cncmet  22301  minveclem3b  22381  minveclem3bOLD  22393  nulmbl2  22501  dveflem  22943  aalioulem2  23301  aalioulem3  23302  aalioulem5  23304  aaliou2b  23309  aaliou3lem3  23312  ulmbdd  23365  iblulm  23374  radcnvlem1  23380  abelthlem2  23399  abelthlem5  23402  abelthlem7  23405  log1  23547  logm1  23550  rplogcl  23565  logge0  23566  divlogrlim  23592  logno1  23593  logcnlem2  23600  logcnlem3  23601  logcnlem4  23602  dvlog2  23610  logtayl  23617  logtayl2  23619  cxpcn3lem  23699  resqrtcn  23701  loglesqrt  23710  ang180lem2  23751  isosctrlem2  23760  angpined  23768  efrlim  23907  sqrtlim  23910  cxp2limlem  23913  logdifbnd  23931  emcllem4  23936  emcllem5  23937  emcllem6  23938  lgamgulmlem5  23970  lgambdd  23974  lgamcvg2  23992  relgamcl  23999  ftalem4  24012  ftalem4OLD  24014  vmalelog  24145  logfacubnd  24161  logfacbnd3  24163  logfacrlim  24164  logexprlim  24165  chpchtlim  24329  vmadivsumb  24333  rpvmasumlem  24337  dchrvmasumlem2  24348  dchrvmasumlema  24350  dchrvmasumiflem1  24351  dchrisum0fno1  24361  dchrisum0re  24363  dirith2  24378  logdivsum  24383  mulog2sumlem2  24385  vmalogdivsum2  24388  vmalogdivsum  24389  2vmadivsumlem  24390  log2sumbnd  24394  selbergb  24399  selberg2lem  24400  selberg2b  24402  chpdifbndlem1  24403  chpdifbndlem2  24404  logdivbnd  24406  selberg3lem1  24407  selberg3lem2  24408  selberg3  24409  selberg4lem1  24410  selberg4  24411  selberg3r  24419  selberg4r  24420  selberg34r  24421  pntrlog2bndlem1  24427  pntrlog2bndlem2  24428  pntrlog2bndlem3  24429  pntrlog2bndlem4  24430  pntrlog2bndlem5  24431  pntrlog2bndlem6a  24432  pntrlog2bndlem6  24433  pntrlog2bnd  24434  pntpbnd1a  24435  pntibndlem3  24442  pntlemd  24444  pntlemn  24450  pntlemq  24451  pntlemr  24452  pntlemj  24453  pntlemk  24456  pntlem3  24459  pntleml  24461  ostth3  24488  smcnlem  26345  blocnilem  26457  0cnop  27644  0cnfn  27645  nmcopexi  27692  nmcfnexi  27716  xrnarchi  28508  xrge0iifcnv  28746  omssubadd  29134  omssubaddOLD  29138  sinccvg  30323  iprodgam  30384  faclimlem1  30385  faclimlem3  30387  faclim  30388  iprodfac  30389  opnrebl2  30983  ptrecube  31942  mblfinlem4  31982  ftc1anc  32027  totbndbnd  32123  rrntotbnd  32170  rencldnfi  35666  irrapxlem1  35668  irrapxlem2  35669  irrapxlem3  35670  pell1qrgaplem  35721  pell14qrgapw  35724  reglogltb  35741  reglogleb  35742  pellfund14  35748  binomcxplemnotnn0  36706  supxrgere  37587  supxrgelem  37591  suplesup  37593  xrlexaddrp  37606  xralrple2  37608  ltdivgt1  37610  infleinf  37627  limcdm0  37740  constlimc  37746  0ellimcdiv  37772  sinaover2ne0  37785  ioodvbdlimc1lem2  37846  ioodvbdlimc1lem2OLD  37848  ioodvbdlimc2lem  37850  ioodvbdlimc2lemOLD  37851  wallispi  37989  stirlinglem5  37997  stirlinglem6  37998  stirlinglem10  38002  fourierdlem30  38056  etransclem48OLD  38204  etransclem48  38205  hoicvrrex  38441  hoidmvlelem3  38482  perfectALTVlem2  38935  logge0b  40667  loggt0b  40668  regt1loggt0  40672
  Copyright terms: Public domain W3C validator