Theorem rpgt0 13028

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

Syntax hints:   → wi 4   ∈ wcel 2141   class class class wbr 5108  ℝcr 11098  0cc0 11099   < clt 11242  ℝ⁺crp 13015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-rp 13016

This theorem is referenced by:  rpge0  13029  neglt  13035  rpgecl  13045  0nrp  13052  rpgt0d  13062  addlelt  13131  0mod  13935  sgnrrp  15128  01sqrexlem2  15294  01sqrexlem4  15296  01sqrexlem6  15298  resqrex  15301  rpsqrtcl  15315  climconst  15594  rlimconst  15595  divrcnv  15906  rprisefaccl  16077  blcntrps  24548  blcntr  24549  stdbdmet  24652  stdbdmopn  24654  prdsxmslem2  24665  metustid  24690  nmoix  24865  metdseq0  24991  lebnumii  25104  itgulm  26547  pilem2  26591  cos02pilt1  26667  tanregt0  26680  logdmnrp  26782  cxple2  26838  asinneg  27027  asin1  27035  reasinsin  27037  atanbndlem  27066  atanbnd  27067  atan1  27069  rlimcnp  27106  chtrpcl  27315  ppiltx  27317  bposlem8  27431  pntlem3  27749  padicabvcxp  27772  0cnop  32297  0cnfn  32298  rpdp2cl  33167  xdivpnfrp  33218  pnfinf  33469  hgt750lem2  35005  taupilem1  37931  itg2gt0cn  38292  areacirclem1  38325  areacirclem4  38328  prdstotbnd  38411  prdsbnd2  38412  aks4d1p1p6  42808  irrapxlem3  43521  xralrple2  46040  constlimc  46310  0cnv  46426  ioodvbdlimc1lem1  46615  fourierdlem103  46893  fourierdlem104  46894  etransclem18  46936  etransclem46  46964  hoidmvlelem3  47281