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

Theorem rpred 11281
Description: A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1  |-  ( ph  ->  A  e.  RR+ )
Assertion
Ref Expression
rpred  |-  ( ph  ->  A  e.  RR )

Proof of Theorem rpred
StepHypRef Expression
1 rpssre 11255 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3497 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1819   RRcr 9508   RR+crp 11245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-in 3478  df-ss 3485  df-rp 11246
This theorem is referenced by:  rpxrd  11282  rpcnd  11283  rpregt0d  11287  rprege0d  11288  rprene0d  11289  rprecred  11292  ltmulgt11d  11312  ltmulgt12d  11313  gt0divd  11314  ge0divd  11315  lediv12ad  11336  xlemul1  11507  xov1plusxeqvd  11691  ltexp2a  12219  expcan  12220  ltexp2  12221  leexp2a  12223  expnlbnd2  12299  expmulnbnd  12300  sqrlem6  13092  cau3lem  13198  rlimcld2  13412  addcn2  13427  mulcn2  13429  reccn2  13430  o1rlimmul  13452  rlimno1  13487  caucvgrlem  13506  isumrpcl  13666  isumltss  13671  expcnv  13686  mertenslem1  13704  effsumlt  13857  recoshcl  13904  eirrlem  13948  rpnnen2lem11  13969  bitsmod  14097  prmreclem3  14447  prmreclem5  14449  4sqlem7  14473  ssblex  21056  metss2lem  21139  methaus  21148  met1stc  21149  met2ndci  21150  metusttoOLD  21185  metustto  21186  metustexhalfOLD  21191  metustexhalf  21192  nlmvscnlem2  21319  nlmvscnlem1  21320  nrginvrcnlem  21324  nmoi2  21362  nghmcn  21377  reperflem  21448  iccntr  21451  icccmplem2  21453  reconnlem2  21457  opnreen  21461  metdcnlem  21466  metnrmlem3  21490  addcnlem  21493  cnheibor  21580  cnllycmp  21581  lebnumlem3  21588  lebnumii  21591  nmoleub2lem  21722  nmoleub2lem3  21723  nmoleub2lem2  21724  nmoleub3  21727  nmhmcn  21728  ipcnlem2  21809  ipcnlem1  21810  lmnn  21827  iscfil3  21837  cfilfcls  21838  iscmet3lem1  21855  iscmet3lem2  21856  bcthlem4  21891  bcthlem5  21892  minveclem3b  21968  minveclem3  21969  ivthlem2  21989  ovolgelb  22016  ovollb2lem  22024  ovolunlem1a  22032  ovolunlem1  22033  ovoliunlem1  22038  ovoliunlem2  22039  ovolscalem1  22049  ioombl1lem2  22094  ioombl1lem4  22096  uniioombllem1  22115  uniioombllem3  22119  uniioombllem4  22120  uniioombllem5  22121  opnmbllem  22135  volcn  22140  vitalilem4  22145  itg2mulclem  22278  itg2monolem3  22284  itg2cnlem2  22294  itg2cn  22295  itggt0  22373  dveflem  22505  dvferm1lem  22510  dvferm2lem  22512  lhop1lem  22539  lhop1  22540  lhop  22542  dvcnvrelem1  22543  dvcnvrelem2  22544  dvcnvre  22545  dvfsumrlim  22557  ftc1a  22563  ftc1lem4  22565  plyeq0lem  22732  aalioulem2  22854  aalioulem4  22856  aalioulem5  22857  aalioulem6  22858  aaliou  22859  aaliou2b  22862  aaliou3lem1  22863  aaliou3lem2  22864  aaliou3lem8  22866  aaliou3lem5  22868  aaliou3lem7  22870  aaliou3lem9  22871  ulmcn  22919  ulmdvlem1  22920  mtest  22924  itgulm  22928  psercn  22946  pserdvlem1  22947  pserdvlem2  22948  pserdv  22949  abelthlem7  22958  pilem2  22972  divlogrlim  23141  logcnlem3  23150  logcnlem4  23151  logccv  23169  divcxp  23193  cxplt  23200  cxple2  23203  cxpcn3lem  23246  cxpaddlelem  23250  cxpaddle  23251  loglesqrt  23257  leibpi  23398  rlimcnp3  23422  cxplim  23426  rlimcxp  23428  cxp2limlem  23430  cxp2lim  23431  cxploglim  23432  cxploglim2  23433  divsqrtsumlem  23434  jensenlem2  23442  logdifbnd  23448  emcllem4  23453  harmonicbnd4  23465  fsumharmonic  23466  ftalem1  23471  ftalem2  23472  ftalem3  23473  ftalem5  23475  basellem1  23479  basellem3  23481  basellem4  23482  basellem8  23486  chtwordi  23555  chpchtsum  23619  logfacrlim  23624  logexprlim  23625  bclbnd  23680  efexple  23681  bposlem1  23684  bposlem2  23685  bposlem6  23689  bposlem7  23690  chebbnd1lem3  23781  chebbnd1  23782  chtppilimlem1  23783  chtppilimlem2  23784  chpo1ubb  23791  rplogsumlem1  23794  rplogsumlem2  23795  dchrisum0lem1a  23796  rpvmasumlem  23797  dchrisumlem2  23800  dchrisumlem3  23801  dchrmusumlema  23803  dchrmusum2  23804  dchrvmasumlem1  23805  dchrvmasum2lem  23806  dchrvmasumlema  23810  dchrvmasumiflem1  23811  dchrisum0fno1  23821  dchrisum0lem1b  23825  dchrisum0lem1  23826  dchrisum0lem2  23828  dchrisum0lem3  23829  dchrisum0  23830  mulogsumlem  23841  logdivsum  23843  mulog2sumlem2  23845  vmalogdivsum2  23848  2vmadivsumlem  23850  log2sumbnd  23854  selberglem2  23856  selberg  23858  selberg2lem  23860  chpdifbndlem1  23863  chpdifbndlem2  23864  selberg3lem1  23867  selberg4lem1  23870  pntrsumbnd2  23877  pntrlog2bndlem2  23888  pntrlog2bndlem3  23889  pntrlog2bndlem5  23891  pntrlog2bndlem6a  23892  pntrlog2bndlem6  23893  pntrlog2bnd  23894  pntpbnd1a  23895  pntpbnd1  23896  pntpbnd2  23897  pntibndlem1  23899  pntibndlem2  23901  pntibndlem3  23902  pntibnd  23903  pntlemc  23905  pntlema  23906  pntlemb  23907  pntlemg  23908  pntlemh  23909  pntlemn  23910  pntlemq  23911  pntlemr  23912  pntlemj  23913  pntlemi  23914  pntlemf  23915  pntlemk  23916  pntlemo  23917  pntleme  23918  pntlem3  23919  pntlemp  23920  pntleml  23921  ostth2lem1  23928  ostth2lem3  23945  ostth2  23947  ostth3  23948  smcnlem  25733  blocnilem  25845  blocni  25846  ubthlem2  25913  minvecolem3  25918  minvecolem4  25922  minvecolem5  25923  nmcexi  27071  lnconi  27078  rpxdivcld  27782  sqsscirc1  28043  cnre2csqlem  28045  tpr2rico  28047  xrmulc1cn  28065  xrge0iifiso  28070  xrge0iifhom  28072  esumcst  28226  esumdivc  28245  dya2icoseg  28409  omssubaddlem  28431  omssubadd  28432  probmeasb  28544  sgnmulrp2  28657  signsply0  28683  signshf  28720  zetacvg  28732  lgamgulmlem2  28747  lgamgulmlem5  28750  lgamucov  28755  regamcl  28778  relgamcl  28779  heicant  30211  opnmbllem0  30212  mblfinlem3  30215  itg2addnclem3  30230  itg2addnc  30231  itggt0cn  30249  ftc1cnnclem  30250  ftc1anclem6  30257  ftc1anclem7  30258  geomcau  30414  sstotbnd2  30432  isbnd3  30442  equivbnd  30448  prdsbnd2  30453  cntotbnd  30454  heibor1lem  30467  heiborlem6  30474  bfplem1  30480  bfplem2  30481  bfp  30482  rrndstprj2  30489  rrnequiv  30493  irrapxlem4  30923  irrapxlem5  30924  irrapx1  30926  pell1qrgaplem  30971  pell14qrgapw  30974  pellqrexplicit  30975  pellqrex  30977  pellfundge  30980  pellfundgt1  30981  rmspecfund  31007  rmxycomplete  31015  rpexpmord  31046  rmxypos  31047  binomcxplemnotnn0  31423  fmul01lt1lem1  31739  fmul01lt1lem2  31740  ltmod  31805  lptre2pt  31807  addlimc  31815  0ellimcdiv  31816  limclner  31818  dvdivbd  31881  ioodvbdlimc1lem2  31890  ioodvbdlimc2lem  31892  itgiccshift  31940  itgperiod  31941  stoweidlem1  31944  stoweidlem3  31946  stoweidlem5  31948  stoweidlem7  31950  stoweidlem11  31954  stoweidlem13  31956  stoweidlem14  31957  stoweidlem24  31967  stoweidlem25  31968  stoweidlem26  31969  stoweidlem34  31977  stoweidlem41  31984  stoweidlem42  31985  stoweidlem49  31992  stoweidlem51  31994  stoweidlem52  31995  stoweidlem59  32002  stoweidlem60  32003  stoweidlem62  32005  stoweid  32006  wallispilem5  32012  stirlinglem1  32017  stirlinglem4  32020  stirlinglem5  32021  stirlinglem6  32022  dirkercncflem1  32046  fourierdlem30  32080  fourierdlem39  32089  fourierdlem47  32097  fourierdlem73  32123  fourierdlem81  32131  fourierdlem87  32137  fourierdlem103  32153  fourierdlem104  32154  fourierdlem107  32157
  Copyright terms: Public domain W3C validator