Theorem rpred 11285

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

Step	Hyp	Ref	Expression
1		rpssre 11259	. 2
2		rpred.1	. 2
3	1, 2	sseldi 3501	1

Syntax hints:  ->wi 4  e.wcel 1818  cr 9512  crp 11249

This theorem is referenced by:  rpxrd  11286  rpcnd  11287  rpregt0d  11291  rprege0d  11292  rprene0d  11293  rprecred  11296  ltmulgt11d  11316  ltmulgt12d  11317  gt0divd  11318  ge0divd  11319  lediv12ad  11340  xlemul1  11511  xov1plusxeqvd  11695  ltexp2a  12217  expcan  12218  ltexp2  12219  leexp2a  12221  expnlbnd2  12297  expmulnbnd  12298  sqrlem6  13081  cau3lem  13187  rlimcld2  13401  addcn2  13416  mulcn2  13418  reccn2  13419  o1rlimmul  13441  rlimno1  13476  caucvgrlem  13495  isumrpcl  13655  isumltss  13660  expcnv  13675  mertenslem1  13693  effsumlt  13846  recoshcl  13893  eirrlem  13937  rpnnen2lem11  13958  bitsmod  14086  prmreclem3  14436  prmreclem5  14438  4sqlem7  14462  ssblex  20931  metss2lem  21014  methaus  21023  met1stc  21024  met2ndci  21025  metusttoOLD  21060  metustto  21061  metustexhalfOLD  21066  metustexhalf  21067  nlmvscnlem2  21194  nlmvscnlem1  21195  nrginvrcnlem  21199  nmoi2  21237  nghmcn  21252  reperflem  21323  iccntr  21326  icccmplem2  21328  reconnlem2  21332  opnreen  21336  metdcnlem  21341  metnrmlem3  21365  addcnlem  21368  cnheibor  21455  cnllycmp  21456  lebnumlem3  21463  lebnumii  21466  nmoleub2lem  21597  nmoleub2lem3  21598  nmoleub2lem2  21599  nmoleub3  21602  nmhmcn  21603  ipcnlem2  21684  ipcnlem1  21685  lmnn  21702  iscfil3  21712  cfilfcls  21713  iscmet3lem1  21730  iscmet3lem2  21731  bcthlem4  21766  bcthlem5  21767  minveclem3b  21843  minveclem3  21844  ivthlem2  21864  ovolgelb  21891  ovollb2lem  21899  ovolunlem1a  21907  ovolunlem1  21908  ovoliunlem1  21913  ovoliunlem2  21914  ovolscalem1  21924  ioombl1lem2  21969  ioombl1lem4  21971  uniioombllem1  21990  uniioombllem3  21994  uniioombllem4  21995  uniioombllem5  21996  opnmbllem  22010  volcn  22015  vitalilem4  22020  itg2mulclem  22153  itg2monolem3  22159  itg2cnlem2  22169  itg2cn  22170  itggt0  22248  dveflem  22380  dvferm1lem  22385  dvferm2lem  22387  lhop1lem  22414  lhop1  22415  lhop  22417  dvcnvrelem1  22418  dvcnvrelem2  22419  dvcnvre  22420  dvfsumrlim  22432  ftc1a  22438  ftc1lem4  22440  plyeq0lem  22607  aalioulem2  22729  aalioulem4  22731  aalioulem5  22732  aalioulem6  22733  aaliou  22734  aaliou2b  22737  aaliou3lem1  22738  aaliou3lem2  22739  aaliou3lem8  22741  aaliou3lem5  22743  aaliou3lem7  22745  aaliou3lem9  22746  ulmcn  22794  ulmdvlem1  22795  mtest  22799  itgulm  22803  psercn  22821  pserdvlem1  22822  pserdvlem2  22823  pserdv  22824  abelthlem7  22833  pilem2  22847  divlogrlim  23016  logcnlem3  23025  logcnlem4  23026  logccv  23044  divcxp  23068  cxplt  23075  cxple2  23078  cxpcn3lem  23121  cxpaddlelem  23125  cxpaddle  23126  loglesqrt  23132  leibpi  23273  rlimcnp3  23297  cxplim  23301  rlimcxp  23303  cxp2limlem  23305  cxp2lim  23306  cxploglim  23307  cxploglim2  23308  divsqrtsumlem  23309  jensenlem2  23317  logdifbnd  23323  emcllem4  23328  harmonicbnd4  23340  fsumharmonic  23341  ftalem1  23346  ftalem2  23347  ftalem3  23348  ftalem5  23350  basellem1  23354  basellem3  23356  basellem4  23357  basellem8  23361  chtwordi  23430  chpchtsum  23494  logfacrlim  23499  logexprlim  23500  bclbnd  23555  efexple  23556  bposlem1  23559  bposlem2  23560  bposlem6  23564  bposlem7  23565  chebbnd1lem3  23656  chebbnd1  23657  chtppilimlem1  23658  chtppilimlem2  23659  chpo1ubb  23666  rplogsumlem1  23669  rplogsumlem2  23670  dchrisum0lem1a  23671  rpvmasumlem  23672  dchrisumlem2  23675  dchrisumlem3  23676  dchrmusumlema  23678  dchrmusum2  23679  dchrvmasumlem1  23680  dchrvmasum2lem  23681  dchrvmasumlema  23685  dchrvmasumiflem1  23686  dchrisum0fno1  23696  dchrisum0lem1b  23700  dchrisum0lem1  23701  dchrisum0lem2  23703  dchrisum0lem3  23704  dchrisum0  23705  mulogsumlem  23716  logdivsum  23718  mulog2sumlem2  23720  vmalogdivsum2  23723  2vmadivsumlem  23725  log2sumbnd  23729  selberglem2  23731  selberg  23733  selberg2lem  23735  chpdifbndlem1  23738  chpdifbndlem2  23739  selberg3lem1  23742  selberg4lem1  23745  pntrsumbnd2  23752  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem5  23766  pntrlog2bndlem6a  23767  pntrlog2bndlem6  23768  pntrlog2bnd  23769  pntpbnd1a  23770  pntpbnd1  23771  pntpbnd2  23772  pntibndlem1  23774  pntibndlem2  23776  pntibndlem3  23777  pntibnd  23778  pntlemc  23780  pntlema  23781  pntlemb  23782  pntlemg  23783  pntlemh  23784  pntlemn  23785  pntlemq  23786  pntlemr  23787  pntlemj  23788  pntlemi  23789  pntlemf  23790  pntlemk  23791  pntlemo  23792  pntleme  23793  pntlem3  23794  pntlemp  23795  pntleml  23796  ostth2lem1  23803  ostth2lem3  23820  ostth2  23822  ostth3  23823  smcnlem  25607  blocnilem  25719  blocni  25720  ubthlem2  25787  minvecolem3  25792  minvecolem4  25796  minvecolem5  25797  nmcexi  26945  lnconi  26952  rpxdivcld  27630  sqsscirc1  27890  cnre2csqlem  27892  tpr2rico  27894  xrmulc1cn  27912  xrge0iifiso  27917  xrge0iifhom  27919  esumcst  28071  esumdivc  28089  dya2icoseg  28248  probmeasb  28369  sgnmulrp2  28482  signsply0  28508  signshf  28545  zetacvg  28557  lgamgulmlem2  28572  lgamgulmlem5  28575  lgamucov  28580  regamcl  28603  relgamcl  28604  heicant  30049  opnmbllem0  30050  mblfinlem3  30053  itg2addnclem3  30068  itg2addnc  30069  itggt0cn  30087  ftc1cnnclem  30088  ftc1anclem6  30095  ftc1anclem7  30096  geomcau  30252  sstotbnd2  30270  isbnd3  30280  equivbnd  30286  prdsbnd2  30291  cntotbnd  30292  heibor1lem  30305  heiborlem6  30312  bfplem1  30318  bfplem2  30319  bfp  30320  rrndstprj2  30327  rrnequiv  30331  irrapxlem4  30761  irrapxlem5  30762  irrapx1  30764  pell1qrgaplem  30809  pell14qrgapw  30812  pellqrexplicit  30813  pellqrex  30815  pellfundge  30818  pellfundgt1  30819  rmspecfund  30845  rmxycomplete  30853  rpexpmord  30884  rmxypos  30885  binomcxplemnotnn0  31261  fmul01lt1lem1  31578  fmul01lt1lem2  31579  ltmod  31644  lptre2pt  31646  addlimc  31654  0ellimcdiv  31655  limclner  31657  dvdivbd  31720  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  itgiccshift  31779  itgperiod  31780  stoweidlem1  31783  stoweidlem3  31785  stoweidlem5  31787  stoweidlem7  31789  stoweidlem11  31793  stoweidlem13  31795  stoweidlem14  31796  stoweidlem24  31806  stoweidlem25  31807  stoweidlem26  31808  stoweidlem34  31816  stoweidlem41  31823  stoweidlem42  31824  stoweidlem49  31831  stoweidlem51  31833  stoweidlem52  31834  stoweidlem59  31841  stoweidlem60  31842  stoweidlem62  31844  stoweid  31845  wallispilem5  31851  stirlinglem1  31856  stirlinglem4  31859  stirlinglem5  31860  stirlinglem6  31861  dirkercncflem1  31885  fourierdlem30  31919  fourierdlem39  31928  fourierdlem47  31936  fourierdlem73  31962  fourierdlem81  31970  fourierdlem87  31976  fourierdlem103  31992  fourierdlem104  31993  fourierdlem107  31996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-in 3482  df-ss 3489  df-rp 11250