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

Theorem elrpd 9680
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 9642 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
41, 2, 3sylanbrc 417 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2148   class class class wbr 4000   RRcr 7801   0cc0 7802    < clt 7982   RR+crp 9640
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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2739  df-un 3133  df-sn 3597  df-pr 3598  df-op 3600  df-br 4001  df-rp 9641
This theorem is referenced by:  mul2lt0rgt0  9747  mul2lt0np  9750  zltaddlt1le  9994  modqval  10310  ltexp2a  10558  leexp2a  10559  expnlbnd2  10631  nn0ltexp2  10674  resqrexlem1arp  10998  resqrexlemp1rp  10999  resqrexlemcalc2  11008  resqrexlemcalc3  11009  resqrexlemgt0  11013  resqrexlemglsq  11015  rpsqrtcl  11034  absrpclap  11054  rpmaxcl  11216  rpmincl  11230  xrminrpcl  11266  xrbdtri  11268  mulcn2  11304  reccn2ap  11305  climge0  11317  divcnv  11489  georeclim  11505  cvgratnnlembern  11515  cvgratnnlemsumlt  11520  cvgratnnlemfm  11521  cvgratnnlemrate  11522  cvgratnn  11523  cvgratz  11524  rpefcl  11677  efltim  11690  ef01bndlem  11748  pythagtriplem12  12258  pythagtriplem14  12260  pythagtriplem16  12262  bdmopn  13671  mulcncflem  13757  ivthinclemlopn  13781  ivthinclemuopn  13783  dveflem  13854  reeff1olem  13859  pilem3  13871  tanrpcl  13925  cosordlem  13937  rplogcl  13967  logdivlti  13969  cxplt  14003  cxple  14004  rpabscxpbnd  14026  ltexp2  14027  iooref1o  14438
  Copyright terms: Public domain W3C validator