Theorem rpred 11872

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

Step	Hyp	Ref	Expression
1		rpssre 11843	. 2 |- RR+ C_ RR
2		rpred.1	. 2 |- ( ph -> A e. RR+ )
3	1, 2	sseldi 3601	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1990   RRcr 9935   RR+crp 11832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-in 3581  df-ss 3588  df-rp 11833

This theorem is referenced by:  rpxrd  11873  rpcnd  11874  rpregt0d  11878  rprege0d  11879  rprene0d  11880  rprecred  11883  ltmulgt11d  11907  ltmulgt12d  11908  gt0divd  11909  ge0divd  11910  lediv12ad  11931  xlemul1  12120  xov1plusxeqvd  12318  ltexp2a  12912  expcan  12913  ltexp2  12914  leexp2a  12916  expnlbnd2  12995  expmulnbnd  12996  sqrlem6  13988  cau3lem  14094  rlimcld2  14309  addcn2  14324  mulcn2  14326  reccn2  14327  o1rlimmul  14349  rlimno1  14384  caucvgrlem  14403  isumrpcl  14575  isumltss  14580  expcnv  14596  mertenslem1  14616  effsumlt  14841  recoshcl  14888  eirrlem  14932  rpnnen2lem11  14953  bitsmod  15158  prmreclem3  15622  prmreclem5  15624  4sqlem7  15648  ssblex  22233  metss2lem  22316  methaus  22325  met1stc  22326  met2ndci  22327  metustto  22358  metustexhalf  22361  nlmvscnlem2  22489  nlmvscnlem1  22490  nrginvrcnlem  22495  nmoi2  22534  nghmcn  22549  reperflem  22621  iccntr  22624  icccmplem2  22626  reconnlem2  22630  opnreen  22634  metdcnlem  22639  metnrmlem3  22664  addcnlem  22667  cnheibor  22754  cnllycmp  22755  lebnumlem3  22762  lebnumii  22765  nmoleub2lem  22914  nmoleub2lem3  22915  nmoleub2lem2  22916  nmoleub3  22919  nmhmcn  22920  ipcnlem2  23043  ipcnlem1  23044  lmnn  23061  iscfil3  23071  cfilfcls  23072  iscmet3lem1  23089  iscmet3lem2  23090  bcthlem4  23124  bcthlem5  23125  minveclem3b  23199  minveclem3  23200  ivthlem2  23221  ovolgelb  23248  ovollb2lem  23256  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliunlem2  23271  ovolscalem1  23281  ioombl1lem2  23327  ioombl1lem4  23329  uniioombllem1  23349  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  opnmbllem  23369  volcn  23374  vitalilem4  23380  itg2mulclem  23513  itg2monolem3  23519  itg2cnlem2  23529  itg2cn  23530  itggt0  23608  dveflem  23742  dvferm1lem  23747  dvferm2lem  23749  lhop1lem  23776  lhop1  23777  lhop  23779  dvcnvrelem1  23780  dvcnvrelem2  23781  dvcnvre  23782  dvfsumrlim  23794  ftc1a  23800  ftc1lem4  23802  plyeq0lem  23966  aalioulem2  24088  aalioulem4  24090  aalioulem5  24091  aalioulem6  24092  aaliou  24093  aaliou2b  24096  aaliou3lem1  24097  aaliou3lem2  24098  aaliou3lem8  24100  aaliou3lem5  24102  aaliou3lem7  24104  aaliou3lem9  24105  ulmcn  24153  ulmdvlem1  24154  mtest  24158  itgulm  24162  psercn  24180  pserdvlem1  24181  pserdvlem2  24182  pserdv  24183  abelthlem7  24192  pilem2  24206  divlogrlim  24381  logcnlem3  24390  logcnlem4  24391  logccv  24409  divcxp  24433  cxplt  24440  cxple2  24443  cxpcn3lem  24488  cxpaddlelem  24492  cxpaddle  24493  loglesqrt  24499  leibpi  24669  rlimcnp3  24694  cxplim  24698  rlimcxp  24700  cxp2limlem  24702  cxp2lim  24703  cxploglim  24704  cxploglim2  24705  divsqrtsumlem  24706  jensenlem2  24714  logdifbnd  24720  emcllem4  24725  harmonicbnd4  24737  fsumharmonic  24738  zetacvg  24741  lgamgulmlem2  24756  lgamgulmlem5  24759  lgamucov  24764  regamcl  24787  relgamcl  24788  ftalem1  24799  ftalem2  24800  ftalem3  24801  ftalem5  24803  basellem1  24807  basellem3  24809  basellem4  24810  basellem8  24814  chtwordi  24882  chpchtsum  24944  logfacrlim  24949  logexprlim  24950  bclbnd  25005  efexple  25006  bposlem1  25009  bposlem2  25010  bposlem6  25014  bposlem7  25015  chebbnd1lem3  25160  chebbnd1  25161  chtppilimlem1  25162  chtppilimlem2  25163  chpo1ubb  25170  rplogsumlem1  25173  rplogsumlem2  25174  dchrisum0lem1a  25175  rpvmasumlem  25176  dchrisumlem2  25179  dchrisumlem3  25180  dchrmusumlema  25182  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasum2lem  25185  dchrvmasumlema  25189  dchrvmasumiflem1  25190  dchrisum0fno1  25200  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2  25207  dchrisum0lem3  25208  dchrisum0  25209  mulogsumlem  25220  logdivsum  25222  mulog2sumlem2  25224  vmalogdivsum2  25227  2vmadivsumlem  25229  log2sumbnd  25233  selberglem2  25235  selberg  25237  selberg2lem  25239  chpdifbndlem1  25242  chpdifbndlem2  25243  selberg3lem1  25246  selberg4lem1  25249  pntrsumbnd2  25256  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem5  25270  pntrlog2bndlem6a  25271  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntibndlem1  25278  pntibndlem2  25280  pntibndlem3  25281  pntibnd  25282  pntlemc  25284  pntlema  25285  pntlemb  25286  pntlemg  25287  pntlemh  25288  pntlemn  25289  pntlemq  25290  pntlemr  25291  pntlemj  25292  pntlemi  25293  pntlemf  25294  pntlemk  25295  pntlemo  25296  pntleme  25297  pntlem3  25298  pntlemp  25299  pntleml  25300  ostth2lem1  25307  ostth2lem3  25324  ostth2  25326  ostth3  25327  crctcshwlkn0lem5  26706  smcnlem  27552  blocnilem  27659  blocni  27660  ubthlem2  27727  minvecolem3  27732  minvecolem4  27736  minvecolem5  27737  nmcexi  28885  lnconi  28892  fsumub  29574  rpxdivcld  29642  sqsscirc1  29954  cnre2csqlem  29956  tpr2rico  29958  xrmulc1cn  29976  xrge0iifiso  29981  xrge0iifhom  29983  esumcst  30125  esumdivc  30145  dya2icoseg  30339  omssubaddlem  30361  omssubadd  30362  probmeasb  30492  sgnmulrp2  30605  signsply0  30628  signshf  30665  logdivsqrle  30728  hgt750leme  30736  dnicn  32482  unblimceq0lem  32497  unbdqndv2lem1  32500  unbdqndv2lem2  32501  knoppndvlem18  32520  knoppndvlem21  32523  poimirlem29  33438  heicant  33444  opnmbllem0  33445  mblfinlem3  33448  itg2addnclem3  33463  itg2addnc  33464  itggt0cn  33482  ftc1cnnclem  33483  ftc1anclem6  33490  ftc1anclem7  33491  geomcau  33555  sstotbnd2  33573  isbnd3  33583  equivbnd  33589  prdsbnd2  33594  cntotbnd  33595  heibor1lem  33608  heiborlem6  33615  bfplem1  33621  bfplem2  33622  bfp  33623  rrndstprj2  33630  rrnequiv  33634  irrapxlem4  37389  irrapxlem5  37390  irrapx1  37392  pell1qrgaplem  37437  pell14qrgapw  37440  pellqrexplicit  37441  pellqrex  37443  pellfundge  37446  pellfundgt1  37447  rmspecfund  37474  rmxycomplete  37482  rpexpmord  37513  rmxypos  37514  binomcxplemnotnn0  38555  suprltrp  39544  supxrge  39554  infrpge  39567  infleinflem1  39586  xralrple4  39589  recnnltrp  39593  rpgtrecnn  39597  fmul01lt1lem1  39816  fmul01lt1lem2  39817  ltmod  39870  lptre2pt  39872  addlimc  39880  0ellimcdiv  39881  limclner  39883  climleltrp  39908  climisp  39978  climxrrelem  39981  climxrre  39982  limsupgtlem  40009  liminfltlem  40036  cnrefiisplem  40055  climxlim2lem  40071  dvdivbd  40138  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  itgiccshift  40196  itgperiod  40197  stoweidlem1  40218  stoweidlem3  40220  stoweidlem5  40222  stoweidlem7  40224  stoweidlem11  40228  stoweidlem13  40230  stoweidlem14  40231  stoweidlem24  40241  stoweidlem25  40242  stoweidlem26  40243  stoweidlem34  40251  stoweidlem41  40258  stoweidlem42  40259  stoweidlem49  40266  stoweidlem51  40268  stoweidlem52  40269  stoweidlem59  40276  stoweidlem60  40277  stoweidlem62  40279  stoweid  40280  wallispilem5  40286  stirlinglem1  40291  stirlinglem4  40294  stirlinglem5  40295  stirlinglem6  40296  dirkercncflem1  40320  fourierdlem30  40354  fourierdlem39  40363  fourierdlem47  40370  fourierdlem73  40396  fourierdlem81  40404  fourierdlem87  40410  fourierdlem103  40426  fourierdlem104  40427  fourierdlem107  40430  rrndistlt  40510  qndenserrnbllem  40514  sge0ltfirp  40617  sge0rpcpnf  40638  sge0xaddlem1  40650  omeiunltfirp  40733  carageniuncllem2  40736  ovnsubaddlem1  40784  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  hoiqssbllem1  40836  hoiqssbllem2  40837  hoiqssbllem3  40838  hspmbllem2  40841  hspmbllem3  40842  ovolval5lem1  40866  ovolval5lem2  40867  iinhoiicc  40888  vonioolem1  40894  pimrecltpos  40919  smflimlem3  40981  smfmullem1  40998  smfmullem2  40999  smfmullem3  41000  modexp2m1d  41529  dignn0flhalflem1  42409  amgmwlem  42548  amgmw2d  42550  young2d  42551