Theorem rpred 10099

Description: A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpred	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem rpred

Step	Hyp	Ref	Expression
1		rpssre 10067	. 2 ⊢ ℝ+ ⊆ ℝ
2		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
3	1, 2	sselid 3246	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℝcr 8178  ℝ⁺crp 10056

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 10057

This theorem is used by:  rpxrd  10100  rpcnd  10101  rpregt0d  10106  rprege0d  10107  rprene0d  10108  rprecred  10111  ltmulgt11d  10135  ltmulgt12d  10136  gt0divd  10137  ge0divd  10138  lediv12ad  10159  ltexp2a  11030  leexp2a  11031  expnlbnd2  11105  cvg1nlemcxze  11750  cvg1nlemcau  11752  cvg1nlemres  11753  cvg1n  11754  resqrexlemp1rp  11774  resqrexlemfp1  11777  resqrexlemover  11778  resqrexlemdec  11779  resqrexlemdecn  11780  resqrexlemlo  11781  resqrexlemcalc1  11782  resqrexlemcalc2  11783  resqrexlemcalc3  11784  resqrexlemnmsq  11785  resqrexlemnm  11786  resqrexlemcvg  11787  resqrexlemgt0  11788  resqrexlemoverl  11789  resqrexlemglsq  11790  resqrexlemga  11791  cau3lem  11882  bdtrilem  12007  bdtri  12008  addcn2  12078  mulcn2  12080  reccn2ap  12081  climrecvg1n  12116  climcvg1nlem  12117  isumrpcl  12263  expcnvap0  12271  absgtap  12279  cvgratnnlemsumlt  12297  cvgratnnlemfm  12298  cvgratnnlemrate  12299  mertenslemi1  12304  effsumlt  12461  eirraplem  12546  bitsmod  12725  4sqlem7  13165  ssblex  15534  metss2lem  15600  addcncntoplem  15664  mulcncflem  15710  ivthinclemlopn  15739  ivthinclemuopn  15741  limcimolemlt  15767  limcimo  15768  cnplimclemle  15771  limccnp2lem  15779  dveflem  15829  efltlemlt  15877  pilem3  15887  cxplt  16024  cxple  16025  rpcxple2  16026  rpcxplt2  16027  rpcxpsqrt  16030  rpabscxpbnd  16048  logbgt0b  16074  logbgcd1irr  16075  logbgcd1irraplemexp  16076  log2tlbndlog2  16088  bclbnd  16127  qdencn  17084  cvgcmp2nlemabs  17093  iooref1o  17095  trilpolemclim  17097  trilpolemisumle  17099  trilpolemeq1  17101  nconstwlpolemgt0  17126  taupi  17135