Theorem 1rp 13017

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 11240	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11764	. 2 ⊢ 0 < 1
3	1, 2	elrpii 13016	1 ⊢ 1 ∈ ℝ+

Syntax hints:   ∈ wcel 2109  1c1 11135  ℝ⁺crp 13013

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 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-po 5566  df-so 5567  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  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 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-rp 13014

This theorem is referenced by:  rpreccl  13040  xov1plusxeqvd  13520  modfrac  13906  rpexpcl  14103  caubnd2  15381  reccn2  15618  rlimo1  15638  rlimno1  15675  caurcvgr  15695  caurcvg  15698  caurcvg2  15699  caucvg  15700  caucvgb  15701  fprodrpcl  15977  rprisefaccl  16044  isprm6  16738  rpmsubg  21404  unirnblps  24363  unirnbl  24364  mopnex  24463  metustfbas  24501  nrginvrcnlem  24635  nrginvrcn  24636  tgioo  24740  xrsmopn  24757  zdis  24761  lebnumlem3  24918  lebnum  24919  xlebnum  24920  nmhmcn  25076  caun0  25238  cmetcaulem  25245  iscmet3lem3  25247  iscmet3lem1  25248  iscmet3lem2  25249  iscmet3  25250  cmpcmet  25276  cncmet  25279  minveclem3b  25385  nulmbl2  25494  dveflem  25940  aalioulem2  26298  aalioulem3  26299  aalioulem5  26301  aaliou2b  26306  aaliou3lem3  26309  ulmbdd  26364  iblulm  26373  radcnvlem1  26379  abelthlem5  26402  log1  26551  logm1  26555  rplogcl  26570  logge0  26571  logge0b  26597  loggt0b  26598  divlogrlim  26601  logno1  26602  logcnlem2  26609  logcnlem3  26610  logcnlem4  26611  logtayl  26626  cxpcn3lem  26714  resqrtcn  26716  zrtelqelz  26725  loglesqrt  26728  ang180lem2  26777  isosctrlem2  26786  angpined  26797  efrlim  26936  efrlimOLD  26937  sqrtlim  26940  cxp2limlem  26943  logdifbnd  26961  emcllem4  26966  emcllem5  26967  emcllem6  26968  lgamgulmlem5  27000  lgambdd  27004  lgamcvg2  27022  relgamcl  27029  ftalem4  27043  vmalelog  27173  logfacubnd  27189  logfacbnd3  27191  logfacrlim  27192  logexprlim  27193  chpchtlim  27447  vmadivsumb  27451  rpvmasumlem  27455  dchrvmasumlem2  27466  dchrvmasumlema  27468  dchrvmasumiflem1  27469  dchrisum0fno1  27479  dchrisum0re  27481  dirith2  27496  logdivsum  27501  mulog2sumlem2  27503  vmalogdivsum2  27506  vmalogdivsum  27507  2vmadivsumlem  27508  log2sumbnd  27512  selbergb  27517  selberg2lem  27518  selberg2b  27520  chpdifbndlem1  27521  chpdifbndlem2  27522  logdivbnd  27524  selberg3lem1  27525  selberg3lem2  27526  selberg3  27527  selberg4lem1  27528  selberg4  27529  selberg3r  27537  selberg4r  27538  selberg34r  27539  pntrlog2bndlem1  27545  pntrlog2bndlem2  27546  pntrlog2bndlem3  27547  pntrlog2bndlem4  27548  pntrlog2bndlem5  27549  pntrlog2bndlem6a  27550  pntrlog2bndlem6  27551  pntrlog2bnd  27552  pntpbnd1a  27553  pntibndlem3  27560  pntlemd  27562  pntlemn  27568  pntlemq  27569  pntlemr  27570  pntlemj  27571  pntlemk  27574  pntlem3  27577  pntleml  27579  ostth3  27606  smcnlem  30683  blocnilem  30790  0cnop  31965  0cnfn  31966  nmcopexi  32013  nmcfnexi  32037  xrnarchi  33187  xrge0iifcnv  33969  omssubadd  34337  hgt750lemd  34685  sinccvg  35700  iprodgam  35764  faclimlem1  35765  faclimlem3  35767  faclim  35768  iprodfac  35769  opnrebl2  36344  unblimceq0  36530  ptrecube  37649  mblfinlem4  37689  ftc1anc  37730  totbndbnd  37818  rrntotbnd  37865  aks4d1p1p4  42089  aks4d1p1p6  42091  aks4d1p1p5  42093  aks4d1p8  42105  explt1d  42341  expeq1d  42342  rencldnfi  42819  irrapxlem1  42820  irrapxlem2  42821  irrapxlem3  42822  pell1qrgaplem  42871  pell14qrgapw  42874  reglogltb  42889  reglogleb  42890  pellfund14  42896  binomcxplemnotnn0  44355  supxrgere  45340  supxrgelem  45344  suplesup  45346  xrlexaddrp  45359  xralrple2  45361  ltdivgt1  45363  infleinf  45379  xralrple3  45381  iooiinicc  45551  iooiinioc  45565  limcdm0  45627  constlimc  45633  0ellimcdiv  45658  climrescn  45757  climxrre  45759  sinaover2ne0  45877  fprodsubrecnncnvlem  45916  fprodaddrecnncnvlem  45918  ioodvbdlimc1lem2  45941  ioodvbdlimc2lem  45943  wallispi  46079  stirlinglem5  46087  stirlinglem6  46088  stirlinglem10  46092  fourierdlem30  46146  etransclem48  46291  hoicvrrex  46565  hoidmvlelem3  46606  vonioolem1  46689  smfmullem1  46800  smfmullem2  46801  smfmullem3  46802  perfectALTVlem2  47716  regt1loggt0  48496