Theorem rpred 9853

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

Syntax hints:   -> wi 4   e. wcel 2178   RRcr 7959   RR+crp 9810

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rab 2495  df-in 3180  df-ss 3187  df-rp 9811

This theorem is referenced by:  rpxrd  9854  rpcnd  9855  rpregt0d  9860  rprege0d  9861  rprene0d  9862  rprecred  9865  ltmulgt11d  9889  ltmulgt12d  9890  gt0divd  9891  ge0divd  9892  lediv12ad  9913  ltexp2a  10773  leexp2a  10774  expnlbnd2  10847  cvg1nlemcxze  11408  cvg1nlemcau  11410  cvg1nlemres  11411  cvg1n  11412  resqrexlemp1rp  11432  resqrexlemfp1  11435  resqrexlemover  11436  resqrexlemdec  11437  resqrexlemdecn  11438  resqrexlemlo  11439  resqrexlemcalc1  11440  resqrexlemcalc2  11441  resqrexlemcalc3  11442  resqrexlemnmsq  11443  resqrexlemnm  11444  resqrexlemcvg  11445  resqrexlemgt0  11446  resqrexlemoverl  11447  resqrexlemglsq  11448  resqrexlemga  11449  cau3lem  11540  bdtrilem  11665  bdtri  11666  addcn2  11736  mulcn2  11738  reccn2ap  11739  climrecvg1n  11774  climcvg1nlem  11775  isumrpcl  11920  expcnvap0  11928  absgtap  11936  cvgratnnlemsumlt  11954  cvgratnnlemfm  11955  cvgratnnlemrate  11956  mertenslemi1  11961  effsumlt  12118  eirraplem  12203  bitsmod  12382  4sqlem7  12822  ssblex  15018  metss2lem  15084  addcncntoplem  15148  mulcncflem  15194  ivthinclemlopn  15223  ivthinclemuopn  15225  limcimolemlt  15251  limcimo  15252  cnplimclemle  15255  limccnp2lem  15263  dveflem  15313  efltlemlt  15361  pilem3  15370  cxplt  15503  cxple  15504  rpcxple2  15505  rpcxplt2  15506  rpcxpsqrt  15509  rpabscxpbnd  15527  logbgt0b  15553  logbgcd1irr  15554  logbgcd1irraplemexp  15555  qdencn  16168  cvgcmp2nlemabs  16173  iooref1o  16175  trilpolemclim  16177  trilpolemisumle  16179  trilpolemeq1  16181  nconstwlpolemgt0  16205  taupi  16214