Theorem rpgt0 12936

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5110  ℝcr 11059  0cc0 11060   < clt 11198  ℝ⁺crp 12924

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-rp 12925

This theorem is referenced by:  rpge0  12937  rpgecl  12952  0nrp  12959  rpgt0d  12969  addlelt  13038  0mod  13817  sgnrrp  14988  01sqrexlem2  15140  01sqrexlem4  15142  01sqrexlem6  15144  resqrex  15147  rpsqrtcl  15161  climconst  15437  rlimconst  15438  divrcnv  15748  rprisefaccl  15917  blcntrps  23802  blcntr  23803  stdbdmet  23909  stdbdmopn  23911  prdsxmslem2  23922  metustid  23947  nmoix  24130  metdseq0  24254  lebnumii  24366  itgulm  25804  pilem2  25848  cos02pilt1  25919  tanregt0  25932  logdmnrp  26033  cxple2  26089  asinneg  26273  asin1  26281  reasinsin  26283  atanbndlem  26312  atanbnd  26313  atan1  26315  rlimcnp  26352  chtrpcl  26561  ppiltx  26563  bposlem8  26676  pntlem3  26994  padicabvcxp  27017  0cnop  30984  0cnfn  30985  rpdp2cl  31808  xdivpnfrp  31859  pnfinf  32089  hgt750lem2  33354  taupilem1  35865  itg2gt0cn  36206  areacirclem1  36239  areacirclem4  36242  prdstotbnd  36326  prdsbnd2  36327  aks4d1p1p6  40603  irrapxlem3  41205  neglt  43639  xralrple2  43709  constlimc  43985  0cnv  44103  ioodvbdlimc1lem1  44292  fourierdlem103  44570  fourierdlem104  44571  etransclem18  44613  etransclem46  44641  hoidmvlelem3  44958