Theorem rpgt0 12996

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

Syntax hints:   → wi 4   ∈ wcel 2136   class class class wbr 5094  ℝcr 11062  0cc0 11063   < clt 11206  ℝ⁺crp 12983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-br 5095  df-rp 12984

This theorem is referenced by:  rpge0  12997  neglt  13003  rpgecl  13013  0nrp  13020  rpgt0d  13030  addlelt  13099  0mod  13902  sgnrrp  15094  01sqrexlem2  15246  01sqrexlem4  15248  01sqrexlem6  15250  resqrex  15253  rpsqrtcl  15267  climconst  15546  rlimconst  15547  divrcnv  15858  rprisefaccl  16029  blcntrps  24445  blcntr  24446  stdbdmet  24549  stdbdmopn  24551  prdsxmslem2  24562  metustid  24587  nmoix  24762  metdseq0  24888  lebnumii  25001  itgulm  26441  pilem2  26485  cos02pilt1  26561  tanregt0  26574  logdmnrp  26676  cxple2  26732  asinneg  26921  asin1  26929  reasinsin  26931  atanbndlem  26960  atanbnd  26961  atan1  26963  rlimcnp  27000  chtrpcl  27209  ppiltx  27211  bposlem8  27325  pntlem3  27643  padicabvcxp  27666  0cnop  32121  0cnfn  32122  rpdp2cl  33013  xdivpnfrp  33064  pnfinf  33317  hgt750lem2  34903  taupilem1  37761  itg2gt0cn  38122  areacirclem1  38155  areacirclem4  38158  prdstotbnd  38241  prdsbnd2  38242  aks4d1p1p6  42638  irrapxlem3  43349  xralrple2  45878  constlimc  46148  0cnv  46264  ioodvbdlimc1lem1  46453  fourierdlem103  46731  fourierdlem104  46732  etransclem18  46774  etransclem46  46802  hoidmvlelem3  47119