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

Theorem elrpd 9509
Description: Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
Hypotheses
Ref Expression
elrpd.1  |-  ( ph  ->  A  e.  RR )
elrpd.2  |-  ( ph  ->  0  <  A )
Assertion
Ref Expression
elrpd  |-  ( ph  ->  A  e.  RR+ )

Proof of Theorem elrpd
StepHypRef Expression
1 elrpd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 elrpd.2 . 2  |-  ( ph  ->  0  <  A )
3 elrp 9471 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3sylanbrc 414 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1481   class class class wbr 3936   RRcr 7642   0cc0 7643    < clt 7823   RR+crp 9469
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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rab 2426  df-v 2691  df-un 3079  df-sn 3537  df-pr 3538  df-op 3540  df-br 3937  df-rp 9470
This theorem is referenced by:  mul2lt0rgt0  9576  mul2lt0np  9579  zltaddlt1le  9819  modqval  10127  ltexp2a  10375  leexp2a  10376  expnlbnd2  10447  resqrexlem1arp  10808  resqrexlemp1rp  10809  resqrexlemcalc2  10818  resqrexlemcalc3  10819  resqrexlemgt0  10823  resqrexlemglsq  10825  rpsqrtcl  10844  absrpclap  10864  rpmaxcl  11026  rpmincl  11040  xrminrpcl  11074  xrbdtri  11076  mulcn2  11112  reccn2ap  11113  climge0  11125  divcnv  11297  georeclim  11313  cvgratnnlembern  11323  cvgratnnlemsumlt  11328  cvgratnnlemfm  11329  cvgratnnlemrate  11330  cvgratnn  11331  cvgratz  11332  rpefcl  11426  efltim  11439  ef01bndlem  11497  bdmopn  12710  mulcncflem  12796  ivthinclemlopn  12820  ivthinclemuopn  12822  dveflem  12893  reeff1olem  12898  pilem3  12910  tanrpcl  12964  cosordlem  12976  rplogcl  13006  logdivlti  13008  cxplt  13042  cxple  13043  rpabscxpbnd  13065  iooref1o  13424
  Copyright terms: Public domain W3C validator