Theorem rpred 10047

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

Syntax hints:   -> wi 4   e. wcel 2205   RRcr 8142   RR+crp 10004

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rab 2531  df-in 3220  df-ss 3227  df-rp 10005

This theorem is referenced by:  rpxrd  10048  rpcnd  10049  rpregt0d  10054  rprege0d  10055  rprene0d  10056  rprecred  10059  ltmulgt11d  10083  ltmulgt12d  10084  gt0divd  10085  ge0divd  10086  lediv12ad  10107  ltexp2a  10977  leexp2a  10978  expnlbnd2  11052  cvg1nlemcxze  11692  cvg1nlemcau  11694  cvg1nlemres  11695  cvg1n  11696  resqrexlemp1rp  11716  resqrexlemfp1  11719  resqrexlemover  11720  resqrexlemdec  11721  resqrexlemdecn  11722  resqrexlemlo  11723  resqrexlemcalc1  11724  resqrexlemcalc2  11725  resqrexlemcalc3  11726  resqrexlemnmsq  11727  resqrexlemnm  11728  resqrexlemcvg  11729  resqrexlemgt0  11730  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemga  11733  cau3lem  11824  bdtrilem  11949  bdtri  11950  addcn2  12020  mulcn2  12022  reccn2ap  12023  climrecvg1n  12058  climcvg1nlem  12059  isumrpcl  12205  expcnvap0  12213  absgtap  12221  cvgratnnlemsumlt  12239  cvgratnnlemfm  12240  cvgratnnlemrate  12241  mertenslemi1  12246  effsumlt  12403  eirraplem  12488  bitsmod  12667  4sqlem7  13107  ssblex  15422  metss2lem  15488  addcncntoplem  15552  mulcncflem  15598  ivthinclemlopn  15627  ivthinclemuopn  15629  limcimolemlt  15655  limcimo  15656  cnplimclemle  15659  limccnp2lem  15667  dveflem  15717  efltlemlt  15765  pilem3  15774  cxplt  15907  cxple  15908  rpcxple2  15909  rpcxplt2  15910  rpcxpsqrt  15913  rpabscxpbnd  15931  logbgt0b  15957  logbgcd1irr  15958  logbgcd1irraplemexp  15959  qdencn  16933  cvgcmp2nlemabs  16942  iooref1o  16944  trilpolemclim  16946  trilpolemisumle  16948  trilpolemeq1  16950  nconstwlpolemgt0  16976  taupi  16985