Theorem 1rp 12663

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 10906	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11427	. 2 ⊢ 0 < 1
3	1, 2	elrpii 12662	1 ⊢ 1 ∈ ℝ+

Syntax hints:   ∈ wcel 2108  1c1 10803  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-rp 12660

This theorem is referenced by:  rpreccl  12685  xov1plusxeqvd  13159  modfrac  13532  rpexpcl  13729  caubnd2  14997  reccn2  15234  rlimo1  15254  rlimno1  15293  caurcvgr  15313  caurcvg  15316  caurcvg2  15317  caucvg  15318  caucvgb  15319  fprodrpcl  15594  rprisefaccl  15661  isprm6  16347  rpmsubg  20574  unirnblps  23480  unirnbl  23481  mopnex  23581  metustfbas  23619  nrginvrcnlem  23761  nrginvrcn  23762  tgioo  23865  xrsmopn  23881  zdis  23885  lebnumlem3  24032  lebnum  24033  xlebnum  24034  nmhmcn  24189  caun0  24350  cmetcaulem  24357  iscmet3lem3  24359  iscmet3lem1  24360  iscmet3lem2  24361  iscmet3  24362  cmpcmet  24388  cncmet  24391  minveclem3b  24497  nulmbl2  24605  dveflem  25048  aalioulem2  25398  aalioulem3  25399  aalioulem5  25401  aaliou2b  25406  aaliou3lem3  25409  ulmbdd  25462  iblulm  25471  radcnvlem1  25477  abelthlem5  25499  log1  25646  logm1  25649  rplogcl  25664  logge0  25665  logge0b  25691  loggt0b  25692  divlogrlim  25695  logno1  25696  logcnlem2  25703  logcnlem3  25704  logcnlem4  25705  logtayl  25720  cxpcn3lem  25805  resqrtcn  25807  loglesqrt  25816  ang180lem2  25865  isosctrlem2  25874  angpined  25885  efrlim  26024  sqrtlim  26027  cxp2limlem  26030  logdifbnd  26048  emcllem4  26053  emcllem5  26054  emcllem6  26055  lgamgulmlem5  26087  lgambdd  26091  lgamcvg2  26109  relgamcl  26116  ftalem4  26130  vmalelog  26258  logfacubnd  26274  logfacbnd3  26276  logfacrlim  26277  logexprlim  26278  chpchtlim  26532  vmadivsumb  26536  rpvmasumlem  26540  dchrvmasumlem2  26551  dchrvmasumlema  26553  dchrvmasumiflem1  26554  dchrisum0fno1  26564  dchrisum0re  26566  dirith2  26581  logdivsum  26586  mulog2sumlem2  26588  vmalogdivsum2  26591  vmalogdivsum  26592  2vmadivsumlem  26593  log2sumbnd  26597  selbergb  26602  selberg2lem  26603  selberg2b  26605  chpdifbndlem1  26606  chpdifbndlem2  26607  logdivbnd  26609  selberg3lem1  26610  selberg3lem2  26611  selberg3  26612  selberg4lem1  26613  selberg4  26614  selberg3r  26622  selberg4r  26623  selberg34r  26624  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntrlog2bndlem6a  26635  pntrlog2bndlem6  26636  pntrlog2bnd  26637  pntpbnd1a  26638  pntibndlem3  26645  pntlemd  26647  pntlemn  26653  pntlemq  26654  pntlemr  26655  pntlemj  26656  pntlemk  26659  pntlem3  26662  pntleml  26664  ostth3  26691  smcnlem  28960  blocnilem  29067  0cnop  30242  0cnfn  30243  nmcopexi  30290  nmcfnexi  30314  xrnarchi  31340  xrge0iifcnv  31785  omssubadd  32167  hgt750lemd  32528  sinccvg  33531  iprodgam  33614  faclimlem1  33615  faclimlem3  33617  faclim  33618  iprodfac  33619  opnrebl2  34437  unblimceq0  34614  ptrecube  35704  mblfinlem4  35744  ftc1anc  35785  totbndbnd  35874  rrntotbnd  35921  aks4d1p1p4  40007  aks4d1p1p6  40009  aks4d1p1p5  40011  aks4d1p8  40023  metakunt28  40080  zrtelqelz  40266  rencldnfi  40559  irrapxlem1  40560  irrapxlem2  40561  irrapxlem3  40562  pell1qrgaplem  40611  pell14qrgapw  40614  reglogltb  40629  reglogleb  40630  pellfund14  40636  binomcxplemnotnn0  41863  supxrgere  42762  supxrgelem  42766  suplesup  42768  xrlexaddrp  42781  xralrple2  42783  ltdivgt1  42785  infleinf  42801  xralrple3  42803  iooiinicc  42970  iooiinioc  42984  limcdm0  43049  constlimc  43055  0ellimcdiv  43080  climrescn  43179  climxrre  43181  sinaover2ne0  43299  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  wallispi  43501  stirlinglem5  43509  stirlinglem6  43510  stirlinglem10  43514  fourierdlem30  43568  etransclem48  43713  hoicvrrex  43984  hoidmvlelem3  44025  vonioolem1  44108  smfmullem1  44212  smfmullem2  44213  smfmullem3  44214  perfectALTVlem2  45062  regt1loggt0  45770