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

Theorem 1rp 12388
Description: 1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
Assertion
Ref Expression
1rp 1 ∈ ℝ+

Proof of Theorem 1rp
StepHypRef Expression
1 1re 10635 . 2 1 ∈ ℝ
2 0lt1 11156 . 2 0 < 1
31, 2elrpii 12387 1 1 ∈ ℝ+
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  1c1 10532  +crp 12384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-po 5473  df-so 5474  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-er 8284  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-rp 12385
This theorem is referenced by:  rpreccl  12410  xov1plusxeqvd  12879  modfrac  13247  rpexpcl  13443  caubnd2  14712  reccn2  14948  rlimo1  14968  rlimno1  15005  caurcvgr  15025  caurcvg  15028  caurcvg2  15029  caucvg  15030  caucvgb  15031  fprodrpcl  15305  rprisefaccl  15372  isprm6  16053  rpmsubg  20544  unirnblps  22963  unirnbl  22964  mopnex  23063  metustfbas  23101  nrginvrcnlem  23234  nrginvrcn  23235  tgioo  23338  xrsmopn  23354  zdis  23358  lebnumlem3  23501  lebnum  23502  xlebnum  23503  nmhmcn  23658  caun0  23818  cmetcaulem  23825  iscmet3lem3  23827  iscmet3lem1  23828  iscmet3lem2  23829  iscmet3  23830  cmpcmet  23856  cncmet  23859  minveclem3b  23965  nulmbl2  24071  dveflem  24510  aalioulem2  24856  aalioulem3  24857  aalioulem5  24859  aaliou2b  24864  aaliou3lem3  24867  ulmbdd  24920  iblulm  24929  radcnvlem1  24935  abelthlem5  24957  log1  25101  logm1  25104  rplogcl  25119  logge0  25120  logge0b  25146  loggt0b  25147  divlogrlim  25150  logno1  25151  logcnlem2  25158  logcnlem3  25159  logcnlem4  25160  logtayl  25175  cxpcn3lem  25260  resqrtcn  25262  loglesqrt  25271  ang180lem2  25320  isosctrlem2  25329  angpined  25340  efrlim  25480  sqrtlim  25483  cxp2limlem  25486  logdifbnd  25504  emcllem4  25509  emcllem5  25510  emcllem6  25511  lgamgulmlem5  25543  lgambdd  25547  lgamcvg2  25565  relgamcl  25572  ftalem4  25586  vmalelog  25714  logfacubnd  25730  logfacbnd3  25732  logfacrlim  25733  logexprlim  25734  chpchtlim  25988  vmadivsumb  25992  rpvmasumlem  25996  dchrvmasumlem2  26007  dchrvmasumlema  26009  dchrvmasumiflem1  26010  dchrisum0fno1  26020  dchrisum0re  26022  dirith2  26037  logdivsum  26042  mulog2sumlem2  26044  vmalogdivsum2  26047  vmalogdivsum  26048  2vmadivsumlem  26049  log2sumbnd  26053  selbergb  26058  selberg2lem  26059  selberg2b  26061  chpdifbndlem1  26062  chpdifbndlem2  26063  logdivbnd  26065  selberg3lem1  26066  selberg3lem2  26067  selberg3  26068  selberg4lem1  26069  selberg4  26070  selberg3r  26078  selberg4r  26079  selberg34r  26080  pntrlog2bndlem1  26086  pntrlog2bndlem2  26087  pntrlog2bndlem3  26088  pntrlog2bndlem4  26089  pntrlog2bndlem5  26090  pntrlog2bndlem6a  26091  pntrlog2bndlem6  26092  pntrlog2bnd  26093  pntpbnd1a  26094  pntibndlem3  26101  pntlemd  26103  pntlemn  26109  pntlemq  26110  pntlemr  26111  pntlemj  26112  pntlemk  26115  pntlem3  26118  pntleml  26120  ostth3  26147  smcnlem  28407  blocnilem  28514  0cnop  29689  0cnfn  29690  nmcopexi  29737  nmcfnexi  29761  xrnarchi  30746  xrge0iifcnv  31081  omssubadd  31463  hgt750lemd  31824  sinccvg  32819  iprodgam  32877  faclimlem1  32878  faclimlem3  32880  faclim  32881  iprodfac  32882  opnrebl2  33572  unblimceq0  33749  ptrecube  34778  mblfinlem4  34818  ftc1anc  34861  totbndbnd  34954  rrntotbnd  35001  zrtelqelz  39076  rencldnfi  39302  irrapxlem1  39303  irrapxlem2  39304  irrapxlem3  39305  pell1qrgaplem  39354  pell14qrgapw  39357  reglogltb  39372  reglogleb  39373  pellfund14  39379  binomcxplemnotnn0  40572  supxrgere  41485  supxrgelem  41489  suplesup  41491  xrlexaddrp  41504  xralrple2  41506  ltdivgt1  41508  infleinf  41524  xralrple3  41526  iooiinicc  41702  iooiinioc  41716  limcdm0  41783  constlimc  41789  0ellimcdiv  41814  climrescn  41913  climxrre  41915  sinaover2ne0  42033  fprodsubrecnncnvlem  42075  fprodaddrecnncnvlem  42077  ioodvbdlimc1lem2  42101  ioodvbdlimc2lem  42103  wallispi  42240  stirlinglem5  42248  stirlinglem6  42249  stirlinglem10  42253  fourierdlem30  42307  etransclem48  42452  hoicvrrex  42723  hoidmvlelem3  42764  vonioolem1  42847  smfmullem1  42951  smfmullem2  42952  smfmullem3  42953  perfectALTVlem2  43738  regt1loggt0  44498
  Copyright terms: Public domain W3C validator