Theorem rpred 9975

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 9943	. 2 |- RR+ C_ RR
2		rpred.1	. 2 |- ( ph -> A e. RR+ )
3	1, 2	sselid 3226	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8074   RR+crp 9932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rab 2520  df-in 3207  df-ss 3214  df-rp 9933

This theorem is referenced by:  rpxrd  9976  rpcnd  9977  rpregt0d  9982  rprege0d  9983  rprene0d  9984  rprecred  9987  ltmulgt11d  10011  ltmulgt12d  10012  gt0divd  10013  ge0divd  10014  lediv12ad  10035  ltexp2a  10899  leexp2a  10900  expnlbnd2  10973  cvg1nlemcxze  11605  cvg1nlemcau  11607  cvg1nlemres  11608  cvg1n  11609  resqrexlemp1rp  11629  resqrexlemfp1  11632  resqrexlemover  11633  resqrexlemdec  11634  resqrexlemdecn  11635  resqrexlemlo  11636  resqrexlemcalc1  11637  resqrexlemcalc2  11638  resqrexlemcalc3  11639  resqrexlemnmsq  11640  resqrexlemnm  11641  resqrexlemcvg  11642  resqrexlemgt0  11643  resqrexlemoverl  11644  resqrexlemglsq  11645  resqrexlemga  11646  cau3lem  11737  bdtrilem  11862  bdtri  11863  addcn2  11933  mulcn2  11935  reccn2ap  11936  climrecvg1n  11971  climcvg1nlem  11972  isumrpcl  12118  expcnvap0  12126  absgtap  12134  cvgratnnlemsumlt  12152  cvgratnnlemfm  12153  cvgratnnlemrate  12154  mertenslemi1  12159  effsumlt  12316  eirraplem  12401  bitsmod  12580  4sqlem7  13020  ssblex  15225  metss2lem  15291  addcncntoplem  15355  mulcncflem  15401  ivthinclemlopn  15430  ivthinclemuopn  15432  limcimolemlt  15458  limcimo  15459  cnplimclemle  15462  limccnp2lem  15470  dveflem  15520  efltlemlt  15568  pilem3  15577  cxplt  15710  cxple  15711  rpcxple2  15712  rpcxplt2  15713  rpcxpsqrt  15716  rpabscxpbnd  15734  logbgt0b  15760  logbgcd1irr  15761  logbgcd1irraplemexp  15762  qdencn  16738  cvgcmp2nlemabs  16747  iooref1o  16749  trilpolemclim  16751  trilpolemisumle  16753  trilpolemeq1  16755  nconstwlpolemgt0  16780  taupi  16789