Theorem 1rp 13134

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 11318	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11848	. 2 ⊢ 0 < 1
3	1, 2	elrpii 13133	1 ⊢ 1 ∈ ℝ+

This proof depends on syntax axioms:   ∈ wcel 2146  1c1 11211  ℝ⁺crp 13130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-resscn 11267  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-mulcom 11274  ax-addass 11275  ax-mulass 11276  ax-distr 11277  ax-i2m1 11278  ax-1ne0 11279  ax-1rid 11280  ax-rnegex 11281  ax-rrecex 11282  ax-cnre 11283  ax-pre-lttri 11284  ax-pre-lttrn 11285  ax-pre-ltadd 11286  ax-pre-mulgt0 11287

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  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 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-po 5562  df-so 5563  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7384  df-ov 7430  df-oprab 7431  df-mpo 7432  df-er 8728  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11355  df-mnf 11356  df-xr 11357  df-ltxr 11358  df-le 11359  df-sub 11553  df-neg 11554  df-rp 13131

This theorem is used by:  rpreccl  13158  xov1plusxeqvd  13639  modfrac  14034  rpexpcl  14233  caubnd2  15537  reccn2  15776  rlimo1  15796  rlimno1  15833  caurcvgr  15853  caurcvg  15856  caurcvg2  15857  caucvg  15858  caucvgb  15859  fprodrpcl  16135  rprisefaccl  16202  isprm6  16902  rpmsubg  21749  unirnblps  24750  unirnbl  24751  mopnex  24850  metustfbas  24888  nrginvrcnlem  25022  nrginvrcn  25023  tgioo  25127  xrsmopn  25144  zdis  25148  lebnumlem3  25296  lebnum  25297  xlebnum  25298  nmhmcn  25453  caun0  25614  cmetcaulem  25621  iscmet3lem3  25623  iscmet3lem1  25624  iscmet3lem2  25625  iscmet3  25626  cmpcmet  25652  cncmet  25655  minveclem3b  25761  nulmbl2  25869  dveflem  26311  aalioulem2  26672  aalioulem3  26673  aalioulem5  26675  aaliou2b  26680  aaliou3lem3  26683  ulmbdd  26737  iblulm  26746  radcnvlem1  26752  abelthlem5  26774  log1  26925  logm1  26929  rplogcl  26944  logge0  26945  logge0b  26971  loggt0b  26972  divlogrlim  26975  logno1  26976  logcnlem2  26983  logcnlem3  26984  logcnlem4  26985  logtayl  27000  cxpcn3lem  27087  resqrtcn  27089  zrtelqelz  27098  loglesqrt  27101  ang180lem2  27150  isosctrlem2  27159  angpined  27170  efrlim  27309  sqrtlim  27312  cxp2limlem  27315  logdifbnd  27333  emcllem4  27338  emcllem5  27339  emcllem6  27340  lgamgulmlem5  27372  lgambdd  27376  lgamcvg2  27394  relgamcl  27401  ftalem4  27415  vmalelog  27544  logfacubnd  27560  logfacbnd3  27562  logfacrlim  27563  logexprlim  27564  chpchtlim  27818  vmadivsumb  27822  rpvmasumlem  27826  dchrvmasumlem2  27837  dchrvmasumlema  27839  dchrvmasumiflem1  27840  dchrisum0fno1  27850  dchrisum0re  27852  dirith2  27867  logdivsum  27872  mulog2sumlem2  27874  vmalogdivsum2  27877  vmalogdivsum  27878  2vmadivsumlem  27879  log2sumbnd  27883  selbergb  27888  selberg2lem  27889  selberg2b  27891  chpdifbndlem1  27892  chpdifbndlem2  27893  logdivbnd  27895  selberg3lem1  27896  selberg3lem2  27897  selberg3  27898  selberg4lem1  27899  selberg4  27900  selberg3r  27908  selberg4r  27909  selberg34r  27910  pntrlog2bndlem1  27916  pntrlog2bndlem2  27917  pntrlog2bndlem3  27918  pntrlog2bndlem4  27919  pntrlog2bndlem5  27920  pntrlog2bndlem6a  27921  pntrlog2bndlem6  27922  pntrlog2bnd  27923  pntpbnd1a  27924  pntibndlem3  27931  pntlemd  27933  pntlemn  27939  pntlemq  27940  pntlemr  27941  pntlemj  27942  pntlemk  27945  pntlem3  27948  pntleml  27950  ostth3  27977  smcnlem  31311  blocnilem  31418  0cnop  32593  0cnfn  32594  nmcopexi  32641  nmcfnexi  32665  xrnarchi  33798  xrge0iifcnv  34618  hgt750lemd  35330  sinccvg  36559  iprodgam  36634  faclimlem1  36635  faclimlem3  36637  faclim  36638  iprodfac  36639  opnrebl2  37236  unblimceq0  37500  qdiff  38388  ptrecube  38678  mblfinlem4  38718  ftc1anc  38759  totbndbnd  38863  rrntotbnd  38910  aks4d1p1p4  43261  aks4d1p1p6  43263  aks4d1p1p5  43265  aks4d1p8  43277  explt1d  43520  expeq1d  43521  rencldnfi  43968  irrapxlem1  43969  irrapxlem2  43970  irrapxlem3  43971  pell1qrgaplem  44020  pell14qrgapw  44023  reglogltb  44038  reglogleb  44039  pellfund14  44045  binomcxplemnotnn0  45480  supxrgere  46484  supxrgelem  46488  suplesup  46490  xrlexaddrp  46503  xralrple2  46505  ltdivgt1  46507  infleinf  46522  xralrple3  46524  iooiinicc  46693  iooiinioc  46707  limcdm0  46769  constlimc  46775  0ellimcdiv  46798  climrescn  46897  climxrre  46899  sinaover2ne0  47017  fprodsubrecnncnvlem  47056  fprodaddrecnncnvlem  47058  ioodvbdlimc1lem2  47081  ioodvbdlimc2lem  47083  wallispi  47219  stirlinglem5  47227  stirlinglem6  47228  stirlinglem10  47232  fourierdlem30  47286  etransclem48  47431  hoicvrrex  47705  hoidmvlelem3  47746  vonioolem1  47829  smfmullem1  47940  smfmullem2  47941  smfmullem3  47942  perfectALTVlem2  48959  regt1loggt0  49787