Theorem rpred 10097

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 10065	. 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 8178   RR+crp 10054

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 10055

This theorem is used by:  rpxrd  10098  rpcnd  10099  rpregt0d  10104  rprege0d  10105  rprene0d  10106  rprecred  10109  ltmulgt11d  10133  ltmulgt12d  10134  gt0divd  10135  ge0divd  10136  lediv12ad  10157  ltexp2a  11028  leexp2a  11029  expnlbnd2  11103  cvg1nlemcxze  11748  cvg1nlemcau  11750  cvg1nlemres  11751  cvg1n  11752  resqrexlemp1rp  11772  resqrexlemfp1  11775  resqrexlemover  11776  resqrexlemdec  11777  resqrexlemdecn  11778  resqrexlemlo  11779  resqrexlemcalc1  11780  resqrexlemcalc2  11781  resqrexlemcalc3  11782  resqrexlemnmsq  11783  resqrexlemnm  11784  resqrexlemcvg  11785  resqrexlemgt0  11786  resqrexlemoverl  11787  resqrexlemglsq  11788  resqrexlemga  11789  cau3lem  11880  bdtrilem  12005  bdtri  12006  addcn2  12076  mulcn2  12078  reccn2ap  12079  climrecvg1n  12114  climcvg1nlem  12115  isumrpcl  12261  expcnvap0  12269  absgtap  12277  cvgratnnlemsumlt  12295  cvgratnnlemfm  12296  cvgratnnlemrate  12297  mertenslemi1  12302  effsumlt  12459  eirraplem  12544  bitsmod  12723  4sqlem7  13163  ssblex  15532  metss2lem  15598  addcncntoplem  15662  mulcncflem  15708  ivthinclemlopn  15737  ivthinclemuopn  15739  limcimolemlt  15765  limcimo  15766  cnplimclemle  15769  limccnp2lem  15777  dveflem  15827  efltlemlt  15875  pilem3  15884  cxplt  16018  cxple  16019  rpcxple2  16020  rpcxplt2  16021  rpcxpsqrt  16024  rpabscxpbnd  16042  logbgt0b  16068  logbgcd1irr  16069  logbgcd1irraplemexp  16070  log2tlbndlog2  16082  qdencn  17072  cvgcmp2nlemabs  17081  iooref1o  17083  trilpolemclim  17085  trilpolemisumle  17087  trilpolemeq1  17089  nconstwlpolemgt0  17114  taupi  17123