Theorem 1rp 12946

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 11144	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11672	. 2 ⊢ 0 < 1
3	1, 2	elrpii 12945	1 ⊢ 1 ∈ ℝ+

Syntax hints:   ∈ wcel 2114  1c1 11039  ℝ⁺crp 12942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-rp 12943

This theorem is referenced by:  rpreccl  12970  xov1plusxeqvd  13451  modfrac  13843  rpexpcl  14042  caubnd2  15320  reccn2  15559  rlimo1  15579  rlimno1  15616  caurcvgr  15636  caurcvg  15639  caurcvg2  15640  caucvg  15641  caucvgb  15642  fprodrpcl  15921  rprisefaccl  15988  isprm6  16684  rpmsubg  21411  unirnblps  24384  unirnbl  24385  mopnex  24484  metustfbas  24522  nrginvrcnlem  24656  nrginvrcn  24657  tgioo  24761  xrsmopn  24778  zdis  24782  lebnumlem3  24930  lebnum  24931  xlebnum  24932  nmhmcn  25087  caun0  25248  cmetcaulem  25255  iscmet3lem3  25257  iscmet3lem1  25258  iscmet3lem2  25259  iscmet3  25260  cmpcmet  25286  cncmet  25289  minveclem3b  25395  nulmbl2  25503  dveflem  25946  aalioulem2  26299  aalioulem3  26300  aalioulem5  26302  aaliou2b  26307  aaliou3lem3  26310  ulmbdd  26363  iblulm  26372  radcnvlem1  26378  abelthlem5  26400  log1  26549  logm1  26553  rplogcl  26568  logge0  26569  logge0b  26595  loggt0b  26596  divlogrlim  26599  logno1  26600  logcnlem2  26607  logcnlem3  26608  logcnlem4  26609  logtayl  26624  cxpcn3lem  26711  resqrtcn  26713  zrtelqelz  26722  loglesqrt  26725  ang180lem2  26774  isosctrlem2  26783  angpined  26794  efrlim  26933  sqrtlim  26936  cxp2limlem  26939  logdifbnd  26957  emcllem4  26962  emcllem5  26963  emcllem6  26964  lgamgulmlem5  26996  lgambdd  27000  lgamcvg2  27018  relgamcl  27025  ftalem4  27039  vmalelog  27168  logfacubnd  27184  logfacbnd3  27186  logfacrlim  27187  logexprlim  27188  chpchtlim  27442  vmadivsumb  27446  rpvmasumlem  27450  dchrvmasumlem2  27461  dchrvmasumlema  27463  dchrvmasumiflem1  27464  dchrisum0fno1  27474  dchrisum0re  27476  dirith2  27491  logdivsum  27496  mulog2sumlem2  27498  vmalogdivsum2  27501  vmalogdivsum  27502  2vmadivsumlem  27503  log2sumbnd  27507  selbergb  27512  selberg2lem  27513  selberg2b  27515  chpdifbndlem1  27516  chpdifbndlem2  27517  logdivbnd  27519  selberg3lem1  27520  selberg3lem2  27521  selberg3  27522  selberg4lem1  27523  selberg4  27524  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6a  27545  pntrlog2bndlem6  27546  pntrlog2bnd  27547  pntpbnd1a  27548  pntibndlem3  27555  pntlemd  27557  pntlemn  27563  pntlemq  27564  pntlemr  27565  pntlemj  27566  pntlemk  27569  pntlem3  27572  pntleml  27574  ostth3  27601  smcnlem  30768  blocnilem  30875  0cnop  32050  0cnfn  32051  nmcopexi  32098  nmcfnexi  32122  xrnarchi  33245  xrge0iifcnv  34077  omssubadd  34444  hgt750lemd  34792  sinccvg  35855  iprodgam  35924  faclimlem1  35925  faclimlem3  35927  faclim  35928  iprodfac  35929  opnrebl2  36503  unblimceq0  36767  qdiff  37641  ptrecube  37941  mblfinlem4  37981  ftc1anc  38022  totbndbnd  38110  rrntotbnd  38157  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p5  42514  aks4d1p8  42526  explt1d  42755  expeq1d  42756  rencldnfi  43249  irrapxlem1  43250  irrapxlem2  43251  irrapxlem3  43252  pell1qrgaplem  43301  pell14qrgapw  43304  reglogltb  43319  reglogleb  43320  pellfund14  43326  binomcxplemnotnn0  44783  supxrgere  45763  supxrgelem  45767  suplesup  45769  xrlexaddrp  45782  xralrple2  45784  ltdivgt1  45786  infleinf  45801  xralrple3  45803  iooiinicc  45972  iooiinioc  45986  limcdm0  46048  constlimc  46054  0ellimcdiv  46077  climrescn  46176  climxrre  46178  sinaover2ne0  46296  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  wallispi  46498  stirlinglem5  46506  stirlinglem6  46507  stirlinglem10  46511  fourierdlem30  46565  etransclem48  46710  hoicvrrex  46984  hoidmvlelem3  47025  vonioolem1  47108  smfmullem1  47219  smfmullem2  47220  smfmullem3  47221  perfectALTVlem2  48198  regt1loggt0  49012