Theorem rpgt0 13044

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

Syntax hints:   → wi 4   ∈ wcel 2105   class class class wbr 5147  ℝcr 11151  0cc0 11152   < clt 11292  ℝ⁺crp 13031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-rp 13032

This theorem is referenced by:  rpge0  13045  rpgecl  13060  0nrp  13067  rpgt0d  13077  addlelt  13146  0mod  13938  sgnrrp  15126  01sqrexlem2  15278  01sqrexlem4  15280  01sqrexlem6  15282  resqrex  15285  rpsqrtcl  15299  climconst  15575  rlimconst  15576  divrcnv  15884  rprisefaccl  16055  blcntrps  24437  blcntr  24438  stdbdmet  24544  stdbdmopn  24546  prdsxmslem2  24557  metustid  24582  nmoix  24765  metdseq0  24889  lebnumii  25011  itgulm  26465  pilem2  26510  cos02pilt1  26582  tanregt0  26595  logdmnrp  26697  cxple2  26753  asinneg  26943  asin1  26951  reasinsin  26953  atanbndlem  26982  atanbnd  26983  atan1  26985  rlimcnp  27022  chtrpcl  27232  ppiltx  27234  bposlem8  27349  pntlem3  27667  padicabvcxp  27690  0cnop  32007  0cnfn  32008  rpdp2cl  32848  xdivpnfrp  32899  pnfinf  33172  hgt750lem2  34645  taupilem1  37303  itg2gt0cn  37661  areacirclem1  37694  areacirclem4  37697  prdstotbnd  37780  prdsbnd2  37781  aks4d1p1p6  42054  irrapxlem3  42811  neglt  45234  xralrple2  45303  constlimc  45579  0cnv  45697  ioodvbdlimc1lem1  45886  fourierdlem103  46164  fourierdlem104  46165  etransclem18  46207  etransclem46  46235  hoidmvlelem3  46552