Theorem rpgt0 11341

Description: A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)

Assertion

Ref	Expression
rpgt0	|- ( A e. RR+ -> 0 < A )

Proof of Theorem rpgt0

Step	Hyp	Ref	Expression
1		elrp 11332	. 2 |- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
2	1	simprbi 470	1 |- ( A e. RR+ -> 0 < A )

Syntax hints:   -> wi 4   e. wcel 1897   class class class wbr 4415   RRcr 9563   0cc0 9564   < clt 9700   RR+crp 11330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-rp 11331

This theorem is referenced by:  rpge0  11342  rpgecl  11356  0nrp  11362  rpgt0d  11372  0mod  12159  sgnrrp  13202  sqrlem2  13355  sqrlem4  13357  sqrlem6  13359  resqrex  13362  rpsqrtcl  13376  climconst  13655  rlimconst  13656  divrcnv  13958  rprisefaccl  14124  blcntrps  21475  blcntr  21476  stdbdmet  21579  stdbdmopn  21581  prdsxmslem2  21592  metustid  21617  nmoix  21782  nmoixOLD  21798  metdseq0  21919  metdseq0OLD  21934  lebnumii  22045  itgulm  23411  pilem2  23455  pilem2OLD  23456  tanregt0  23536  logdmnrp  23634  cxple2  23690  asinneg  23860  asin1  23868  reasinsin  23870  atanbndlem  23899  atanbnd  23900  atan1  23902  rlimcnp  23939  chtrpcl  24150  ppiltx  24152  bposlem8  24267  pntlem3  24495  padicabvcxp  24518  0cnop  27680  0cnfn  27681  xdivpnfrp  28450  pnfinf  28548  taupilem1  31766  itg2gt0cn  32041  areacirclem1  32076  areacirclem4  32079  prdstotbnd  32170  prdsbnd2  32171  irrapxlem3  35712  neglt  37531  xralrple2  37614  constlimc  37741  ioodvbdlimc1lem1  37840  ioodvbdlimc1lem1OLD  37842  fourierdlem103  38110  fourierdlem104  38111  etransclem18  38154  etransclem46  38182  hoidmvlelem3  38456