Theorem rpgt0 12924

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 12913	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2	1	simprbi 496	1 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5095  ℝcr 11027  0cc0 11028   < clt 11168  ℝ⁺crp 12911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-rp 12912

This theorem is referenced by:  rpge0  12925  neglt  12931  rpgecl  12941  0nrp  12948  rpgt0d  12958  addlelt  13027  0mod  13824  sgnrrp  15016  01sqrexlem2  15168  01sqrexlem4  15170  01sqrexlem6  15172  resqrex  15175  rpsqrtcl  15189  climconst  15468  rlimconst  15469  divrcnv  15777  rprisefaccl  15948  blcntrps  24316  blcntr  24317  stdbdmet  24420  stdbdmopn  24422  prdsxmslem2  24433  metustid  24458  nmoix  24633  metdseq0  24759  lebnumii  24881  itgulm  26333  pilem2  26378  cos02pilt1  26451  tanregt0  26464  logdmnrp  26566  cxple2  26622  asinneg  26812  asin1  26820  reasinsin  26822  atanbndlem  26851  atanbnd  26852  atan1  26854  rlimcnp  26891  chtrpcl  27101  ppiltx  27103  bposlem8  27218  pntlem3  27536  padicabvcxp  27559  0cnop  31941  0cnfn  31942  rpdp2cl  32835  xdivpnfrp  32886  pnfinf  33135  hgt750lem2  34619  taupilem1  37294  itg2gt0cn  37654  areacirclem1  37687  areacirclem4  37690  prdstotbnd  37773  prdsbnd2  37774  aks4d1p1p6  42046  irrapxlem3  42797  xralrple2  45334  constlimc  45606  0cnv  45724  ioodvbdlimc1lem1  45913  fourierdlem103  46191  fourierdlem104  46192  etransclem18  46234  etransclem46  46262  hoidmvlelem3  46579