Theorem 1rp 13015

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 11203	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11731	. 2 ⊢ 0 < 1
3	1, 2	elrpii 13014	1 ⊢ 1 ∈ ℝ+

Syntax hints:   ∈ wcel 2143  1c1 11096  ℝ⁺crp 13011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-rp 13012

This theorem is referenced by:  rpreccl  13039  xov1plusxeqvd  13520  modfrac  13913  rpexpcl  14112  caubnd2  15405  reccn2  15644  rlimo1  15664  rlimno1  15701  caurcvgr  15721  caurcvg  15724  caurcvg2  15725  caucvg  15726  caucvgb  15727  fprodrpcl  16006  rprisefaccl  16073  isprm6  16768  rpmsubg  21581  unirnblps  24576  unirnbl  24577  mopnex  24676  metustfbas  24714  nrginvrcnlem  24848  nrginvrcn  24849  tgioo  24953  xrsmopn  24970  zdis  24974  lebnumlem3  25122  lebnum  25123  xlebnum  25124  nmhmcn  25279  caun0  25440  cmetcaulem  25447  iscmet3lem3  25449  iscmet3lem1  25450  iscmet3lem2  25451  iscmet3  25452  cmpcmet  25478  cncmet  25481  minveclem3b  25587  nulmbl2  25695  dveflem  26138  aalioulem2  26496  aalioulem3  26497  aalioulem5  26499  aaliou2b  26504  aaliou3lem3  26507  ulmbdd  26561  iblulm  26570  radcnvlem1  26576  abelthlem5  26598  log1  26750  logm1  26754  rplogcl  26769  logge0  26770  logge0b  26796  loggt0b  26797  divlogrlim  26800  logno1  26801  logcnlem2  26808  logcnlem3  26809  logcnlem4  26810  logtayl  26825  cxpcn3lem  26912  resqrtcn  26914  zrtelqelz  26923  loglesqrt  26926  ang180lem2  26975  isosctrlem2  26984  angpined  26995  efrlim  27134  sqrtlim  27137  cxp2limlem  27140  logdifbnd  27158  emcllem4  27163  emcllem5  27164  emcllem6  27165  lgamgulmlem5  27197  lgambdd  27201  lgamcvg2  27219  relgamcl  27226  ftalem4  27240  vmalelog  27369  logfacubnd  27385  logfacbnd3  27387  logfacrlim  27388  logexprlim  27389  chpchtlim  27643  vmadivsumb  27647  rpvmasumlem  27651  dchrvmasumlem2  27662  dchrvmasumlema  27664  dchrvmasumiflem1  27665  dchrisum0fno1  27675  dchrisum0re  27677  dirith2  27692  logdivsum  27697  mulog2sumlem2  27699  vmalogdivsum2  27702  vmalogdivsum  27703  2vmadivsumlem  27704  log2sumbnd  27708  selbergb  27713  selberg2lem  27714  selberg2b  27716  chpdifbndlem1  27717  chpdifbndlem2  27718  logdivbnd  27720  selberg3lem1  27721  selberg3lem2  27722  selberg3  27723  selberg4lem1  27724  selberg4  27725  selberg3r  27733  selberg4r  27734  selberg34r  27735  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bndlem6a  27746  pntrlog2bndlem6  27747  pntrlog2bnd  27748  pntpbnd1a  27749  pntibndlem3  27756  pntlemd  27758  pntlemn  27764  pntlemq  27765  pntlemr  27766  pntlemj  27767  pntlemk  27770  pntlem3  27773  pntleml  27775  ostth3  27802  smcnlem  31049  blocnilem  31156  0cnop  32331  0cnfn  32332  nmcopexi  32379  nmcfnexi  32403  xrnarchi  33504  xrge0iifcnv  34323  omssubadd  34690  hgt750lemd  35035  sinccvg  36165  iprodgam  36234  faclimlem1  36235  faclimlem3  36237  faclim  36238  iprodfac  36239  opnrebl2  36852  unblimceq0  37116  qdiff  37991  ptrecube  38291  mblfinlem4  38331  ftc1anc  38372  totbndbnd  38460  rrntotbnd  38507  aks4d1p1p4  42858  aks4d1p1p6  42860  aks4d1p1p5  42862  aks4d1p8  42874  explt1d  43104  expeq1d  43105  rencldnfi  43568  irrapxlem1  43569  irrapxlem2  43570  irrapxlem3  43571  pell1qrgaplem  43620  pell14qrgapw  43623  reglogltb  43638  reglogleb  43639  pellfund14  43645  binomcxplemnotnn0  45086  supxrgere  46069  supxrgelem  46073  suplesup  46075  xrlexaddrp  46088  xralrple2  46090  ltdivgt1  46092  infleinf  46107  xralrple3  46109  iooiinicc  46278  iooiinioc  46292  limcdm0  46354  constlimc  46360  0ellimcdiv  46383  climrescn  46482  climxrre  46484  sinaover2ne0  46602  fprodsubrecnncnvlem  46641  fprodaddrecnncnvlem  46643  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  wallispi  46804  stirlinglem5  46812  stirlinglem6  46813  stirlinglem10  46817  fourierdlem30  46871  etransclem48  47016  hoicvrrex  47290  hoidmvlelem3  47331  vonioolem1  47414  smfmullem1  47525  smfmullem2  47526  smfmullem3  47527  perfectALTVlem2  48507  regt1loggt0  49336