Theorem rpgt0 11720

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

Syntax hints:   → wi 4   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814  0cc0 9815   < clt 9953  ℝ⁺crp 11708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-rp 11709

This theorem is referenced by:  rpge0  11721  rpgecl  11735  0nrp  11741  rpgt0d  11751  addlelt  11818  0mod  12563  sgnrrp  13679  sqrlem2  13832  sqrlem4  13834  sqrlem6  13836  resqrex  13839  rpsqrtcl  13853  climconst  14122  rlimconst  14123  divrcnv  14423  rprisefaccl  14593  blcntrps  22027  blcntr  22028  stdbdmet  22131  stdbdmopn  22133  prdsxmslem2  22144  metustid  22169  nmoix  22343  metdseq0  22465  lebnumii  22573  itgulm  23966  pilem2  24010  tanregt0  24089  logdmnrp  24187  cxple2  24243  asinneg  24413  asin1  24421  reasinsin  24423  atanbndlem  24452  atanbnd  24453  atan1  24455  rlimcnp  24492  chtrpcl  24701  ppiltx  24703  bposlem8  24816  pntlem3  25098  padicabvcxp  25121  0cnop  28222  0cnfn  28223  xdivpnfrp  28972  pnfinf  29068  taupilem1  32344  itg2gt0cn  32635  areacirclem1  32670  areacirclem4  32673  prdstotbnd  32763  prdsbnd2  32764  irrapxlem3  36406  neglt  38437  xralrple2  38511  constlimc  38691  ioodvbdlimc1lem1  38821  fourierdlem103  39102  fourierdlem104  39103  etransclem18  39145  etransclem46  39173  hoidmvlelem3  39487