ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rpred Unicode version

Theorem rpred 9429
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
StepHypRef Expression
1 rpssre 9400 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3063 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1463   RRcr 7583   RR+crp 9390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-rab 2400  df-in 3045  df-ss 3052  df-rp 9391
This theorem is referenced by:  rpxrd  9430  rpcnd  9431  rpregt0d  9436  rprege0d  9437  rprene0d  9438  rprecred  9441  ltmulgt11d  9465  ltmulgt12d  9466  gt0divd  9467  ge0divd  9468  lediv12ad  9489  ltexp2a  10285  leexp2a  10286  expnlbnd2  10357  cvg1nlemcxze  10694  cvg1nlemcau  10696  cvg1nlemres  10697  cvg1n  10698  resqrexlemp1rp  10718  resqrexlemfp1  10721  resqrexlemover  10722  resqrexlemdec  10723  resqrexlemdecn  10724  resqrexlemlo  10725  resqrexlemcalc1  10726  resqrexlemcalc2  10727  resqrexlemcalc3  10728  resqrexlemnmsq  10729  resqrexlemnm  10730  resqrexlemcvg  10731  resqrexlemgt0  10732  resqrexlemoverl  10733  resqrexlemglsq  10734  resqrexlemga  10735  cau3lem  10826  bdtrilem  10950  bdtri  10951  addcn2  11019  mulcn2  11021  reccn2ap  11022  climrecvg1n  11057  climcvg1nlem  11058  isumrpcl  11203  expcnvap0  11211  absgtap  11219  cvgratnnlemsumlt  11237  cvgratnnlemfm  11238  cvgratnnlemrate  11239  mertenslemi1  11244  effsumlt  11297  eirraplem  11379  ssblex  12495  metss2lem  12561  addcncntoplem  12615  mulcncflem  12654  limcimolemlt  12685  limcimo  12686  cnplimclemle  12689  limccnp2lem  12697  dveflem  12738  qdencn  13033  cvgcmp2nlemabs  13038  trilpolemclim  13040  trilpolemisumle  13042  trilpolemeq1  13044
  Copyright terms: Public domain W3C validator