Theorem 1rp 13038

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 11225	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11753	. 2 ⊢ 0 < 1
3	1, 2	elrpii 13037	1 ⊢ 1 ∈ ℝ+

This proof depends on syntax axioms:   ∈ wcel 2146  1c1 11118  ℝ⁺crp 13034

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193  ax-pre-mulgt0 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-sub 11460  df-neg 11461  df-rp 13035

This theorem is used by:  rpreccl  13062  xov1plusxeqvd  13543  modfrac  13937  rpexpcl  14136  caubnd2  15435  reccn2  15674  rlimo1  15694  rlimno1  15731  caurcvgr  15751  caurcvg  15754  caurcvg2  15755  caucvg  15756  caucvgb  15757  fprodrpcl  16035  rprisefaccl  16102  isprm6  16797  rpmsubg  21633  unirnblps  24629  unirnbl  24630  mopnex  24729  metustfbas  24767  nrginvrcnlem  24901  nrginvrcn  24902  tgioo  25006  xrsmopn  25023  zdis  25027  lebnumlem3  25175  lebnum  25176  xlebnum  25177  nmhmcn  25332  caun0  25493  cmetcaulem  25500  iscmet3lem3  25502  iscmet3lem1  25503  iscmet3lem2  25504  iscmet3  25505  cmpcmet  25531  cncmet  25534  minveclem3b  25640  nulmbl2  25748  dveflem  26191  aalioulem2  26549  aalioulem3  26550  aalioulem5  26552  aaliou2b  26557  aaliou3lem3  26560  ulmbdd  26614  iblulm  26623  radcnvlem1  26629  abelthlem5  26651  log1  26803  logm1  26807  rplogcl  26822  logge0  26823  logge0b  26849  loggt0b  26850  divlogrlim  26853  logno1  26854  logcnlem2  26861  logcnlem3  26862  logcnlem4  26863  logtayl  26878  cxpcn3lem  26965  resqrtcn  26967  zrtelqelz  26976  loglesqrt  26979  ang180lem2  27028  isosctrlem2  27037  angpined  27048  efrlim  27187  sqrtlim  27190  cxp2limlem  27193  logdifbnd  27211  emcllem4  27216  emcllem5  27217  emcllem6  27218  lgamgulmlem5  27250  lgambdd  27254  lgamcvg2  27272  relgamcl  27279  ftalem4  27293  vmalelog  27422  logfacubnd  27438  logfacbnd3  27440  logfacrlim  27441  logexprlim  27442  chpchtlim  27696  vmadivsumb  27700  rpvmasumlem  27704  dchrvmasumlem2  27715  dchrvmasumlema  27717  dchrvmasumiflem1  27718  dchrisum0fno1  27728  dchrisum0re  27730  dirith2  27745  logdivsum  27750  mulog2sumlem2  27752  vmalogdivsum2  27755  vmalogdivsum  27756  2vmadivsumlem  27757  log2sumbnd  27761  selbergb  27766  selberg2lem  27767  selberg2b  27769  chpdifbndlem1  27770  chpdifbndlem2  27771  logdivbnd  27773  selberg3lem1  27774  selberg3lem2  27775  selberg3  27776  selberg4lem1  27777  selberg4  27778  selberg3r  27786  selberg4r  27787  selberg34r  27788  pntrlog2bndlem1  27794  pntrlog2bndlem2  27795  pntrlog2bndlem3  27796  pntrlog2bndlem4  27797  pntrlog2bndlem5  27798  pntrlog2bndlem6a  27799  pntrlog2bndlem6  27800  pntrlog2bnd  27801  pntpbnd1a  27802  pntibndlem3  27809  pntlemd  27811  pntlemn  27817  pntlemq  27818  pntlemr  27819  pntlemj  27820  pntlemk  27823  pntlem3  27826  pntleml  27828  ostth3  27855  smcnlem  31122  blocnilem  31229  0cnop  32404  0cnfn  32405  nmcopexi  32452  nmcfnexi  32476  xrnarchi  33570  xrge0iifcnv  34389  omssubadd  34757  hgt750lemd  35102  sinccvg  36204  iprodgam  36273  faclimlem1  36274  faclimlem3  36276  faclim  36277  iprodfac  36278  opnrebl2  36891  unblimceq0  37155  qdiff  38030  ptrecube  38330  mblfinlem4  38370  ftc1anc  38411  totbndbnd  38500  rrntotbnd  38547  aks4d1p1p4  42898  aks4d1p1p6  42900  aks4d1p1p5  42902  aks4d1p8  42914  explt1d  43144  expeq1d  43145  rencldnfi  43608  irrapxlem1  43609  irrapxlem2  43610  irrapxlem3  43611  pell1qrgaplem  43660  pell14qrgapw  43663  reglogltb  43678  reglogleb  43679  pellfund14  43685  binomcxplemnotnn0  45126  supxrgere  46109  supxrgelem  46113  suplesup  46115  xrlexaddrp  46128  xralrple2  46130  ltdivgt1  46132  infleinf  46147  xralrple3  46149  iooiinicc  46318  iooiinioc  46332  limcdm0  46394  constlimc  46400  0ellimcdiv  46423  climrescn  46522  climxrre  46524  sinaover2ne0  46642  fprodsubrecnncnvlem  46681  fprodaddrecnncnvlem  46683  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  wallispi  46844  stirlinglem5  46852  stirlinglem6  46853  stirlinglem10  46857  fourierdlem30  46911  etransclem48  47056  hoicvrrex  47330  hoidmvlelem3  47371  vonioolem1  47454  smfmullem1  47565  smfmullem2  47566  smfmullem3  47567  perfectALTVlem2  48547  regt1loggt0  49375