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

Theorem 1rp 12383
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 10630 . 2 1 ∈ ℝ
2 0lt1 11151 . 2 0 < 1
31, 2elrpii 12382 1 1 ∈ ℝ+
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  1c1 10527  +crp 12379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-po 5468  df-so 5469  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-rp 12380
This theorem is referenced by:  rpreccl  12405  xov1plusxeqvd  12874  modfrac  13242  rpexpcl  13438  caubnd2  14707  reccn2  14943  rlimo1  14963  rlimno1  15000  caurcvgr  15020  caurcvg  15023  caurcvg2  15024  caucvg  15025  caucvgb  15026  fprodrpcl  15300  rprisefaccl  15367  isprm6  16048  rpmsubg  20539  unirnblps  22958  unirnbl  22959  mopnex  23058  metustfbas  23096  nrginvrcnlem  23229  nrginvrcn  23230  tgioo  23333  xrsmopn  23349  zdis  23353  lebnumlem3  23496  lebnum  23497  xlebnum  23498  nmhmcn  23653  caun0  23813  cmetcaulem  23820  iscmet3lem3  23822  iscmet3lem1  23823  iscmet3lem2  23824  iscmet3  23825  cmpcmet  23851  cncmet  23854  minveclem3b  23960  nulmbl2  24066  dveflem  24505  aalioulem2  24851  aalioulem3  24852  aalioulem5  24854  aaliou2b  24859  aaliou3lem3  24862  ulmbdd  24915  iblulm  24924  radcnvlem1  24930  abelthlem5  24952  log1  25096  logm1  25099  rplogcl  25114  logge0  25115  logge0b  25141  loggt0b  25142  divlogrlim  25145  logno1  25146  logcnlem2  25153  logcnlem3  25154  logcnlem4  25155  logtayl  25170  cxpcn3lem  25255  resqrtcn  25257  loglesqrt  25266  ang180lem2  25315  isosctrlem2  25324  angpined  25335  efrlim  25475  sqrtlim  25478  cxp2limlem  25481  logdifbnd  25499  emcllem4  25504  emcllem5  25505  emcllem6  25506  lgamgulmlem5  25538  lgambdd  25542  lgamcvg2  25560  relgamcl  25567  ftalem4  25581  vmalelog  25709  logfacubnd  25725  logfacbnd3  25727  logfacrlim  25728  logexprlim  25729  chpchtlim  25983  vmadivsumb  25987  rpvmasumlem  25991  dchrvmasumlem2  26002  dchrvmasumlema  26004  dchrvmasumiflem1  26005  dchrisum0fno1  26015  dchrisum0re  26017  dirith2  26032  logdivsum  26037  mulog2sumlem2  26039  vmalogdivsum2  26042  vmalogdivsum  26043  2vmadivsumlem  26044  log2sumbnd  26048  selbergb  26053  selberg2lem  26054  selberg2b  26056  chpdifbndlem1  26057  chpdifbndlem2  26058  logdivbnd  26060  selberg3lem1  26061  selberg3lem2  26062  selberg3  26063  selberg4lem1  26064  selberg4  26065  selberg3r  26073  selberg4r  26074  selberg34r  26075  pntrlog2bndlem1  26081  pntrlog2bndlem2  26082  pntrlog2bndlem3  26083  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntrlog2bndlem6a  26086  pntrlog2bndlem6  26087  pntrlog2bnd  26088  pntpbnd1a  26089  pntibndlem3  26096  pntlemd  26098  pntlemn  26104  pntlemq  26105  pntlemr  26106  pntlemj  26107  pntlemk  26110  pntlem3  26113  pntleml  26115  ostth3  26142  smcnlem  28402  blocnilem  28509  0cnop  29684  0cnfn  29685  nmcopexi  29732  nmcfnexi  29756  xrnarchi  30741  xrge0iifcnv  31076  omssubadd  31458  hgt750lemd  31819  sinccvg  32814  iprodgam  32872  faclimlem1  32873  faclimlem3  32875  faclim  32876  iprodfac  32877  opnrebl2  33567  unblimceq0  33744  ptrecube  34774  mblfinlem4  34814  ftc1anc  34857  totbndbnd  34950  rrntotbnd  34997  zrtelqelz  39072  rencldnfi  39298  irrapxlem1  39299  irrapxlem2  39300  irrapxlem3  39301  pell1qrgaplem  39350  pell14qrgapw  39353  reglogltb  39368  reglogleb  39369  pellfund14  39375  binomcxplemnotnn0  40568  supxrgere  41481  supxrgelem  41485  suplesup  41487  xrlexaddrp  41500  xralrple2  41502  ltdivgt1  41504  infleinf  41520  xralrple3  41522  iooiinicc  41698  iooiinioc  41712  limcdm0  41779  constlimc  41785  0ellimcdiv  41810  climrescn  41909  climxrre  41911  sinaover2ne0  42029  fprodsubrecnncnvlem  42071  fprodaddrecnncnvlem  42073  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  wallispi  42236  stirlinglem5  42244  stirlinglem6  42245  stirlinglem10  42249  fourierdlem30  42303  etransclem48  42448  hoicvrrex  42719  hoidmvlelem3  42760  vonioolem1  42843  smfmullem1  42947  smfmullem2  42948  smfmullem3  42949  perfectALTVlem2  43734  regt1loggt0  44494
  Copyright terms: Public domain W3C validator