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

Theorem rpred 9171
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 9142 . 2  |-  RR+  C_  RR
2 rpred.1 . 2  |-  ( ph  ->  A  e.  RR+ )
31, 2sseldi 3023 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1438   RRcr 7347   RR+crp 9132
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rab 2368  df-in 3005  df-ss 3012  df-rp 9133
This theorem is referenced by:  rpxrd  9172  rpcnd  9173  rpregt0d  9178  rprege0d  9179  rprene0d  9180  rprecred  9183  ltmulgt11d  9207  ltmulgt12d  9208  gt0divd  9209  ge0divd  9210  lediv12ad  9231  ltexp2a  10003  leexp2a  10004  expnlbnd2  10075  cvg1nlemcxze  10411  cvg1nlemcau  10413  cvg1nlemres  10414  cvg1n  10415  resqrexlemp1rp  10435  resqrexlemfp1  10438  resqrexlemover  10439  resqrexlemdec  10440  resqrexlemdecn  10441  resqrexlemlo  10442  resqrexlemcalc1  10443  resqrexlemcalc2  10444  resqrexlemcalc3  10445  resqrexlemnmsq  10446  resqrexlemnm  10447  resqrexlemcvg  10448  resqrexlemgt0  10449  resqrexlemoverl  10450  resqrexlemglsq  10451  resqrexlemga  10452  cau3lem  10543  addcn2  10695  mulcn2  10697  climrecvg1n  10733  climcvg1nlem  10734  isumrpcl  10884  expcnvap0  10892  absgtap  10900  cvgratnnlemsumlt  10918  cvgratnnlemfm  10919  cvgratnnlemrate  10920  mertenslemi1  10925  effsumlt  10978  eirraplem  11060  qdencn  11870
  Copyright terms: Public domain W3C validator