Theorem rpred 10113

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 10081	. 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 10070

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 10071

This theorem is used by:  rpxrd  10114  rpcnd  10115  rpregt0d  10120  rprege0d  10121  rprene0d  10122  rprecred  10125  ltmulgt11d  10149  ltmulgt12d  10150  gt0divd  10151  ge0divd  10152  lediv12ad  10173  ltexp2a  11048  leexp2a  11049  expnlbnd2  11123  cvg1nlemcxze  11769  cvg1nlemcau  11771  cvg1nlemres  11772  cvg1n  11773  resqrexlemp1rp  11793  resqrexlemfp1  11796  resqrexlemover  11797  resqrexlemdec  11798  resqrexlemdecn  11799  resqrexlemlo  11800  resqrexlemcalc1  11801  resqrexlemcalc2  11802  resqrexlemcalc3  11803  resqrexlemnmsq  11804  resqrexlemnm  11805  resqrexlemcvg  11806  resqrexlemgt0  11807  resqrexlemoverl  11808  resqrexlemglsq  11809  resqrexlemga  11810  cau3lem  11902  bdtrilem  12029  bdtri  12030  addcn2  12100  mulcn2  12102  reccn2ap  12103  climrecvg1n  12138  climcvg1nlem  12139  isumrpcl  12285  expcnvap0  12293  absgtap  12301  cvgratnnlemsumlt  12319  cvgratnnlemfm  12320  cvgratnnlemrate  12321  mertenslemi1  12326  effsumlt  12483  eirraplem  12568  bitsmod  12747  4sqlem7  13191  ssblex  15674  metss2lem  15740  addcncntoplem  15804  mulcncflem  15850  ivthinclemlopn  15879  ivthinclemuopn  15881  limcimolemlt  15907  limcimo  15908  cnplimclemle  15911  limccnp2lem  15919  dveflem  15969  efltlemlt  16017  pilem3  16027  cxplt  16168  cxple  16169  rpcxple2  16170  rpcxplt2  16171  rpcxpsqrt  16174  rpabscxpbnd  16192  logbgt0b  16219  logbgcd1irr  16220  logbgcd1irraplemexp  16221  log2tlbndlog2  16237  chtqwordi  16280  bclbnd  16324  prmefexple  16325  bposlem1  16328  bposlem5  16332  bposlem6  16333  bposlem7  16334  qdencn  17295  cvgcmp2nlemabs  17304  iooref1o  17306  trilpolemclim  17309  trilpolemisumle  17311  trilpolemeq1  17313  nconstwlpolemgt0  17338  taupi  17347