Theorem 1rp 12938

Description: 1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)

Assertion

Ref	Expression
1rp	⊢ 1 ∈ ℝ+

Proof of Theorem 1rp

Step	Hyp	Ref	Expression
1		1re 11136	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11664	. 2 ⊢ 0 < 1
3	1, 2	elrpii 12937	1 ⊢ 1 ∈ ℝ+

Syntax hints:   ∈ wcel 2119  1c1 11031  ℝ⁺crp 12934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-nul 5229  ax-pow 5295  ax-pr 5363  ax-un 7679  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106  ax-pre-mulgt0 11107

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-opab 5136  df-mpt 5155  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7314  df-ov 7360  df-oprab 7361  df-mpo 7362  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11173  df-mnf 11174  df-xr 11175  df-ltxr 11176  df-le 11177  df-sub 11371  df-neg 11372  df-rp 12935

This theorem is referenced by:  rpreccl  12962  xov1plusxeqvd  13443  modfrac  13835  rpexpcl  14034  caubnd2  15312  reccn2  15551  rlimo1  15571  rlimno1  15608  caurcvgr  15628  caurcvg  15631  caurcvg2  15632  caucvg  15633  caucvgb  15634  fprodrpcl  15913  rprisefaccl  15980  isprm6  16676  rpmsubg  21407  unirnblps  24403  unirnbl  24404  mopnex  24503  metustfbas  24541  nrginvrcnlem  24675  nrginvrcn  24676  tgioo  24780  xrsmopn  24797  zdis  24801  lebnumlem3  24949  lebnum  24950  xlebnum  24951  nmhmcn  25106  caun0  25267  cmetcaulem  25274  iscmet3lem3  25276  iscmet3lem1  25277  iscmet3lem2  25278  iscmet3  25279  cmpcmet  25305  cncmet  25308  minveclem3b  25414  nulmbl2  25522  dveflem  25965  aalioulem2  26318  aalioulem3  26319  aalioulem5  26321  aaliou2b  26326  aaliou3lem3  26329  ulmbdd  26382  iblulm  26391  radcnvlem1  26397  abelthlem5  26419  log1  26568  logm1  26572  rplogcl  26587  logge0  26588  logge0b  26614  loggt0b  26615  divlogrlim  26618  logno1  26619  logcnlem2  26626  logcnlem3  26627  logcnlem4  26628  logtayl  26643  cxpcn3lem  26730  resqrtcn  26732  zrtelqelz  26741  loglesqrt  26744  ang180lem2  26793  isosctrlem2  26802  angpined  26813  efrlim  26952  sqrtlim  26955  cxp2limlem  26958  logdifbnd  26976  emcllem4  26981  emcllem5  26982  emcllem6  26983  lgamgulmlem5  27015  lgambdd  27019  lgamcvg2  27037  relgamcl  27044  ftalem4  27058  vmalelog  27187  logfacubnd  27203  logfacbnd3  27205  logfacrlim  27206  logexprlim  27207  chpchtlim  27461  vmadivsumb  27465  rpvmasumlem  27469  dchrvmasumlem2  27480  dchrvmasumlema  27482  dchrvmasumiflem1  27483  dchrisum0fno1  27493  dchrisum0re  27495  dirith2  27510  logdivsum  27515  mulog2sumlem2  27517  vmalogdivsum2  27520  vmalogdivsum  27521  2vmadivsumlem  27522  log2sumbnd  27526  selbergb  27531  selberg2lem  27532  selberg2b  27534  chpdifbndlem1  27535  chpdifbndlem2  27536  logdivbnd  27538  selberg3lem1  27539  selberg3lem2  27540  selberg3  27541  selberg4lem1  27542  selberg4  27543  selberg3r  27551  selberg4r  27552  selberg34r  27553  pntrlog2bndlem1  27559  pntrlog2bndlem2  27560  pntrlog2bndlem3  27561  pntrlog2bndlem4  27562  pntrlog2bndlem5  27563  pntrlog2bndlem6a  27564  pntrlog2bndlem6  27565  pntrlog2bnd  27566  pntpbnd1a  27567  pntibndlem3  27574  pntlemd  27576  pntlemn  27582  pntlemq  27583  pntlemr  27584  pntlemj  27585  pntlemk  27588  pntlem3  27591  pntleml  27593  ostth3  27620  smcnlem  30787  blocnilem  30894  0cnop  32069  0cnfn  32070  nmcopexi  32117  nmcfnexi  32141  xrnarchi  33266  xrge0iifcnv  34126  omssubadd  34493  hgt750lemd  34841  sinccvg  35910  iprodgam  35979  faclimlem1  35980  faclimlem3  35982  faclim  35983  iprodfac  35984  opnrebl2  36558  unblimceq0  36822  qdiff  37696  ptrecube  37996  mblfinlem4  38036  ftc1anc  38077  totbndbnd  38165  rrntotbnd  38212  aks4d1p1p4  42565  aks4d1p1p6  42567  aks4d1p1p5  42569  aks4d1p8  42581  explt1d  42809  expeq1d  42810  rencldnfi  43275  irrapxlem1  43276  irrapxlem2  43277  irrapxlem3  43278  pell1qrgaplem  43327  pell14qrgapw  43330  reglogltb  43345  reglogleb  43346  pellfund14  43352  binomcxplemnotnn0  44809  supxrgere  45786  supxrgelem  45790  suplesup  45792  xrlexaddrp  45805  xralrple2  45807  ltdivgt1  45809  infleinf  45824  xralrple3  45826  iooiinicc  45995  iooiinioc  46009  limcdm0  46071  constlimc  46077  0ellimcdiv  46100  climrescn  46199  climxrre  46201  sinaover2ne0  46319  fprodsubrecnncnvlem  46358  fprodaddrecnncnvlem  46360  ioodvbdlimc1lem2  46383  ioodvbdlimc2lem  46385  wallispi  46521  stirlinglem5  46529  stirlinglem6  46530  stirlinglem10  46534  fourierdlem30  46588  etransclem48  46733  hoicvrrex  47007  hoidmvlelem3  47048  vonioolem1  47131  smfmullem1  47242  smfmullem2  47243  smfmullem3  47244  perfectALTVlem2  48221  regt1loggt0  49035