Theorem rpred 10114

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

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

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 10072

This theorem is used by:  rpxrd  10115  rpcnd  10116  rpregt0d  10121  rprege0d  10122  rprene0d  10123  rprecred  10126  ltmulgt11d  10150  ltmulgt12d  10151  gt0divd  10152  ge0divd  10153  lediv12ad  10174  ltexp2a  11049  leexp2a  11050  expnlbnd2  11124  cvg1nlemcxze  11770  cvg1nlemcau  11772  cvg1nlemres  11773  cvg1n  11774  resqrexlemp1rp  11794  resqrexlemfp1  11797  resqrexlemover  11798  resqrexlemdec  11799  resqrexlemdecn  11800  resqrexlemlo  11801  resqrexlemcalc1  11802  resqrexlemcalc2  11803  resqrexlemcalc3  11804  resqrexlemnmsq  11805  resqrexlemnm  11806  resqrexlemcvg  11807  resqrexlemgt0  11808  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemga  11811  cau3lem  11903  bdtrilem  12030  bdtri  12031  addcn2  12101  mulcn2  12103  reccn2ap  12104  climrecvg1n  12139  climcvg1nlem  12140  isumrpcl  12286  expcnvap0  12294  absgtap  12302  cvgratnnlemsumlt  12320  cvgratnnlemfm  12321  cvgratnnlemrate  12322  mertenslemi1  12327  effsumlt  12484  eirraplem  12569  bitsmod  12748  4sqlem7  13192  ssblex  15654  metss2lem  15720  addcncntoplem  15784  mulcncflem  15830  ivthinclemlopn  15859  ivthinclemuopn  15861  limcimolemlt  15887  limcimo  15888  cnplimclemle  15891  limccnp2lem  15899  dveflem  15949  efltlemlt  15997  pilem3  16007  cxplt  16148  cxple  16149  rpcxple2  16150  rpcxplt2  16151  rpcxpsqrt  16154  rpabscxpbnd  16172  logbgt0b  16199  logbgcd1irr  16200  logbgcd1irraplemexp  16201  log2tlbndlog2  16217  chtqwordi  16260  bclbnd  16304  prmefexple  16305  bposlem1  16308  bposlem5  16312  bposlem6  16313  bposlem7  16314  qdencn  17275  cvgcmp2nlemabs  17284  iooref1o  17286  trilpolemclim  17289  trilpolemisumle  17291  trilpolemeq1  17293  nconstwlpolemgt0  17318  taupi  17327