MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1rp Structured version   Visualization version   GIF version

Theorem 1rp 11668
Description: 1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.)
Assertion
Ref Expression
1rp 1 ∈ ℝ+

Proof of Theorem 1rp
StepHypRef Expression
1 1re 9895 . 2 1 ∈ ℝ
2 0lt1 10399 . 2 0 < 1
31, 2elrpii 11667 1 1 ∈ ℝ+
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  1c1 9793  +crp 11664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-rp 11665
This theorem is referenced by:  rpreccl  11689  xov1plusxeqvd  12145  modfrac  12500  rpexpcl  12696  caubnd2  13891  reccn2  14121  rlimo1  14141  rlimno1  14178  caurcvgr  14198  caurcvg  14201  caurcvg2  14202  caucvg  14203  caucvgb  14204  fprodrpcl  14471  rprisefaccl  14539  isprm6  15210  rpmsubg  19575  unirnblps  21975  unirnbl  21976  mopnex  22075  metustfbas  22113  dscopn  22129  nrginvrcnlem  22238  nrginvrcn  22239  tgioo  22339  xrsmopn  22355  zdis  22359  lebnumlem3  22501  lebnum  22502  xlebnum  22503  nmhmcn  22659  caun0  22805  cmetcaulem  22812  iscmet3lem3  22814  iscmet3lem1  22815  iscmet3lem2  22816  iscmet3  22817  cmpcmet  22841  cncmet  22844  minveclem3b  22924  nulmbl2  23028  dveflem  23463  aalioulem2  23809  aalioulem3  23810  aalioulem5  23812  aaliou2b  23817  aaliou3lem3  23820  ulmbdd  23873  iblulm  23882  radcnvlem1  23888  abelthlem2  23907  abelthlem5  23910  abelthlem7  23913  log1  24053  logm1  24056  rplogcl  24071  logge0  24072  divlogrlim  24098  logno1  24099  logcnlem2  24106  logcnlem3  24107  logcnlem4  24108  dvlog2  24116  logtayl  24123  logtayl2  24125  cxpcn3lem  24205  resqrtcn  24207  loglesqrt  24216  ang180lem2  24257  isosctrlem2  24266  angpined  24274  efrlim  24413  sqrtlim  24416  cxp2limlem  24419  logdifbnd  24437  emcllem4  24442  emcllem5  24443  emcllem6  24444  lgamgulmlem5  24476  lgambdd  24480  lgamcvg2  24498  relgamcl  24505  ftalem4  24519  vmalelog  24647  logfacubnd  24663  logfacbnd3  24665  logfacrlim  24666  logexprlim  24667  chpchtlim  24885  vmadivsumb  24889  rpvmasumlem  24893  dchrvmasumlem2  24904  dchrvmasumlema  24906  dchrvmasumiflem1  24907  dchrisum0fno1  24917  dchrisum0re  24919  dirith2  24934  logdivsum  24939  mulog2sumlem2  24941  vmalogdivsum2  24944  vmalogdivsum  24945  2vmadivsumlem  24946  log2sumbnd  24950  selbergb  24955  selberg2lem  24956  selberg2b  24958  chpdifbndlem1  24959  chpdifbndlem2  24960  logdivbnd  24962  selberg3lem1  24963  selberg3lem2  24964  selberg3  24965  selberg4lem1  24966  selberg4  24967  selberg3r  24975  selberg4r  24976  selberg34r  24977  pntrlog2bndlem1  24983  pntrlog2bndlem2  24984  pntrlog2bndlem3  24985  pntrlog2bndlem4  24986  pntrlog2bndlem5  24987  pntrlog2bndlem6a  24988  pntrlog2bndlem6  24989  pntrlog2bnd  24990  pntpbnd1a  24991  pntibndlem3  24998  pntlemd  25000  pntlemn  25006  pntlemq  25007  pntlemr  25008  pntlemj  25009  pntlemk  25012  pntlem3  25015  pntleml  25017  ostth3  25044  smcnlem  26737  blocnilem  26849  0cnop  28028  0cnfn  28029  nmcopexi  28076  nmcfnexi  28100  xrnarchi  28875  xrge0iifcnv  29113  omssubadd  29495  sinccvg  30627  iprodgam  30687  faclimlem1  30688  faclimlem3  30690  faclim  30691  iprodfac  30692  opnrebl2  31292  unblimceq0  31474  ptrecube  32375  mblfinlem4  32415  ftc1anc  32459  totbndbnd  32554  rrntotbnd  32601  rencldnfi  36199  irrapxlem1  36200  irrapxlem2  36201  irrapxlem3  36202  pell1qrgaplem  36251  pell14qrgapw  36254  reglogltb  36269  reglogleb  36270  pellfund14  36276  binomcxplemnotnn0  37373  supxrgere  38287  supxrgelem  38291  suplesup  38293  xrlexaddrp  38306  xralrple2  38308  ltdivgt1  38310  infleinf  38326  xralrple3  38328  iooiinicc  38413  iooiinioc  38427  limcdm0  38482  constlimc  38488  0ellimcdiv  38513  sinaover2ne0  38548  fprodsubrecnncnvlem  38591  fprodaddrecnncnvlem  38593  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  wallispi  38760  stirlinglem5  38768  stirlinglem6  38769  stirlinglem10  38773  fourierdlem30  38827  etransclem48  38972  hoicvrrex  39243  hoidmvlelem3  39284  vonioolem1  39368  smfmullem1  39473  smfmullem2  39474  smfmullem3  39475  perfectALTVlem2  39963  logge0b  42118  loggt0b  42119  regt1loggt0  42123
  Copyright terms: Public domain W3C validator