Theorem 1rp 12955

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 11174	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11700	. 2 ⊢ 0 < 1
3	1, 2	elrpii 12954	1 ⊢ 1 ∈ ℝ+

Syntax hints:   ∈ wcel 2109  1c1 11069  ℝ⁺crp 12951

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-rp 12952

This theorem is referenced by:  rpreccl  12979  xov1plusxeqvd  13459  modfrac  13846  rpexpcl  14045  caubnd2  15324  reccn2  15563  rlimo1  15583  rlimno1  15620  caurcvgr  15640  caurcvg  15643  caurcvg2  15644  caucvg  15645  caucvgb  15646  fprodrpcl  15922  rprisefaccl  15989  isprm6  16684  rpmsubg  21348  unirnblps  24307  unirnbl  24308  mopnex  24407  metustfbas  24445  nrginvrcnlem  24579  nrginvrcn  24580  tgioo  24684  xrsmopn  24701  zdis  24705  lebnumlem3  24862  lebnum  24863  xlebnum  24864  nmhmcn  25020  caun0  25181  cmetcaulem  25188  iscmet3lem3  25190  iscmet3lem1  25191  iscmet3lem2  25192  iscmet3  25193  cmpcmet  25219  cncmet  25222  minveclem3b  25328  nulmbl2  25437  dveflem  25883  aalioulem2  26241  aalioulem3  26242  aalioulem5  26244  aaliou2b  26249  aaliou3lem3  26252  ulmbdd  26307  iblulm  26316  radcnvlem1  26322  abelthlem5  26345  log1  26494  logm1  26498  rplogcl  26513  logge0  26514  logge0b  26540  loggt0b  26541  divlogrlim  26544  logno1  26545  logcnlem2  26552  logcnlem3  26553  logcnlem4  26554  logtayl  26569  cxpcn3lem  26657  resqrtcn  26659  zrtelqelz  26668  loglesqrt  26671  ang180lem2  26720  isosctrlem2  26729  angpined  26740  efrlim  26879  efrlimOLD  26880  sqrtlim  26883  cxp2limlem  26886  logdifbnd  26904  emcllem4  26909  emcllem5  26910  emcllem6  26911  lgamgulmlem5  26943  lgambdd  26947  lgamcvg2  26965  relgamcl  26972  ftalem4  26986  vmalelog  27116  logfacubnd  27132  logfacbnd3  27134  logfacrlim  27135  logexprlim  27136  chpchtlim  27390  vmadivsumb  27394  rpvmasumlem  27398  dchrvmasumlem2  27409  dchrvmasumlema  27411  dchrvmasumiflem1  27412  dchrisum0fno1  27422  dchrisum0re  27424  dirith2  27439  logdivsum  27444  mulog2sumlem2  27446  vmalogdivsum2  27449  vmalogdivsum  27450  2vmadivsumlem  27451  log2sumbnd  27455  selbergb  27460  selberg2lem  27461  selberg2b  27463  chpdifbndlem1  27464  chpdifbndlem2  27465  logdivbnd  27467  selberg3lem1  27468  selberg3lem2  27469  selberg3  27470  selberg4lem1  27471  selberg4  27472  selberg3r  27480  selberg4r  27481  selberg34r  27482  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6a  27493  pntrlog2bndlem6  27494  pntrlog2bnd  27495  pntpbnd1a  27496  pntibndlem3  27503  pntlemd  27505  pntlemn  27511  pntlemq  27512  pntlemr  27513  pntlemj  27514  pntlemk  27517  pntlem3  27520  pntleml  27522  ostth3  27549  smcnlem  30626  blocnilem  30733  0cnop  31908  0cnfn  31909  nmcopexi  31956  nmcfnexi  31980  xrnarchi  33138  xrge0iifcnv  33923  omssubadd  34291  hgt750lemd  34639  sinccvg  35660  iprodgam  35729  faclimlem1  35730  faclimlem3  35732  faclim  35733  iprodfac  35734  opnrebl2  36309  unblimceq0  36495  ptrecube  37614  mblfinlem4  37654  ftc1anc  37695  totbndbnd  37783  rrntotbnd  37830  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p5  42063  aks4d1p8  42075  explt1d  42311  expeq1d  42312  rencldnfi  42809  irrapxlem1  42810  irrapxlem2  42811  irrapxlem3  42812  pell1qrgaplem  42861  pell14qrgapw  42864  reglogltb  42879  reglogleb  42880  pellfund14  42886  binomcxplemnotnn0  44345  supxrgere  45329  supxrgelem  45333  suplesup  45335  xrlexaddrp  45348  xralrple2  45350  ltdivgt1  45352  infleinf  45368  xralrple3  45370  iooiinicc  45540  iooiinioc  45554  limcdm0  45616  constlimc  45622  0ellimcdiv  45647  climrescn  45746  climxrre  45748  sinaover2ne0  45866  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  wallispi  46068  stirlinglem5  46076  stirlinglem6  46077  stirlinglem10  46081  fourierdlem30  46135  etransclem48  46280  hoicvrrex  46554  hoidmvlelem3  46595  vonioolem1  46678  smfmullem1  46789  smfmullem2  46790  smfmullem3  46791  perfectALTVlem2  47723  regt1loggt0  48525