Theorem rpred 9892

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

Hypothesis

Ref	Expression
rpred.1	|- ( ph -> A e. RR+ )

Assertion

Ref	Expression
rpred	|- ( ph -> A e. RR )

Proof of Theorem rpred

Step	Hyp	Ref	Expression
1		rpssre 9860	. 2 |- RR+ C_ RR
2		rpred.1	. 2 |- ( ph -> A e. RR+ )
3	1, 2	sselid 3222	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 7998   RR+crp 9849

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-in 3203  df-ss 3210  df-rp 9850

This theorem is referenced by:  rpxrd  9893  rpcnd  9894  rpregt0d  9899  rprege0d  9900  rprene0d  9901  rprecred  9904  ltmulgt11d  9928  ltmulgt12d  9929  gt0divd  9930  ge0divd  9931  lediv12ad  9952  ltexp2a  10813  leexp2a  10814  expnlbnd2  10887  cvg1nlemcxze  11493  cvg1nlemcau  11495  cvg1nlemres  11496  cvg1n  11497  resqrexlemp1rp  11517  resqrexlemfp1  11520  resqrexlemover  11521  resqrexlemdec  11522  resqrexlemdecn  11523  resqrexlemlo  11524  resqrexlemcalc1  11525  resqrexlemcalc2  11526  resqrexlemcalc3  11527  resqrexlemnmsq  11528  resqrexlemnm  11529  resqrexlemcvg  11530  resqrexlemgt0  11531  resqrexlemoverl  11532  resqrexlemglsq  11533  resqrexlemga  11534  cau3lem  11625  bdtrilem  11750  bdtri  11751  addcn2  11821  mulcn2  11823  reccn2ap  11824  climrecvg1n  11859  climcvg1nlem  11860  isumrpcl  12005  expcnvap0  12013  absgtap  12021  cvgratnnlemsumlt  12039  cvgratnnlemfm  12040  cvgratnnlemrate  12041  mertenslemi1  12046  effsumlt  12203  eirraplem  12288  bitsmod  12467  4sqlem7  12907  ssblex  15105  metss2lem  15171  addcncntoplem  15235  mulcncflem  15281  ivthinclemlopn  15310  ivthinclemuopn  15312  limcimolemlt  15338  limcimo  15339  cnplimclemle  15342  limccnp2lem  15350  dveflem  15400  efltlemlt  15448  pilem3  15457  cxplt  15590  cxple  15591  rpcxple2  15592  rpcxplt2  15593  rpcxpsqrt  15596  rpabscxpbnd  15614  logbgt0b  15640  logbgcd1irr  15641  logbgcd1irraplemexp  15642  qdencn  16395  cvgcmp2nlemabs  16400  iooref1o  16402  trilpolemclim  16404  trilpolemisumle  16406  trilpolemeq1  16408  nconstwlpolemgt0  16432  taupi  16441