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

Theorem rpred 10640
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 10614 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3338 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   RRcr 8981   RR+crp 10604
This theorem is referenced by:  rpxrd  10641  rpcnd  10642  rpregt0d  10646  rprege0d  10647  rprene0d  10648  rprecred  10651  ltmulgt11d  10671  ltmulgt12d  10672  gt0divd  10673  ge0divd  10674  lediv12ad  10695  xlemul1  10861  xov1plusxeqvd  11033  ltexp2a  11423  expcan  11424  ltexp2  11425  leexp2a  11427  expnlbnd2  11502  expmulnbnd  11503  sqrlem6  12045  cau3lem  12150  rlimcld2  12364  addcn2  12379  mulcn2  12381  reccn2  12382  o1rlimmul  12404  rlimno1  12439  caucvgrlem  12458  isumrpcl  12615  isumltss  12620  expcnv  12635  mertenslem1  12653  effsumlt  12704  recoshcl  12751  eirrlem  12795  rpnnen2lem11  12816  bitsmod  12940  prmreclem3  13278  prmreclem5  13280  4sqlem7  13304  ssblex  18450  metss2lem  18533  methaus  18542  met1stc  18543  met2ndci  18544  metusttoOLD  18579  metustto  18580  metustexhalfOLD  18585  metustexhalf  18586  nlmvscnlem2  18713  nlmvscnlem1  18714  nrginvrcnlem  18718  nmoi2  18756  nghmcn  18771  reperflem  18841  iccntr  18844  icccmplem2  18846  reconnlem2  18850  opnreen  18854  metdcnlem  18859  metnrmlem3  18883  addcnlem  18886  cnheibor  18972  cnllycmp  18973  lebnumlem3  18980  lebnumii  18983  nmoleub2lem  19114  nmoleub2lem3  19115  nmoleub2lem2  19116  nmoleub3  19119  nmhmcn  19120  ipcnlem2  19190  ipcnlem1  19191  lmnn  19208  iscfil3  19218  cfilfcls  19219  iscmet3lem1  19236  iscmet3lem2  19237  bcthlem4  19272  bcthlem5  19273  minveclem3b  19321  minveclem3  19322  ivthlem2  19341  ovolgelb  19368  ovollb2lem  19376  ovolunlem1a  19384  ovolunlem1  19385  ovoliunlem1  19390  ovoliunlem2  19391  ovolscalem1  19401  ioombl1lem2  19445  ioombl1lem4  19447  uniioombllem1  19465  uniioombllem3  19469  uniioombllem4  19470  uniioombllem5  19471  opnmbllem  19485  volcn  19490  vitalilem4  19495  itg2mulclem  19630  itg2monolem3  19636  itg2cnlem2  19646  itg2cn  19647  itggt0  19725  dveflem  19855  dvferm1lem  19860  dvferm2lem  19862  lhop1lem  19889  lhop1  19890  lhop  19892  dvcnvrelem1  19893  dvcnvrelem2  19894  dvcnvre  19895  dvfsumrlim  19907  ftc1a  19913  ftc1lem4  19915  plyeq0lem  20121  aalioulem2  20242  aalioulem4  20244  aalioulem5  20245  aalioulem6  20246  aaliou  20247  aaliou2b  20250  aaliou3lem1  20251  aaliou3lem2  20252  aaliou3lem8  20254  aaliou3lem5  20256  aaliou3lem7  20258  aaliou3lem9  20259  ulmcn  20307  ulmdvlem1  20308  mtest  20312  itgulm  20316  psercn  20334  pserdvlem1  20335  pserdvlem2  20336  pserdv  20337  abelthlem7  20346  pilem2  20360  divlogrlim  20518  logcnlem3  20527  logcnlem4  20528  logccv  20546  divcxp  20570  cxplt  20577  cxple2  20580  cxpcn3lem  20623  cxpaddlelem  20627  cxpaddle  20628  loglesqr  20634  leibpi  20774  rlimcnp3  20798  cxplim  20802  rlimcxp  20804  cxp2limlem  20806  cxp2lim  20807  cxploglim  20808  cxploglim2  20809  divsqrsumlem  20810  jensenlem2  20818  logdifbnd  20824  emcllem4  20829  harmonicbnd4  20841  fsumharmonic  20842  ftalem1  20847  ftalem2  20848  ftalem3  20849  ftalem5  20851  basellem1  20855  basellem3  20857  basellem4  20858  basellem8  20862  chtwordi  20931  chpchtsum  20995  logfacrlim  21000  logexprlim  21001  bclbnd  21056  efexple  21057  bposlem1  21060  bposlem2  21061  bposlem6  21065  bposlem7  21066  chebbnd1lem3  21157  chebbnd1  21158  chtppilimlem1  21159  chtppilimlem2  21160  chpo1ubb  21167  rplogsumlem1  21170  rplogsumlem2  21171  dchrisum0lem1a  21172  rpvmasumlem  21173  dchrisumlem2  21176  dchrisumlem3  21177  dchrmusumlema  21179  dchrmusum2  21180  dchrvmasumlem1  21181  dchrvmasum2lem  21182  dchrvmasumlema  21186  dchrvmasumiflem1  21187  dchrisum0fno1  21197  dchrisum0lem1b  21201  dchrisum0lem1  21202  dchrisum0lem2  21204  dchrisum0lem3  21205  dchrisum0  21206  mulogsumlem  21217  logdivsum  21219  mulog2sumlem2  21221  vmalogdivsum2  21224  vmalogdivsum  21225  2vmadivsumlem  21226  log2sumbnd  21230  selberglem2  21232  selberg  21234  selberg2lem  21236  chpdifbndlem1  21239  chpdifbndlem2  21240  selberg3lem1  21243  selberg3  21245  selberg4lem1  21246  selberg4  21247  pntrsumbnd2  21253  selberg3r  21255  selberg4r  21256  selberg34r  21257  pntrlog2bndlem1  21263  pntrlog2bndlem2  21264  pntrlog2bndlem3  21265  pntrlog2bndlem5  21267  pntrlog2bndlem6a  21268  pntrlog2bndlem6  21269  pntrlog2bnd  21270  pntpbnd1a  21271  pntpbnd1  21272  pntpbnd2  21273  pntibndlem1  21275  pntibndlem2  21277  pntibndlem3  21278  pntibnd  21279  pntlemc  21281  pntlema  21282  pntlemb  21283  pntlemg  21284  pntlemh  21285  pntlemn  21286  pntlemq  21287  pntlemr  21288  pntlemj  21289  pntlemi  21290  pntlemf  21291  pntlemk  21292  pntlemo  21293  pntleme  21294  pntlem3  21295  pntlemp  21296  pntleml  21297  ostth2lem1  21304  ostth2lem3  21321  ostth2  21323  ostth3  21324  smcnlem  22185  blocnilem  22297  blocni  22298  ubthlem2  22365  minvecolem3  22370  minvecolem4  22374  minvecolem5  22375  nmcexi  23521  lnconi  23528  rpxdivcld  24172  sqsscirc1  24298  cnre2csqlem  24300  tpr2rico  24302  xrmulc1cn  24308  xrge0iifiso  24313  xrge0iifhom  24315  esumcst  24447  esumdivc  24465  dya2icoseg  24619  probmeasb  24680  zetacvg  24791  lgamgulmlem2  24806  lgamgulmlem5  24809  lgamucov  24814  regamcl  24837  relgamcl  24838  mblfinlem  26234  mblfinlem2  26235  itg2addnclem3  26248  itg2addnc  26249  itggt0cn  26267  ftc1cnnclem  26268  ftc1anclem6  26275  ftc1anclem7  26276  geomcau  26456  sstotbnd2  26474  isbnd3  26484  equivbnd  26490  prdsbnd2  26495  cntotbnd  26496  heibor1lem  26509  heiborlem6  26516  bfplem1  26522  bfplem2  26523  bfp  26524  rrndstprj2  26531  rrnequiv  26535  irrapxlem4  26879  irrapxlem5  26880  irrapx1  26882  pell1qrgaplem  26927  pell14qrgapw  26930  pellqrexplicit  26931  pellqrex  26933  pellfundge  26936  pellfundgt1  26937  rmspecfund  26963  rmxycomplete  26971  rpexpmord  27002  rmxypos  27003  fmul01lt1lem1  27681  fmul01lt1lem2  27682  stoweidlem1  27717  stoweidlem3  27719  stoweidlem5  27721  stoweidlem7  27723  stoweidlem11  27727  stoweidlem13  27729  stoweidlem14  27730  stoweidlem24  27740  stoweidlem25  27741  stoweidlem26  27742  stoweidlem34  27750  stoweidlem41  27757  stoweidlem42  27758  stoweidlem49  27765  stoweidlem51  27767  stoweidlem52  27768  stoweidlem59  27775  stoweidlem60  27776  stoweidlem62  27778  stoweid  27779  wallispilem5  27785  stirlinglem1  27790  stirlinglem4  27793  stirlinglem5  27794  stirlinglem6  27795
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-in 3319  df-ss 3326  df-rp 10605
  Copyright terms: Public domain W3C validator