Theorem rpgt0 12925

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 12914	. 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 12912

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 12913

This theorem is referenced by:  rpge0  12926  neglt  12932  rpgecl  12942  0nrp  12949  rpgt0d  12959  addlelt  13028  0mod  13825  sgnrrp  15017  01sqrexlem2  15169  01sqrexlem4  15171  01sqrexlem6  15173  resqrex  15176  rpsqrtcl  15190  climconst  15469  rlimconst  15470  divrcnv  15778  rprisefaccl  15949  blcntrps  24317  blcntr  24318  stdbdmet  24421  stdbdmopn  24423  prdsxmslem2  24434  metustid  24459  nmoix  24634  metdseq0  24760  lebnumii  24882  itgulm  26334  pilem2  26379  cos02pilt1  26452  tanregt0  26465  logdmnrp  26567  cxple2  26623  asinneg  26813  asin1  26821  reasinsin  26823  atanbndlem  26852  atanbnd  26853  atan1  26855  rlimcnp  26892  chtrpcl  27102  ppiltx  27104  bposlem8  27219  pntlem3  27537  padicabvcxp  27560  0cnop  31942  0cnfn  31943  rpdp2cl  32841  xdivpnfrp  32892  pnfinf  33144  hgt750lem2  34639  taupilem1  37314  itg2gt0cn  37674  areacirclem1  37707  areacirclem4  37710  prdstotbnd  37793  prdsbnd2  37794  aks4d1p1p6  42066  irrapxlem3  42817  xralrple2  45354  constlimc  45625  0cnv  45743  ioodvbdlimc1lem1  45932  fourierdlem103  46210  fourierdlem104  46211  etransclem18  46253  etransclem46  46281  hoidmvlelem3  46598