Theorem rpgt0 13057

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5107  ℝcr 11126  0cc0 11127   < clt 11270  ℝ⁺crp 13044

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-rp 13045

This theorem is used by:  rpge0  13058  neglt  13064  rpgecl  13074  0nrp  13081  rpgt0d  13091  addlelt  13160  0mod  13965  sgnrrp  15166  01sqrexlem2  15332  01sqrexlem4  15334  01sqrexlem6  15336  resqrex  15339  rpsqrtcl  15353  climconst  15632  rlimconst  15633  divrcnv  15943  rprisefaccl  16114  blcntrps  24642  blcntr  24643  stdbdmet  24746  stdbdmopn  24748  prdsxmslem2  24759  metustid  24784  nmoix  24959  metdseq0  25085  lebnumii  25198  itgulm  26644  pilem2  26688  cos02pilt1  26764  tanregt0  26777  logdmnrp  26879  cxple2  26935  asinneg  27124  asin1  27132  reasinsin  27134  atanbndlem  27163  atanbnd  27164  atan1  27166  rlimcnp  27203  chtrpcl  27412  ppiltx  27414  bposlem8  27528  pntlem3  27846  padicabvcxp  27869  0cnop  32461  0cnfn  32462  rpdp2cl  33329  xdivpnfrp  33380  pnfinf  33625  hgt750lem2  35162  taupilem1  38075  itg2gt0cn  38426  areacirclem1  38459  areacirclem4  38462  prdstotbnd  38546  prdsbnd2  38547  aks4d1p1p6  42941  irrapxlem3  43667  xralrple2  46186  constlimc  46456  0cnv  46572  ioodvbdlimc1lem1  46761  fourierdlem103  47039  fourierdlem104  47040  etransclem18  47082  etransclem46  47110  hoidmvlelem3  47427