Theorem rpred 10035

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 10003	. 2 ⊢ ℝ+ ⊆ ℝ
2		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
3	1, 2	sselid 3238	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2205  ℝcr 8131  ℝ⁺crp 9992

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rab 2531  df-in 3219  df-ss 3226  df-rp 9993

This theorem is referenced by:  rpxrd  10036  rpcnd  10037  rpregt0d  10042  rprege0d  10043  rprene0d  10044  rprecred  10047  ltmulgt11d  10071  ltmulgt12d  10072  gt0divd  10073  ge0divd  10074  lediv12ad  10095  ltexp2a  10960  leexp2a  10961  expnlbnd2  11035  cvg1nlemcxze  11675  cvg1nlemcau  11677  cvg1nlemres  11678  cvg1n  11679  resqrexlemp1rp  11699  resqrexlemfp1  11702  resqrexlemover  11703  resqrexlemdec  11704  resqrexlemdecn  11705  resqrexlemlo  11706  resqrexlemcalc1  11707  resqrexlemcalc2  11708  resqrexlemcalc3  11709  resqrexlemnmsq  11710  resqrexlemnm  11711  resqrexlemcvg  11712  resqrexlemgt0  11713  resqrexlemoverl  11714  resqrexlemglsq  11715  resqrexlemga  11716  cau3lem  11807  bdtrilem  11932  bdtri  11933  addcn2  12003  mulcn2  12005  reccn2ap  12006  climrecvg1n  12041  climcvg1nlem  12042  isumrpcl  12188  expcnvap0  12196  absgtap  12204  cvgratnnlemsumlt  12222  cvgratnnlemfm  12223  cvgratnnlemrate  12224  mertenslemi1  12229  effsumlt  12386  eirraplem  12471  bitsmod  12650  4sqlem7  13090  ssblex  15345  metss2lem  15411  addcncntoplem  15475  mulcncflem  15521  ivthinclemlopn  15550  ivthinclemuopn  15552  limcimolemlt  15578  limcimo  15579  cnplimclemle  15582  limccnp2lem  15590  dveflem  15640  efltlemlt  15688  pilem3  15697  cxplt  15830  cxple  15831  rpcxple2  15832  rpcxplt2  15833  rpcxpsqrt  15836  rpabscxpbnd  15854  logbgt0b  15880  logbgcd1irr  15881  logbgcd1irraplemexp  15882  qdencn  16856  cvgcmp2nlemabs  16865  iooref1o  16867  trilpolemclim  16869  trilpolemisumle  16871  trilpolemeq1  16873  nconstwlpolemgt0  16899  taupi  16908