Theorem rpgt0 12971

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074  0cc0 11075   < clt 11215  ℝ⁺crp 12958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-rp 12959

This theorem is referenced by:  rpge0  12972  neglt  12978  rpgecl  12988  0nrp  12995  rpgt0d  13005  addlelt  13074  0mod  13871  sgnrrp  15064  01sqrexlem2  15216  01sqrexlem4  15218  01sqrexlem6  15220  resqrex  15223  rpsqrtcl  15237  climconst  15516  rlimconst  15517  divrcnv  15825  rprisefaccl  15996  blcntrps  24307  blcntr  24308  stdbdmet  24411  stdbdmopn  24413  prdsxmslem2  24424  metustid  24449  nmoix  24624  metdseq0  24750  lebnumii  24872  itgulm  26324  pilem2  26369  cos02pilt1  26442  tanregt0  26455  logdmnrp  26557  cxple2  26613  asinneg  26803  asin1  26811  reasinsin  26813  atanbndlem  26842  atanbnd  26843  atan1  26845  rlimcnp  26882  chtrpcl  27092  ppiltx  27094  bposlem8  27209  pntlem3  27527  padicabvcxp  27550  0cnop  31915  0cnfn  31916  rpdp2cl  32809  xdivpnfrp  32860  pnfinf  33144  hgt750lem2  34650  taupilem1  37316  itg2gt0cn  37676  areacirclem1  37709  areacirclem4  37712  prdstotbnd  37795  prdsbnd2  37796  aks4d1p1p6  42068  irrapxlem3  42819  xralrple2  45357  constlimc  45629  0cnv  45747  ioodvbdlimc1lem1  45936  fourierdlem103  46214  fourierdlem104  46215  etransclem18  46257  etransclem46  46285  hoidmvlelem3  46602