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

Theorem rpred 12423
Description: A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1 (𝜑𝐴 ∈ ℝ+)
Assertion
Ref Expression
rpred (𝜑𝐴 ∈ ℝ)

Proof of Theorem rpred
StepHypRef Expression
1 rpssre 12388 . 2 + ⊆ ℝ
2 rpred.1 . 2 (𝜑𝐴 ∈ ℝ+)
31, 2sseldi 3916 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  cr 10529  +crp 12381
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-rab 3118  df-v 3446  df-in 3891  df-ss 3901  df-rp 12382
This theorem is referenced by:  rpxrd  12424  rpcnd  12425  rpregt0d  12429  rprege0d  12430  rprene0d  12431  rprecred  12434  ltmulgt11d  12458  ltmulgt12d  12459  gt0divd  12460  ge0divd  12461  lediv12ad  12482  prodge0rd  12488  xlemul1  12675  xov1plusxeqvd  12880  ltexp2a  13530  rpexpmord  13532  expcan  13533  ltexp2  13534  leexp2a  13536  expnlbnd2  13595  expmulnbnd  13596  sqrlem6  14602  cau3lem  14709  rlimcld2  14930  addcn2  14945  mulcn2  14947  reccn2  14948  o1rlimmul  14970  rlimno1  15005  caucvgrlem  15024  isumrpcl  15193  isumltss  15198  expcnv  15214  mertenslem1  15235  effsumlt  15459  recoshcl  15506  eirrlem  15552  rpnnen2lem11  15572  bitsmod  15778  prmreclem3  16247  prmreclem5  16249  4sqlem7  16273  ssblex  23038  metss2lem  23121  methaus  23130  met1stc  23131  met2ndci  23132  metustto  23163  metustexhalf  23166  nlmvscnlem2  23294  nlmvscnlem1  23295  nrginvrcnlem  23300  nmoi2  23339  nghmcn  23354  reperflem  23426  iccntr  23429  icccmplem2  23431  reconnlem2  23435  opnreen  23439  metdcnlem  23444  metnrmlem3  23469  addcnlem  23472  cnheibor  23563  cnllycmp  23564  lebnumlem3  23571  lebnumii  23574  nmoleub2lem  23722  nmoleub2lem3  23723  nmoleub2lem2  23724  nmoleub3  23727  nmhmcn  23728  ipcnlem2  23851  ipcnlem1  23852  lmnn  23870  iscfil3  23880  cfilfcls  23881  iscmet3lem1  23898  iscmet3lem2  23899  bcthlem4  23934  bcthlem5  23935  minveclem3b  24035  minveclem3  24036  ivthlem2  24059  ovolgelb  24087  ovollb2lem  24095  ovolunlem1a  24103  ovolunlem1  24104  ovoliunlem1  24109  ovoliunlem2  24110  ovolscalem1  24120  ioombl1lem2  24166  ioombl1lem4  24168  uniioombllem1  24188  uniioombllem3  24192  uniioombllem4  24193  uniioombllem5  24194  opnmbllem  24208  volcn  24213  vitalilem4  24218  itg2mulclem  24353  itg2monolem3  24359  itg2cnlem2  24369  itg2cn  24370  itggt0  24450  dveflem  24585  dvferm1lem  24590  dvferm2lem  24592  lhop1lem  24619  lhop1  24620  lhop  24622  dvcnvrelem1  24623  dvcnvrelem2  24624  dvcnvre  24625  dvfsumrlim  24637  ftc1a  24643  ftc1lem4  24645  plyeq0lem  24810  aalioulem2  24932  aalioulem4  24934  aalioulem5  24935  aalioulem6  24936  aaliou  24937  aaliou2b  24940  aaliou3lem1  24941  aaliou3lem2  24942  aaliou3lem8  24944  aaliou3lem5  24946  aaliou3lem7  24948  aaliou3lem9  24949  ulmcn  24997  ulmdvlem1  24998  mtest  25002  itgulm  25006  psercn  25024  pserdvlem1  25025  pserdvlem2  25026  pserdv  25027  abelthlem7  25036  pilem2  25050  divlogrlim  25229  logcnlem3  25238  logcnlem4  25239  logccv  25257  divcxp  25281  cxplt  25288  cxple2  25291  cxpcn3lem  25339  cxpaddlelem  25343  cxpaddle  25344  loglesqrt  25350  leibpi  25531  rlimcnp3  25556  cxplim  25560  rlimcxp  25562  cxp2limlem  25564  cxp2lim  25565  cxploglim  25566  cxploglim2  25567  divsqrtsumlem  25568  jensenlem2  25576  logdifbnd  25582  emcllem4  25587  harmonicbnd4  25599  fsumharmonic  25600  zetacvg  25603  lgamgulmlem2  25618  lgamgulmlem5  25621  lgamucov  25626  regamcl  25649  relgamcl  25650  ftalem1  25661  ftalem2  25662  ftalem3  25663  ftalem5  25665  basellem1  25669  basellem3  25671  basellem4  25672  basellem8  25676  chtwordi  25744  chpchtsum  25806  logfacrlim  25811  logexprlim  25812  bclbnd  25867  efexple  25868  bposlem1  25871  bposlem2  25872  bposlem6  25876  bposlem7  25877  chebbnd1lem3  26058  chebbnd1  26059  chtppilimlem1  26060  chtppilimlem2  26061  chpo1ubb  26068  rplogsumlem1  26071  rplogsumlem2  26072  dchrisum0lem1a  26073  rpvmasumlem  26074  dchrisumlem2  26077  dchrisumlem3  26078  dchrmusumlema  26080  dchrmusum2  26081  dchrvmasumlem1  26082  dchrvmasum2lem  26083  dchrvmasumlema  26087  dchrvmasumiflem1  26088  dchrisum0fno1  26098  dchrisum0lem1b  26102  dchrisum0lem1  26103  dchrisum0lem2  26105  dchrisum0lem3  26106  dchrisum0  26107  mulogsumlem  26118  logdivsum  26120  mulog2sumlem2  26122  vmalogdivsum2  26125  2vmadivsumlem  26127  log2sumbnd  26131  selberglem2  26133  selberg  26135  selberg2lem  26137  chpdifbndlem1  26140  chpdifbndlem2  26141  selberg3lem1  26144  selberg4lem1  26147  pntrsumbnd2  26154  pntrlog2bndlem2  26165  pntrlog2bndlem3  26166  pntrlog2bndlem5  26168  pntrlog2bndlem6a  26169  pntrlog2bndlem6  26170  pntrlog2bnd  26171  pntpbnd1a  26172  pntpbnd1  26173  pntpbnd2  26174  pntibndlem1  26176  pntibndlem2  26178  pntibndlem3  26179  pntibnd  26180  pntlemc  26182  pntlema  26183  pntlemb  26184  pntlemg  26185  pntlemh  26186  pntlemn  26187  pntlemq  26188  pntlemr  26189  pntlemj  26190  pntlemi  26191  pntlemf  26192  pntlemk  26193  pntlemo  26194  pntleme  26195  pntlem3  26196  pntlemp  26197  pntleml  26198  ostth2lem1  26205  ostth2lem3  26222  ostth2  26224  ostth3  26225  crctcshwlkn0lem5  27603  smcnlem  28483  blocnilem  28590  blocni  28591  ubthlem2  28657  minvecolem3  28662  minvecolem4  28666  minvecolem5  28667  nmcexi  29812  lnconi  29819  fsumub  30573  rpxdivcld  30639  sqsscirc1  31259  cnre2csqlem  31261  tpr2rico  31263  xrmulc1cn  31281  xrge0iifiso  31286  xrge0iifhom  31288  esumcst  31430  esumdivc  31450  dya2icoseg  31643  omssubaddlem  31665  omssubadd  31666  probmeasb  31796  sgnmulrp2  31909  signsply0  31929  logdivsqrle  32029  hgt750leme  32037  dnicn  33939  unblimceq0lem  33953  unbdqndv2lem1  33956  unbdqndv2lem2  33957  knoppndvlem18  33976  knoppndvlem21  33979  poimirlem29  35079  heicant  35085  opnmbllem0  35086  mblfinlem3  35089  itg2addnclem3  35103  itg2addnc  35104  itggt0cn  35120  ftc1cnnclem  35121  ftc1anclem6  35128  ftc1anclem7  35129  geomcau  35190  sstotbnd2  35205  isbnd3  35215  equivbnd  35221  prdsbnd2  35226  cntotbnd  35227  heibor1lem  35240  heiborlem6  35247  bfplem1  35253  bfplem2  35254  bfp  35255  rrndstprj2  35262  rrnequiv  35266  lcmineqlem21  39330  fltnlta  39606  irrapxlem4  39753  irrapxlem5  39754  irrapx1  39756  pell1qrgaplem  39801  pell14qrgapw  39804  pellqrexplicit  39805  pellqrex  39807  pellfundge  39810  pellfundgt1  39811  rmspecfund  39837  rmxycomplete  39845  rmxypos  39875  binomcxplemnotnn0  41047  suprltrp  41947  supxrge  41957  infrpge  41970  infleinflem1  41989  xralrple4  41992  recnnltrp  41996  rpgtrecnn  42000  fmul01lt1lem1  42213  fmul01lt1lem2  42214  ltmod  42267  lptre2pt  42269  addlimc  42277  0ellimcdiv  42278  limclner  42280  climleltrp  42305  climisp  42375  climxrrelem  42378  climxrre  42379  limsupgtlem  42406  liminfltlem  42433  cnrefiisplem  42458  climxlim2lem  42474  dvdivbd  42552  ioodvbdlimc1lem2  42561  ioodvbdlimc2lem  42563  itgiccshift  42609  itgperiod  42610  stoweidlem1  42630  stoweidlem3  42632  stoweidlem5  42634  stoweidlem7  42636  stoweidlem11  42640  stoweidlem13  42642  stoweidlem14  42643  stoweidlem24  42653  stoweidlem25  42654  stoweidlem26  42655  stoweidlem34  42663  stoweidlem41  42670  stoweidlem42  42671  stoweidlem49  42678  stoweidlem51  42680  stoweidlem52  42681  stoweidlem59  42688  stoweidlem60  42689  stoweidlem62  42691  stoweid  42692  wallispilem5  42698  stirlinglem1  42703  stirlinglem4  42706  stirlinglem5  42707  stirlinglem6  42708  dirkercncflem1  42732  fourierdlem30  42766  fourierdlem39  42775  fourierdlem47  42782  fourierdlem73  42808  fourierdlem81  42816  fourierdlem87  42822  fourierdlem103  42838  fourierdlem104  42839  fourierdlem107  42842  rrndistlt  42919  qndenserrnbllem  42923  sge0ltfirp  43026  sge0rpcpnf  43047  sge0xaddlem1  43059  omeiunltfirp  43145  carageniuncllem2  43148  ovnsubaddlem1  43196  hoidmvlelem1  43221  hoidmvlelem2  43222  hoidmvlelem3  43223  hoidmvlelem4  43224  hoiqssbllem1  43248  hoiqssbllem2  43249  hoiqssbllem3  43250  hspmbllem2  43253  hspmbllem3  43254  ovolval5lem1  43278  ovolval5lem2  43279  iinhoiicc  43300  vonioolem1  43306  pimrecltpos  43331  smflimlem3  43393  smfmullem1  43410  smfmullem2  43411  smfmullem3  43412  modexp2m1d  44117  dignn0flhalflem1  45016  itsclc0yqsol  45165  amgmwlem  45317  amgmw2d  45319  young2d  45320
  Copyright terms: Public domain W3C validator