Theorem 1rp 12396

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 10643	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11164	. 2 ⊢ 0 < 1
3	1, 2	elrpii 12395	1 ⊢ 1 ∈ ℝ+

Syntax hints:   ∈ wcel 2114  1c1 10540  ℝ⁺crp 12392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-po 5476  df-so 5477  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-rp 12393

This theorem is referenced by:  rpreccl  12418  xov1plusxeqvd  12887  modfrac  13255  rpexpcl  13451  caubnd2  14719  reccn2  14955  rlimo1  14975  rlimno1  15012  caurcvgr  15032  caurcvg  15035  caurcvg2  15036  caucvg  15037  caucvgb  15038  fprodrpcl  15312  rprisefaccl  15379  isprm6  16060  rpmsubg  20611  unirnblps  23031  unirnbl  23032  mopnex  23131  metustfbas  23169  nrginvrcnlem  23302  nrginvrcn  23303  tgioo  23406  xrsmopn  23422  zdis  23426  lebnumlem3  23569  lebnum  23570  xlebnum  23571  nmhmcn  23726  caun0  23886  cmetcaulem  23893  iscmet3lem3  23895  iscmet3lem1  23896  iscmet3lem2  23897  iscmet3  23898  cmpcmet  23924  cncmet  23927  minveclem3b  24033  nulmbl2  24139  dveflem  24578  aalioulem2  24924  aalioulem3  24925  aalioulem5  24927  aaliou2b  24932  aaliou3lem3  24935  ulmbdd  24988  iblulm  24997  radcnvlem1  25003  abelthlem5  25025  log1  25171  logm1  25174  rplogcl  25189  logge0  25190  logge0b  25216  loggt0b  25217  divlogrlim  25220  logno1  25221  logcnlem2  25228  logcnlem3  25229  logcnlem4  25230  logtayl  25245  cxpcn3lem  25330  resqrtcn  25332  loglesqrt  25341  ang180lem2  25390  isosctrlem2  25399  angpined  25410  efrlim  25549  sqrtlim  25552  cxp2limlem  25555  logdifbnd  25573  emcllem4  25578  emcllem5  25579  emcllem6  25580  lgamgulmlem5  25612  lgambdd  25616  lgamcvg2  25634  relgamcl  25641  ftalem4  25655  vmalelog  25783  logfacubnd  25799  logfacbnd3  25801  logfacrlim  25802  logexprlim  25803  chpchtlim  26057  vmadivsumb  26061  rpvmasumlem  26065  dchrvmasumlem2  26076  dchrvmasumlema  26078  dchrvmasumiflem1  26079  dchrisum0fno1  26089  dchrisum0re  26091  dirith2  26106  logdivsum  26111  mulog2sumlem2  26113  vmalogdivsum2  26116  vmalogdivsum  26117  2vmadivsumlem  26118  log2sumbnd  26122  selbergb  26127  selberg2lem  26128  selberg2b  26130  chpdifbndlem1  26131  chpdifbndlem2  26132  logdivbnd  26134  selberg3lem1  26135  selberg3lem2  26136  selberg3  26137  selberg4lem1  26138  selberg4  26139  selberg3r  26147  selberg4r  26148  selberg34r  26149  pntrlog2bndlem1  26155  pntrlog2bndlem2  26156  pntrlog2bndlem3  26157  pntrlog2bndlem4  26158  pntrlog2bndlem5  26159  pntrlog2bndlem6a  26160  pntrlog2bndlem6  26161  pntrlog2bnd  26162  pntpbnd1a  26163  pntibndlem3  26170  pntlemd  26172  pntlemn  26178  pntlemq  26179  pntlemr  26180  pntlemj  26181  pntlemk  26184  pntlem3  26187  pntleml  26189  ostth3  26216  smcnlem  28476  blocnilem  28583  0cnop  29758  0cnfn  29759  nmcopexi  29806  nmcfnexi  29830  xrnarchi  30815  xrge0iifcnv  31178  omssubadd  31560  hgt750lemd  31921  sinccvg  32918  iprodgam  32976  faclimlem1  32977  faclimlem3  32979  faclim  32980  iprodfac  32981  opnrebl2  33671  unblimceq0  33848  ptrecube  34894  mblfinlem4  34934  ftc1anc  34977  totbndbnd  35069  rrntotbnd  35116  zrtelqelz  39199  rencldnfi  39425  irrapxlem1  39426  irrapxlem2  39427  irrapxlem3  39428  pell1qrgaplem  39477  pell14qrgapw  39480  reglogltb  39495  reglogleb  39496  pellfund14  39502  binomcxplemnotnn0  40695  supxrgere  41608  supxrgelem  41612  suplesup  41614  xrlexaddrp  41627  xralrple2  41629  ltdivgt1  41631  infleinf  41647  xralrple3  41649  iooiinicc  41825  iooiinioc  41839  limcdm0  41906  constlimc  41912  0ellimcdiv  41937  climrescn  42036  climxrre  42038  sinaover2ne0  42156  fprodsubrecnncnvlem  42198  fprodaddrecnncnvlem  42200  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  wallispi  42362  stirlinglem5  42370  stirlinglem6  42371  stirlinglem10  42375  fourierdlem30  42429  etransclem48  42574  hoicvrrex  42845  hoidmvlelem3  42886  vonioolem1  42969  smfmullem1  43073  smfmullem2  43074  smfmullem3  43075  perfectALTVlem2  43894  regt1loggt0  44603