Theorem rpgt0 13021

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5119  ℝcr 11128  0cc0 11129   < clt 11269  ℝ⁺crp 13008

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-rp 13009

This theorem is referenced by:  rpge0  13022  rpgecl  13037  0nrp  13044  rpgt0d  13054  addlelt  13123  0mod  13919  sgnrrp  15110  01sqrexlem2  15262  01sqrexlem4  15264  01sqrexlem6  15266  resqrex  15269  rpsqrtcl  15283  climconst  15559  rlimconst  15560  divrcnv  15868  rprisefaccl  16039  blcntrps  24351  blcntr  24352  stdbdmet  24455  stdbdmopn  24457  prdsxmslem2  24468  metustid  24493  nmoix  24668  metdseq0  24794  lebnumii  24916  itgulm  26369  pilem2  26414  cos02pilt1  26487  tanregt0  26500  logdmnrp  26602  cxple2  26658  asinneg  26848  asin1  26856  reasinsin  26858  atanbndlem  26887  atanbnd  26888  atan1  26890  rlimcnp  26927  chtrpcl  27137  ppiltx  27139  bposlem8  27254  pntlem3  27572  padicabvcxp  27595  0cnop  31960  0cnfn  31961  rpdp2cl  32856  xdivpnfrp  32907  pnfinf  33181  hgt750lem2  34684  taupilem1  37339  itg2gt0cn  37699  areacirclem1  37732  areacirclem4  37735  prdstotbnd  37818  prdsbnd2  37819  aks4d1p1p6  42086  irrapxlem3  42847  neglt  45313  xralrple2  45381  constlimc  45653  0cnv  45771  ioodvbdlimc1lem1  45960  fourierdlem103  46238  fourierdlem104  46239  etransclem18  46281  etransclem46  46309  hoidmvlelem3  46626