Theorem rpred 10108

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   RRcr 8179   RR+crp 10065

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-in 3226  df-ss 3233  df-rp 10066

This theorem is used by:  rpxrd  10109  rpcnd  10110  rpregt0d  10115  rprege0d  10116  rprene0d  10117  rprecred  10120  ltmulgt11d  10144  ltmulgt12d  10145  gt0divd  10146  ge0divd  10147  lediv12ad  10168  ltexp2a  11043  leexp2a  11044  expnlbnd2  11118  cvg1nlemcxze  11764  cvg1nlemcau  11766  cvg1nlemres  11767  cvg1n  11768  resqrexlemp1rp  11788  resqrexlemfp1  11791  resqrexlemover  11792  resqrexlemdec  11793  resqrexlemdecn  11794  resqrexlemlo  11795  resqrexlemcalc1  11796  resqrexlemcalc2  11797  resqrexlemcalc3  11798  resqrexlemnmsq  11799  resqrexlemnm  11800  resqrexlemcvg  11801  resqrexlemgt0  11802  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemga  11805  cau3lem  11897  bdtrilem  12024  bdtri  12025  addcn2  12095  mulcn2  12097  reccn2ap  12098  climrecvg1n  12133  climcvg1nlem  12134  isumrpcl  12280  expcnvap0  12288  absgtap  12296  cvgratnnlemsumlt  12314  cvgratnnlemfm  12315  cvgratnnlemrate  12316  mertenslemi1  12321  effsumlt  12478  eirraplem  12563  bitsmod  12742  4sqlem7  13186  ssblex  15623  metss2lem  15689  addcncntoplem  15753  mulcncflem  15799  ivthinclemlopn  15828  ivthinclemuopn  15830  limcimolemlt  15856  limcimo  15857  cnplimclemle  15860  limccnp2lem  15868  dveflem  15918  efltlemlt  15966  pilem3  15976  cxplt  16113  cxple  16114  rpcxple2  16115  rpcxplt2  16116  rpcxpsqrt  16119  rpabscxpbnd  16137  logbgt0b  16163  logbgcd1irr  16164  logbgcd1irraplemexp  16165  log2tlbndlog2  16181  chtqwordi  16224  bclbnd  16268  prmefexple  16269  bposlem1  16272  bposlem5  16276  bposlem6  16277  bposlem7  16278  qdencn  17238  cvgcmp2nlemabs  17247  iooref1o  17249  trilpolemclim  17252  trilpolemisumle  17254  trilpolemeq1  17256  nconstwlpolemgt0  17281  taupi  17290