Theorem rpgt0 13103

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5102  ℝcr 11171  0cc0 11172   < clt 11315  ℝ⁺crp 13090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-rp 13091

This theorem is used by:  rpge0  13104  neglt  13110  rpgecl  13120  0nrp  13127  rpgt0d  13137  addlelt  13206  0mod  14011  sgnrrp  15212  01sqrexlem2  15378  01sqrexlem4  15380  01sqrexlem6  15382  resqrex  15385  rpsqrtcl  15399  climconst  15678  rlimconst  15679  divrcnv  15989  rprisefaccl  16158  blcntrps  24693  blcntr  24694  stdbdmet  24797  stdbdmopn  24799  prdsxmslem2  24810  metustid  24835  nmoix  25010  metdseq0  25136  lebnumii  25249  itgulm  26699  pilem2  26743  cos02pilt1  26818  tanregt0  26831  logdmnrp  26933  cxple2  26989  asinneg  27178  asin1  27186  reasinsin  27188  atanbndlem  27217  atanbnd  27218  atan1  27220  rlimcnp  27257  chtrpcl  27466  ppiltx  27468  bposlem8  27582  pntlem3  27900  padicabvcxp  27923  0cnop  32515  0cnfn  32516  rpdp2cl  33382  xdivpnfrp  33433  pnfinf  33678  hgt750lem2  35216  taupilem1  38162  itg2gt0cn  38513  areacirclem1  38546  areacirclem4  38549  prdstotbnd  38648  prdsbnd2  38649  aks4d1p1p6  43043  irrapxlem3  43769  xralrple2  46288  constlimc  46558  0cnv  46674  ioodvbdlimc1lem1  46863  fourierdlem103  47141  fourierdlem104  47142  etransclem18  47184  etransclem46  47212  hoidmvlelem3  47529