Theorem 1rp 12921

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 11144	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11671	. 2 ⊢ 0 < 1
3	1, 2	elrpii 12920	1 ⊢ 1 ∈ ℝ+

Syntax hints:   ∈ wcel 2114  1c1 11039  ℝ⁺crp 12917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-rp 12918

This theorem is referenced by:  rpreccl  12945  xov1plusxeqvd  13426  modfrac  13816  rpexpcl  14015  caubnd2  15293  reccn2  15532  rlimo1  15552  rlimno1  15589  caurcvgr  15609  caurcvg  15612  caurcvg2  15613  caucvg  15614  caucvgb  15615  fprodrpcl  15891  rprisefaccl  15958  isprm6  16653  rpmsubg  21401  unirnblps  24378  unirnbl  24379  mopnex  24478  metustfbas  24516  nrginvrcnlem  24650  nrginvrcn  24651  tgioo  24755  xrsmopn  24772  zdis  24776  lebnumlem3  24933  lebnum  24934  xlebnum  24935  nmhmcn  25091  caun0  25252  cmetcaulem  25259  iscmet3lem3  25261  iscmet3lem1  25262  iscmet3lem2  25263  iscmet3  25264  cmpcmet  25290  cncmet  25293  minveclem3b  25399  nulmbl2  25508  dveflem  25954  aalioulem2  26312  aalioulem3  26313  aalioulem5  26315  aaliou2b  26320  aaliou3lem3  26323  ulmbdd  26378  iblulm  26387  radcnvlem1  26393  abelthlem5  26416  log1  26565  logm1  26569  rplogcl  26584  logge0  26585  logge0b  26611  loggt0b  26612  divlogrlim  26615  logno1  26616  logcnlem2  26623  logcnlem3  26624  logcnlem4  26625  logtayl  26640  cxpcn3lem  26728  resqrtcn  26730  zrtelqelz  26739  loglesqrt  26742  ang180lem2  26791  isosctrlem2  26800  angpined  26811  efrlim  26950  efrlimOLD  26951  sqrtlim  26954  cxp2limlem  26957  logdifbnd  26975  emcllem4  26980  emcllem5  26981  emcllem6  26982  lgamgulmlem5  27014  lgambdd  27018  lgamcvg2  27036  relgamcl  27043  ftalem4  27057  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  30789  blocnilem  30896  0cnop  32071  0cnfn  32072  nmcopexi  32119  nmcfnexi  32143  xrnarchi  33282  xrge0iifcnv  34115  omssubadd  34482  hgt750lemd  34830  sinccvg  35893  iprodgam  35962  faclimlem1  35963  faclimlem3  35965  faclim  35966  iprodfac  35967  opnrebl2  36541  unblimceq0  36733  ptrecube  37875  mblfinlem4  37915  ftc1anc  37956  totbndbnd  38044  rrntotbnd  38091  aks4d1p1p4  42445  aks4d1p1p6  42447  aks4d1p1p5  42449  aks4d1p8  42461  explt1d  42697  expeq1d  42698  rencldnfi  43182  irrapxlem1  43183  irrapxlem2  43184  irrapxlem3  43185  pell1qrgaplem  43234  pell14qrgapw  43237  reglogltb  43252  reglogleb  43253  pellfund14  43259  binomcxplemnotnn0  44716  supxrgere  45696  supxrgelem  45700  suplesup  45702  xrlexaddrp  45715  xralrple2  45717  ltdivgt1  45719  infleinf  45734  xralrple3  45736  iooiinicc  45906  iooiinioc  45920  limcdm0  45982  constlimc  45988  0ellimcdiv  46011  climrescn  46110  climxrre  46112  sinaover2ne0  46230  fprodsubrecnncnvlem  46269  fprodaddrecnncnvlem  46271  ioodvbdlimc1lem2  46294  ioodvbdlimc2lem  46296  wallispi  46432  stirlinglem5  46440  stirlinglem6  46441  stirlinglem10  46445  fourierdlem30  46499  etransclem48  46644  hoicvrrex  46918  hoidmvlelem3  46959  vonioolem1  47042  smfmullem1  47153  smfmullem2  47154  smfmullem3  47155  perfectALTVlem2  48086  regt1loggt0  48900