Theorem 1rp 12940

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 11138	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11666	. 2 ⊢ 0 < 1
3	1, 2	elrpii 12939	1 ⊢ 1 ∈ ℝ+

Syntax hints:   ∈ wcel 2114  1c1 11033  ℝ⁺crp 12936

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 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-rp 12937

This theorem is referenced by:  rpreccl  12964  xov1plusxeqvd  13445  modfrac  13837  rpexpcl  14036  caubnd2  15314  reccn2  15553  rlimo1  15573  rlimno1  15610  caurcvgr  15630  caurcvg  15633  caurcvg2  15634  caucvg  15635  caucvgb  15636  fprodrpcl  15915  rprisefaccl  15982  isprm6  16678  rpmsubg  21424  unirnblps  24397  unirnbl  24398  mopnex  24497  metustfbas  24535  nrginvrcnlem  24669  nrginvrcn  24670  tgioo  24774  xrsmopn  24791  zdis  24795  lebnumlem3  24943  lebnum  24944  xlebnum  24945  nmhmcn  25100  caun0  25261  cmetcaulem  25268  iscmet3lem3  25270  iscmet3lem1  25271  iscmet3lem2  25272  iscmet3  25273  cmpcmet  25299  cncmet  25302  minveclem3b  25408  nulmbl2  25516  dveflem  25959  aalioulem2  26313  aalioulem3  26314  aalioulem5  26316  aaliou2b  26321  aaliou3lem3  26324  ulmbdd  26379  iblulm  26388  radcnvlem1  26394  abelthlem5  26416  log1  26565  logm1  26569  rplogcl  26584  logge0  26585  logge0b  26611  loggt0b  26612  divlogrlim  26615  logno1  26616  logcnlem2  26623  logcnlem3  26624  logcnlem4  26625  logtayl  26640  cxpcn3lem  26727  resqrtcn  26729  zrtelqelz  26738  loglesqrt  26741  ang180lem2  26790  isosctrlem2  26799  angpined  26810  efrlim  26949  efrlimOLD  26950  sqrtlim  26953  cxp2limlem  26956  logdifbnd  26974  emcllem4  26979  emcllem5  26980  emcllem6  26981  lgamgulmlem5  27013  lgambdd  27017  lgamcvg2  27035  relgamcl  27042  ftalem4  27056  vmalelog  27185  logfacubnd  27201  logfacbnd3  27203  logfacrlim  27204  logexprlim  27205  chpchtlim  27459  vmadivsumb  27463  rpvmasumlem  27467  dchrvmasumlem2  27478  dchrvmasumlema  27480  dchrvmasumiflem1  27481  dchrisum0fno1  27491  dchrisum0re  27493  dirith2  27508  logdivsum  27513  mulog2sumlem2  27515  vmalogdivsum2  27518  vmalogdivsum  27519  2vmadivsumlem  27520  log2sumbnd  27524  selbergb  27529  selberg2lem  27530  selberg2b  27532  chpdifbndlem1  27533  chpdifbndlem2  27534  logdivbnd  27536  selberg3lem1  27537  selberg3lem2  27538  selberg3  27539  selberg4lem1  27540  selberg4  27541  selberg3r  27549  selberg4r  27550  selberg34r  27551  pntrlog2bndlem1  27557  pntrlog2bndlem2  27558  pntrlog2bndlem3  27559  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntrlog2bndlem6a  27562  pntrlog2bndlem6  27563  pntrlog2bnd  27564  pntpbnd1a  27565  pntibndlem3  27572  pntlemd  27574  pntlemn  27580  pntlemq  27581  pntlemr  27582  pntlemj  27583  pntlemk  27586  pntlem3  27589  pntleml  27591  ostth3  27618  smcnlem  30786  blocnilem  30893  0cnop  32068  0cnfn  32069  nmcopexi  32116  nmcfnexi  32140  xrnarchi  33263  xrge0iifcnv  34096  omssubadd  34463  hgt750lemd  34811  sinccvg  35874  iprodgam  35943  faclimlem1  35944  faclimlem3  35946  faclim  35947  iprodfac  35948  opnrebl2  36522  unblimceq0  36786  ptrecube  37958  mblfinlem4  37998  ftc1anc  38039  totbndbnd  38127  rrntotbnd  38174  aks4d1p1p4  42527  aks4d1p1p6  42529  aks4d1p1p5  42531  aks4d1p8  42543  explt1d  42772  expeq1d  42773  rencldnfi  43270  irrapxlem1  43271  irrapxlem2  43272  irrapxlem3  43273  pell1qrgaplem  43322  pell14qrgapw  43325  reglogltb  43340  reglogleb  43341  pellfund14  43347  binomcxplemnotnn0  44804  supxrgere  45784  supxrgelem  45788  suplesup  45790  xrlexaddrp  45803  xralrple2  45805  ltdivgt1  45807  infleinf  45822  xralrple3  45824  iooiinicc  45993  iooiinioc  46007  limcdm0  46069  constlimc  46075  0ellimcdiv  46098  climrescn  46197  climxrre  46199  sinaover2ne0  46317  fprodsubrecnncnvlem  46356  fprodaddrecnncnvlem  46358  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  wallispi  46519  stirlinglem5  46527  stirlinglem6  46528  stirlinglem10  46532  fourierdlem30  46586  etransclem48  46731  hoicvrrex  47005  hoidmvlelem3  47046  vonioolem1  47129  smfmullem1  47240  smfmullem2  47241  smfmullem3  47242  perfectALTVlem2  48213  regt1loggt0  49027