Theorem rpred 10114

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 10082	. 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 8184   RR+crp 10071

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 10072

This theorem is used by:  rpxrd  10115  rpcnd  10116  rpregt0d  10121  rprege0d  10122  rprene0d  10123  rprecred  10126  ltmulgt11d  10150  ltmulgt12d  10151  gt0divd  10152  ge0divd  10153  lediv12ad  10174  ltexp2a  11049  leexp2a  11050  expnlbnd2  11124  cvg1nlemcxze  11770  cvg1nlemcau  11772  cvg1nlemres  11773  cvg1n  11774  resqrexlemp1rp  11794  resqrexlemfp1  11797  resqrexlemover  11798  resqrexlemdec  11799  resqrexlemdecn  11800  resqrexlemlo  11801  resqrexlemcalc1  11802  resqrexlemcalc2  11803  resqrexlemcalc3  11804  resqrexlemnmsq  11805  resqrexlemnm  11806  resqrexlemcvg  11807  resqrexlemgt0  11808  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemga  11811  cau3lem  11903  bdtrilem  12030  bdtri  12031  addcn2  12101  mulcn2  12103  reccn2ap  12104  climrecvg1n  12139  climcvg1nlem  12140  isumrpcl  12286  expcnvap0  12294  absgtap  12302  cvgratnnlemsumlt  12320  cvgratnnlemfm  12321  cvgratnnlemrate  12322  mertenslemi1  12327  effsumlt  12484  eirraplem  12569  bitsmod  12748  4sqlem7  13192  ssblex  15657  metss2lem  15723  addcncntoplem  15787  mulcncflem  15833  ivthinclemlopn  15862  ivthinclemuopn  15864  limcimolemlt  15890  limcimo  15891  cnplimclemle  15894  limccnp2lem  15902  dveflem  15952  efltlemlt  16000  pilem3  16010  cxplt  16151  cxple  16152  rpcxple2  16153  rpcxplt2  16154  rpcxpsqrt  16157  rpabscxpbnd  16175  logbgt0b  16202  logbgcd1irr  16203  logbgcd1irraplemexp  16204  log2tlbndlog2  16220  chtqwordi  16263  bclbnd  16307  prmefexple  16308  bposlem1  16311  bposlem5  16315  bposlem6  16316  bposlem7  16317  qdencn  17278  cvgcmp2nlemabs  17287  iooref1o  17289  trilpolemclim  17292  trilpolemisumle  17294  trilpolemeq1  17296  nconstwlpolemgt0  17321  taupi  17330