Theorem rpgt0 12922

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5099  ℝcr 11029  0cc0 11030   < clt 11170  ℝ⁺crp 12909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-rp 12910

This theorem is referenced by:  rpge0  12923  neglt  12929  rpgecl  12939  0nrp  12946  rpgt0d  12956  addlelt  13025  0mod  13826  sgnrrp  15018  01sqrexlem2  15170  01sqrexlem4  15172  01sqrexlem6  15174  resqrex  15177  rpsqrtcl  15191  climconst  15470  rlimconst  15471  divrcnv  15779  rprisefaccl  15950  blcntrps  24360  blcntr  24361  stdbdmet  24464  stdbdmopn  24466  prdsxmslem2  24477  metustid  24502  nmoix  24677  metdseq0  24803  lebnumii  24925  itgulm  26377  pilem2  26422  cos02pilt1  26495  tanregt0  26508  logdmnrp  26610  cxple2  26666  asinneg  26856  asin1  26864  reasinsin  26866  atanbndlem  26895  atanbnd  26896  atan1  26898  rlimcnp  26935  chtrpcl  27145  ppiltx  27147  bposlem8  27262  pntlem3  27580  padicabvcxp  27603  0cnop  32037  0cnfn  32038  rpdp2cl  32944  xdivpnfrp  32995  pnfinf  33246  hgt750lem2  34790  taupilem1  37497  itg2gt0cn  37847  areacirclem1  37880  areacirclem4  37883  prdstotbnd  37966  prdsbnd2  37967  aks4d1p1p6  42364  irrapxlem3  43102  xralrple2  45635  constlimc  45906  0cnv  46022  ioodvbdlimc1lem1  46211  fourierdlem103  46489  fourierdlem104  46490  etransclem18  46532  etransclem46  46560  hoidmvlelem3  46877