Theorem 1rp 12931

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 11150	. 2 ⊢ 1 ∈ ℝ
2		0lt1 11676	. 2 ⊢ 0 < 1
3	1, 2	elrpii 12930	1 ⊢ 1 ∈ ℝ+

Syntax hints:   ∈ wcel 2109  1c1 11045  ℝ⁺crp 12927

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 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  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 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-rp 12928

This theorem is referenced by:  rpreccl  12955  xov1plusxeqvd  13435  modfrac  13822  rpexpcl  14021  caubnd2  15300  reccn2  15539  rlimo1  15559  rlimno1  15596  caurcvgr  15616  caurcvg  15619  caurcvg2  15620  caucvg  15621  caucvgb  15622  fprodrpcl  15898  rprisefaccl  15965  isprm6  16660  rpmsubg  21373  unirnblps  24340  unirnbl  24341  mopnex  24440  metustfbas  24478  nrginvrcnlem  24612  nrginvrcn  24613  tgioo  24717  xrsmopn  24734  zdis  24738  lebnumlem3  24895  lebnum  24896  xlebnum  24897  nmhmcn  25053  caun0  25214  cmetcaulem  25221  iscmet3lem3  25223  iscmet3lem1  25224  iscmet3lem2  25225  iscmet3  25226  cmpcmet  25252  cncmet  25255  minveclem3b  25361  nulmbl2  25470  dveflem  25916  aalioulem2  26274  aalioulem3  26275  aalioulem5  26277  aaliou2b  26282  aaliou3lem3  26285  ulmbdd  26340  iblulm  26349  radcnvlem1  26355  abelthlem5  26378  log1  26527  logm1  26531  rplogcl  26546  logge0  26547  logge0b  26573  loggt0b  26574  divlogrlim  26577  logno1  26578  logcnlem2  26585  logcnlem3  26586  logcnlem4  26587  logtayl  26602  cxpcn3lem  26690  resqrtcn  26692  zrtelqelz  26701  loglesqrt  26704  ang180lem2  26753  isosctrlem2  26762  angpined  26773  efrlim  26912  efrlimOLD  26913  sqrtlim  26916  cxp2limlem  26919  logdifbnd  26937  emcllem4  26942  emcllem5  26943  emcllem6  26944  lgamgulmlem5  26976  lgambdd  26980  lgamcvg2  26998  relgamcl  27005  ftalem4  27019  vmalelog  27149  logfacubnd  27165  logfacbnd3  27167  logfacrlim  27168  logexprlim  27169  chpchtlim  27423  vmadivsumb  27427  rpvmasumlem  27431  dchrvmasumlem2  27442  dchrvmasumlema  27444  dchrvmasumiflem1  27445  dchrisum0fno1  27455  dchrisum0re  27457  dirith2  27472  logdivsum  27477  mulog2sumlem2  27479  vmalogdivsum2  27482  vmalogdivsum  27483  2vmadivsumlem  27484  log2sumbnd  27488  selbergb  27493  selberg2lem  27494  selberg2b  27496  chpdifbndlem1  27497  chpdifbndlem2  27498  logdivbnd  27500  selberg3lem1  27501  selberg3lem2  27502  selberg3  27503  selberg4lem1  27504  selberg4  27505  selberg3r  27513  selberg4r  27514  selberg34r  27515  pntrlog2bndlem1  27521  pntrlog2bndlem2  27522  pntrlog2bndlem3  27523  pntrlog2bndlem4  27524  pntrlog2bndlem5  27525  pntrlog2bndlem6a  27526  pntrlog2bndlem6  27527  pntrlog2bnd  27528  pntpbnd1a  27529  pntibndlem3  27536  pntlemd  27538  pntlemn  27544  pntlemq  27545  pntlemr  27546  pntlemj  27547  pntlemk  27550  pntlem3  27553  pntleml  27555  ostth3  27582  smcnlem  30676  blocnilem  30783  0cnop  31958  0cnfn  31959  nmcopexi  32006  nmcfnexi  32030  xrnarchi  33153  xrge0iifcnv  33916  omssubadd  34284  hgt750lemd  34632  sinccvg  35653  iprodgam  35722  faclimlem1  35723  faclimlem3  35725  faclim  35726  iprodfac  35727  opnrebl2  36302  unblimceq0  36488  ptrecube  37607  mblfinlem4  37647  ftc1anc  37688  totbndbnd  37776  rrntotbnd  37823  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p5  42056  aks4d1p8  42068  explt1d  42304  expeq1d  42305  rencldnfi  42802  irrapxlem1  42803  irrapxlem2  42804  irrapxlem3  42805  pell1qrgaplem  42854  pell14qrgapw  42857  reglogltb  42872  reglogleb  42873  pellfund14  42879  binomcxplemnotnn0  44338  supxrgere  45322  supxrgelem  45326  suplesup  45328  xrlexaddrp  45341  xralrple2  45343  ltdivgt1  45345  infleinf  45361  xralrple3  45363  iooiinicc  45533  iooiinioc  45547  limcdm0  45609  constlimc  45615  0ellimcdiv  45640  climrescn  45739  climxrre  45741  sinaover2ne0  45859  fprodsubrecnncnvlem  45898  fprodaddrecnncnvlem  45900  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  wallispi  46061  stirlinglem5  46069  stirlinglem6  46070  stirlinglem10  46074  fourierdlem30  46128  etransclem48  46273  hoicvrrex  46547  hoidmvlelem3  46588  vonioolem1  46671  smfmullem1  46782  smfmullem2  46783  smfmullem3  46784  perfectALTVlem2  47716  regt1loggt0  48518