Theorem rpgt0 12944

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

Assertion

Ref	Expression
rpgt0	⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)

Proof of Theorem rpgt0

Step	Hyp	Ref	Expression
1		elrp 12933	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2	1	simprbi 497	1 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ℝcr 11026  0cc0 11027   < clt 11168  ℝ⁺crp 12931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-rp 12932

This theorem is referenced by:  rpge0  12945  neglt  12951  rpgecl  12961  0nrp  12968  rpgt0d  12978  addlelt  13047  0mod  13850  sgnrrp  15042  01sqrexlem2  15194  01sqrexlem4  15196  01sqrexlem6  15198  resqrex  15201  rpsqrtcl  15215  climconst  15494  rlimconst  15495  divrcnv  15806  rprisefaccl  15977  blcntrps  24386  blcntr  24387  stdbdmet  24490  stdbdmopn  24492  prdsxmslem2  24503  metustid  24528  nmoix  24703  metdseq0  24829  lebnumii  24942  itgulm  26388  pilem2  26433  cos02pilt1  26506  tanregt0  26519  logdmnrp  26621  cxple2  26677  asinneg  26867  asin1  26875  reasinsin  26877  atanbndlem  26906  atanbnd  26907  atan1  26909  rlimcnp  26946  chtrpcl  27156  ppiltx  27158  bposlem8  27273  pntlem3  27591  padicabvcxp  27614  0cnop  32070  0cnfn  32071  rpdp2cl  32961  xdivpnfrp  33012  pnfinf  33264  hgt750lem2  34817  taupilem1  37648  itg2gt0cn  38007  areacirclem1  38040  areacirclem4  38043  prdstotbnd  38126  prdsbnd2  38127  aks4d1p1p6  42523  irrapxlem3  43267  xralrple2  45799  constlimc  46069  0cnv  46185  ioodvbdlimc1lem1  46374  fourierdlem103  46652  fourierdlem104  46653  etransclem18  46695  etransclem46  46723  hoidmvlelem3  47040