Theorem 1rp 12897

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 11115	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11642	. 2 ⊢ 0 < 1
3	1, 2	elrpii 12896	1 ⊢ 1 ∈ ℝ+

Syntax hints:   ∈ wcel 2109  1c1 11010  ℝ⁺crp 12893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  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 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-rp 12894

This theorem is referenced by:  rpreccl  12921  xov1plusxeqvd  13401  modfrac  13788  rpexpcl  13987  caubnd2  15265  reccn2  15504  rlimo1  15524  rlimno1  15561  caurcvgr  15581  caurcvg  15584  caurcvg2  15585  caucvg  15586  caucvgb  15587  fprodrpcl  15863  rprisefaccl  15930  isprm6  16625  rpmsubg  21338  unirnblps  24305  unirnbl  24306  mopnex  24405  metustfbas  24443  nrginvrcnlem  24577  nrginvrcn  24578  tgioo  24682  xrsmopn  24699  zdis  24703  lebnumlem3  24860  lebnum  24861  xlebnum  24862  nmhmcn  25018  caun0  25179  cmetcaulem  25186  iscmet3lem3  25188  iscmet3lem1  25189  iscmet3lem2  25190  iscmet3  25191  cmpcmet  25217  cncmet  25220  minveclem3b  25326  nulmbl2  25435  dveflem  25881  aalioulem2  26239  aalioulem3  26240  aalioulem5  26242  aaliou2b  26247  aaliou3lem3  26250  ulmbdd  26305  iblulm  26314  radcnvlem1  26320  abelthlem5  26343  log1  26492  logm1  26496  rplogcl  26511  logge0  26512  logge0b  26538  loggt0b  26539  divlogrlim  26542  logno1  26543  logcnlem2  26550  logcnlem3  26551  logcnlem4  26552  logtayl  26567  cxpcn3lem  26655  resqrtcn  26657  zrtelqelz  26666  loglesqrt  26669  ang180lem2  26718  isosctrlem2  26727  angpined  26738  efrlim  26877  efrlimOLD  26878  sqrtlim  26881  cxp2limlem  26884  logdifbnd  26902  emcllem4  26907  emcllem5  26908  emcllem6  26909  lgamgulmlem5  26941  lgambdd  26945  lgamcvg2  26963  relgamcl  26970  ftalem4  26984  vmalelog  27114  logfacubnd  27130  logfacbnd3  27132  logfacrlim  27133  logexprlim  27134  chpchtlim  27388  vmadivsumb  27392  rpvmasumlem  27396  dchrvmasumlem2  27407  dchrvmasumlema  27409  dchrvmasumiflem1  27410  dchrisum0fno1  27420  dchrisum0re  27422  dirith2  27437  logdivsum  27442  mulog2sumlem2  27444  vmalogdivsum2  27447  vmalogdivsum  27448  2vmadivsumlem  27449  log2sumbnd  27453  selbergb  27458  selberg2lem  27459  selberg2b  27461  chpdifbndlem1  27462  chpdifbndlem2  27463  logdivbnd  27465  selberg3lem1  27466  selberg3lem2  27467  selberg3  27468  selberg4lem1  27469  selberg4  27470  selberg3r  27478  selberg4r  27479  selberg34r  27480  pntrlog2bndlem1  27486  pntrlog2bndlem2  27487  pntrlog2bndlem3  27488  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntrlog2bndlem6a  27491  pntrlog2bndlem6  27492  pntrlog2bnd  27493  pntpbnd1a  27494  pntibndlem3  27501  pntlemd  27503  pntlemn  27509  pntlemq  27510  pntlemr  27511  pntlemj  27512  pntlemk  27515  pntlem3  27518  pntleml  27520  ostth3  27547  smcnlem  30641  blocnilem  30748  0cnop  31923  0cnfn  31924  nmcopexi  31971  nmcfnexi  31995  xrnarchi  33127  xrge0iifcnv  33906  omssubadd  34274  hgt750lemd  34622  sinccvg  35656  iprodgam  35725  faclimlem1  35726  faclimlem3  35728  faclim  35729  iprodfac  35730  opnrebl2  36305  unblimceq0  36491  ptrecube  37610  mblfinlem4  37650  ftc1anc  37691  totbndbnd  37779  rrntotbnd  37826  aks4d1p1p4  42054  aks4d1p1p6  42056  aks4d1p1p5  42058  aks4d1p8  42070  explt1d  42306  expeq1d  42307  rencldnfi  42804  irrapxlem1  42805  irrapxlem2  42806  irrapxlem3  42807  pell1qrgaplem  42856  pell14qrgapw  42859  reglogltb  42874  reglogleb  42875  pellfund14  42881  binomcxplemnotnn0  44339  supxrgere  45323  supxrgelem  45327  suplesup  45329  xrlexaddrp  45342  xralrple2  45344  ltdivgt1  45346  infleinf  45361  xralrple3  45363  iooiinicc  45533  iooiinioc  45547  limcdm0  45609  constlimc  45615  0ellimcdiv  45640  climrescn  45739  climxrre  45741  sinaover2ne0  45859  fprodsubrecnncnvlem  45898  fprodaddrecnncnvlem  45900  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  wallispi  46061  stirlinglem5  46069  stirlinglem6  46070  stirlinglem10  46074  fourierdlem30  46128  etransclem48  46273  hoicvrrex  46547  hoidmvlelem3  46588  vonioolem1  46671  smfmullem1  46782  smfmullem2  46783  smfmullem3  46784  perfectALTVlem2  47716  regt1loggt0  48531