Theorem rpgt0 13035

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142   class class class wbr 5108  ℝcr 11105  0cc0 11106   < clt 11249  ℝ⁺crp 13022

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-rp 13023

This theorem is used by:  rpge0  13036  neglt  13042  rpgecl  13052  0nrp  13059  rpgt0d  13069  addlelt  13138  0mod  13942  sgnrrp  15135  01sqrexlem2  15301  01sqrexlem4  15303  01sqrexlem6  15305  resqrex  15308  rpsqrtcl  15322  climconst  15601  rlimconst  15602  divrcnv  15913  rprisefaccl  16084  blcntrps  24580  blcntr  24581  stdbdmet  24684  stdbdmopn  24686  prdsxmslem2  24697  metustid  24722  nmoix  24897  metdseq0  25023  lebnumii  25136  itgulm  26582  pilem2  26626  cos02pilt1  26702  tanregt0  26715  logdmnrp  26817  cxple2  26873  asinneg  27062  asin1  27070  reasinsin  27072  atanbndlem  27101  atanbnd  27102  atan1  27104  rlimcnp  27141  chtrpcl  27350  ppiltx  27352  bposlem8  27466  pntlem3  27784  padicabvcxp  27807  0cnop  32342  0cnfn  32343  rpdp2cl  33212  xdivpnfrp  33263  pnfinf  33512  hgt750lem2  35048  taupilem1  37993  itg2gt0cn  38354  areacirclem1  38387  areacirclem4  38390  prdstotbnd  38473  prdsbnd2  38474  aks4d1p1p6  42868  irrapxlem3  43579  xralrple2  46098  constlimc  46368  0cnv  46484  ioodvbdlimc1lem1  46673  fourierdlem103  46951  fourierdlem104  46952  etransclem18  46994  etransclem46  47022  hoidmvlelem3  47339