Theorem rpred 10115

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

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

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 10073

This theorem is used by:  rpxrd  10116  rpcnd  10117  rpregt0d  10122  rprege0d  10123  rprene0d  10124  rprecred  10127  ltmulgt11d  10151  ltmulgt12d  10152  gt0divd  10153  ge0divd  10154  lediv12ad  10175  ltexp2a  11050  leexp2a  11051  expnlbnd2  11125  cvg1nlemcxze  11771  cvg1nlemcau  11773  cvg1nlemres  11774  cvg1n  11775  resqrexlemp1rp  11795  resqrexlemfp1  11798  resqrexlemover  11799  resqrexlemdec  11800  resqrexlemdecn  11801  resqrexlemlo  11802  resqrexlemcalc1  11803  resqrexlemcalc2  11804  resqrexlemcalc3  11805  resqrexlemnmsq  11806  resqrexlemnm  11807  resqrexlemcvg  11808  resqrexlemgt0  11809  resqrexlemoverl  11810  resqrexlemglsq  11811  resqrexlemga  11812  cau3lem  11904  bdtrilem  12031  bdtri  12032  addcn2  12102  mulcn2  12104  reccn2ap  12105  climrecvg1n  12140  climcvg1nlem  12141  isumrpcl  12287  expcnvap0  12295  absgtap  12303  cvgratnnlemsumlt  12321  cvgratnnlemfm  12322  cvgratnnlemrate  12323  mertenslemi1  12328  effsumlt  12485  eirraplem  12570  bitsmod  12749  4sqlem7  13193  ssblex  15669  metss2lem  15735  addcncntoplem  15799  mulcncflem  15845  ivthinclemlopn  15874  ivthinclemuopn  15876  limcimolemlt  15902  limcimo  15903  cnplimclemle  15906  limccnp2lem  15914  dveflem  15964  efltlemlt  16012  pilem3  16022  cxplt  16163  cxple  16164  rpcxple2  16165  rpcxplt2  16166  rpcxpsqrt  16169  rpabscxpbnd  16187  logbgt0b  16214  logbgcd1irr  16215  logbgcd1irraplemexp  16216  log2tlbndlog2  16232  chtqwordi  16275  bclbnd  16319  prmefexple  16320  bposlem1  16323  bposlem5  16327  bposlem6  16328  bposlem7  16329  qdencn  17290  cvgcmp2nlemabs  17299  iooref1o  17301  trilpolemclim  17304  trilpolemisumle  17306  trilpolemeq1  17308  nconstwlpolemgt0  17333  taupi  17342