Theorem rpgt0 12088

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

Syntax hints:   → wi 4   ∈ wcel 2157   class class class wbr 4843  ℝcr 10223  0cc0 10224   < clt 10363  ℝ⁺crp 12074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-br 4844  df-rp 12075

This theorem is referenced by:  rpge0  12089  rpgecl  12104  0nrp  12110  rpgt0d  12120  addlelt  12189  0mod  12956  sgnrrp  14172  sqrlem2  14325  sqrlem4  14327  sqrlem6  14329  resqrex  14332  rpsqrtcl  14346  climconst  14615  rlimconst  14616  divrcnv  14922  rprisefaccl  15090  blcntrps  22545  blcntr  22546  stdbdmet  22649  stdbdmopn  22651  prdsxmslem2  22662  metustid  22687  nmoix  22861  metdseq0  22985  lebnumii  23093  itgulm  24503  pilem2  24547  tanregt0  24627  logdmnrp  24728  cxple2  24784  asinneg  24965  asin1  24973  reasinsin  24975  atanbndlem  25004  atanbnd  25005  atan1  25007  rlimcnp  25044  chtrpcl  25253  ppiltx  25255  bposlem8  25368  pntlem3  25650  padicabvcxp  25673  0cnop  29363  0cnfn  29364  rpdp2cl  30106  xdivpnfrp  30157  pnfinf  30253  hgt750lem2  31250  taupilem1  33666  itg2gt0cn  33953  areacirclem1  33988  areacirclem4  33991  prdstotbnd  34080  prdsbnd2  34081  irrapxlem3  38174  neglt  40242  xralrple2  40314  constlimc  40600  0cnv  40718  ioodvbdlimc1lem1  40890  fourierdlem103  41169  fourierdlem104  41170  etransclem18  41212  etransclem46  41240  hoidmvlelem3  41557