Theorem rpred 9692

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

Syntax hints:   -> wi 4   e. wcel 2148   RRcr 7807   RR+crp 9649

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-in 3135  df-ss 3142  df-rp 9650

This theorem is referenced by:  rpxrd  9693  rpcnd  9694  rpregt0d  9699  rprege0d  9700  rprene0d  9701  rprecred  9704  ltmulgt11d  9728  ltmulgt12d  9729  gt0divd  9730  ge0divd  9731  lediv12ad  9752  ltexp2a  10567  leexp2a  10568  expnlbnd2  10640  cvg1nlemcxze  10984  cvg1nlemcau  10986  cvg1nlemres  10987  cvg1n  10988  resqrexlemp1rp  11008  resqrexlemfp1  11011  resqrexlemover  11012  resqrexlemdec  11013  resqrexlemdecn  11014  resqrexlemlo  11015  resqrexlemcalc1  11016  resqrexlemcalc2  11017  resqrexlemcalc3  11018  resqrexlemnmsq  11019  resqrexlemnm  11020  resqrexlemcvg  11021  resqrexlemgt0  11022  resqrexlemoverl  11023  resqrexlemglsq  11024  resqrexlemga  11025  cau3lem  11116  bdtrilem  11240  bdtri  11241  addcn2  11311  mulcn2  11313  reccn2ap  11314  climrecvg1n  11349  climcvg1nlem  11350  isumrpcl  11495  expcnvap0  11503  absgtap  11511  cvgratnnlemsumlt  11529  cvgratnnlemfm  11530  cvgratnnlemrate  11531  mertenslemi1  11536  effsumlt  11693  eirraplem  11777  4sqlem7  12374  ssblex  13802  metss2lem  13868  addcncntoplem  13922  mulcncflem  13961  ivthinclemlopn  13985  ivthinclemuopn  13987  limcimolemlt  14004  limcimo  14005  cnplimclemle  14008  limccnp2lem  14016  dveflem  14058  efltlemlt  14066  pilem3  14075  cxplt  14207  cxple  14208  rpcxple2  14209  rpcxplt2  14210  rpcxpsqrt  14213  rpabscxpbnd  14230  logbgt0b  14255  logbgcd1irr  14256  logbgcd1irraplemexp  14257  qdencn  14635  cvgcmp2nlemabs  14640  iooref1o  14642  trilpolemclim  14644  trilpolemisumle  14646  trilpolemeq1  14648  nconstwlpolemgt0  14671  taupi  14680