Theorem 1rp 12998

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 11182	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11710	. 2 ⊢ 0 < 1
3	1, 2	elrpii 12997	1 ⊢ 1 ∈ ℝ+

Syntax hints:   ∈ wcel 2143  1c1 11075  ℝ⁺crp 12994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7719  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150  ax-pre-mulgt0 11151

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-po 5556  df-so 5557  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-fv 6530  df-riota 7354  df-ov 7400  df-oprab 7401  df-mpo 7402  df-er 8679  df-en 8929  df-dom 8930  df-sdom 8931  df-pnf 11219  df-mnf 11220  df-xr 11221  df-ltxr 11222  df-le 11223  df-sub 11417  df-neg 11418  df-rp 12995

This theorem is referenced by:  rpreccl  13022  xov1plusxeqvd  13503  modfrac  13895  rpexpcl  14094  caubnd2  15386  reccn2  15625  rlimo1  15645  rlimno1  15682  caurcvgr  15702  caurcvg  15705  caurcvg2  15706  caucvg  15707  caucvgb  15708  fprodrpcl  15987  rprisefaccl  16054  isprm6  16750  rpmsubg  21484  unirnblps  24480  unirnbl  24481  mopnex  24580  metustfbas  24618  nrginvrcnlem  24752  nrginvrcn  24753  tgioo  24857  xrsmopn  24874  zdis  24878  lebnumlem3  25026  lebnum  25027  xlebnum  25028  nmhmcn  25183  caun0  25344  cmetcaulem  25351  iscmet3lem3  25353  iscmet3lem1  25354  iscmet3lem2  25355  iscmet3  25356  cmpcmet  25382  cncmet  25385  minveclem3b  25491  nulmbl2  25599  dveflem  26042  aalioulem2  26398  aalioulem3  26399  aalioulem5  26401  aaliou2b  26406  aaliou3lem3  26409  ulmbdd  26462  iblulm  26471  radcnvlem1  26477  abelthlem5  26499  log1  26651  logm1  26655  rplogcl  26670  logge0  26671  logge0b  26697  loggt0b  26698  divlogrlim  26701  logno1  26702  logcnlem2  26709  logcnlem3  26710  logcnlem4  26711  logtayl  26726  cxpcn3lem  26813  resqrtcn  26815  zrtelqelz  26824  loglesqrt  26827  ang180lem2  26876  isosctrlem2  26885  angpined  26896  efrlim  27035  sqrtlim  27038  cxp2limlem  27041  logdifbnd  27059  emcllem4  27064  emcllem5  27065  emcllem6  27066  lgamgulmlem5  27098  lgambdd  27102  lgamcvg2  27120  relgamcl  27127  ftalem4  27141  vmalelog  27270  logfacubnd  27286  logfacbnd3  27288  logfacrlim  27289  logexprlim  27290  chpchtlim  27544  vmadivsumb  27548  rpvmasumlem  27552  dchrvmasumlem2  27563  dchrvmasumlema  27565  dchrvmasumiflem1  27566  dchrisum0fno1  27576  dchrisum0re  27578  dirith2  27593  logdivsum  27598  mulog2sumlem2  27600  vmalogdivsum2  27603  vmalogdivsum  27604  2vmadivsumlem  27605  log2sumbnd  27609  selbergb  27614  selberg2lem  27615  selberg2b  27617  chpdifbndlem1  27618  chpdifbndlem2  27619  logdivbnd  27621  selberg3lem1  27622  selberg3lem2  27623  selberg3  27624  selberg4lem1  27625  selberg4  27626  selberg3r  27634  selberg4r  27635  selberg34r  27636  pntrlog2bndlem1  27642  pntrlog2bndlem2  27643  pntrlog2bndlem3  27644  pntrlog2bndlem4  27645  pntrlog2bndlem5  27646  pntrlog2bndlem6a  27647  pntrlog2bndlem6  27648  pntrlog2bnd  27649  pntpbnd1a  27650  pntibndlem3  27657  pntlemd  27659  pntlemn  27665  pntlemq  27666  pntlemr  27667  pntlemj  27668  pntlemk  27671  pntlem3  27674  pntleml  27676  ostth3  27703  smcnlem  30901  blocnilem  31008  0cnop  32183  0cnfn  32184  nmcopexi  32231  nmcfnexi  32255  xrnarchi  33365  xrge0iifcnv  34231  omssubadd  34598  hgt750lemd  34943  sinccvg  36024  iprodgam  36093  faclimlem1  36094  faclimlem3  36096  faclim  36097  iprodfac  36098  opnrebl2  36682  unblimceq0  36946  qdiff  37820  ptrecube  38120  mblfinlem4  38160  ftc1anc  38201  totbndbnd  38289  rrntotbnd  38336  aks4d1p1p4  42689  aks4d1p1p6  42691  aks4d1p1p5  42693  aks4d1p8  42705  explt1d  42933  expeq1d  42934  rencldnfi  43399  irrapxlem1  43400  irrapxlem2  43401  irrapxlem3  43402  pell1qrgaplem  43451  pell14qrgapw  43454  reglogltb  43469  reglogleb  43470  pellfund14  43476  binomcxplemnotnn0  44933  supxrgere  45910  supxrgelem  45914  suplesup  45916  xrlexaddrp  45929  xralrple2  45931  ltdivgt1  45933  infleinf  45948  xralrple3  45950  iooiinicc  46119  iooiinioc  46133  limcdm0  46195  constlimc  46201  0ellimcdiv  46224  climrescn  46323  climxrre  46325  sinaover2ne0  46443  fprodsubrecnncnvlem  46482  fprodaddrecnncnvlem  46484  ioodvbdlimc1lem2  46507  ioodvbdlimc2lem  46509  wallispi  46645  stirlinglem5  46653  stirlinglem6  46654  stirlinglem10  46658  fourierdlem30  46712  etransclem48  46857  hoicvrrex  47131  hoidmvlelem3  47172  vonioolem1  47255  smfmullem1  47366  smfmullem2  47367  smfmullem3  47368  perfectALTVlem2  48345  regt1loggt0  49159