Theorem rpred 9765

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℝcr 7873  ℝ⁺crp 9722

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rab 2481  df-in 3160  df-ss 3167  df-rp 9723

This theorem is referenced by:  rpxrd  9766  rpcnd  9767  rpregt0d  9772  rprege0d  9773  rprene0d  9774  rprecred  9777  ltmulgt11d  9801  ltmulgt12d  9802  gt0divd  9803  ge0divd  9804  lediv12ad  9825  ltexp2a  10665  leexp2a  10666  expnlbnd2  10739  cvg1nlemcxze  11129  cvg1nlemcau  11131  cvg1nlemres  11132  cvg1n  11133  resqrexlemp1rp  11153  resqrexlemfp1  11156  resqrexlemover  11157  resqrexlemdec  11158  resqrexlemdecn  11159  resqrexlemlo  11160  resqrexlemcalc1  11161  resqrexlemcalc2  11162  resqrexlemcalc3  11163  resqrexlemnmsq  11164  resqrexlemnm  11165  resqrexlemcvg  11166  resqrexlemgt0  11167  resqrexlemoverl  11168  resqrexlemglsq  11169  resqrexlemga  11170  cau3lem  11261  bdtrilem  11385  bdtri  11386  addcn2  11456  mulcn2  11458  reccn2ap  11459  climrecvg1n  11494  climcvg1nlem  11495  isumrpcl  11640  expcnvap0  11648  absgtap  11656  cvgratnnlemsumlt  11674  cvgratnnlemfm  11675  cvgratnnlemrate  11676  mertenslemi1  11681  effsumlt  11838  eirraplem  11923  4sqlem7  12525  ssblex  14610  metss2lem  14676  addcncntoplem  14740  mulcncflem  14786  ivthinclemlopn  14815  ivthinclemuopn  14817  limcimolemlt  14843  limcimo  14844  cnplimclemle  14847  limccnp2lem  14855  dveflem  14905  efltlemlt  14950  pilem3  14959  cxplt  15091  cxple  15092  rpcxple2  15093  rpcxplt2  15094  rpcxpsqrt  15097  rpabscxpbnd  15114  logbgt0b  15139  logbgcd1irr  15140  logbgcd1irraplemexp  15141  qdencn  15587  cvgcmp2nlemabs  15592  iooref1o  15594  trilpolemclim  15596  trilpolemisumle  15598  trilpolemeq1  15600  nconstwlpolemgt0  15624  taupi  15633