Theorem rpgt0 12930

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037  0cc0 11038   < clt 11178  ℝ⁺crp 12917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-rp 12918

This theorem is referenced by:  rpge0  12931  neglt  12937  rpgecl  12947  0nrp  12954  rpgt0d  12964  addlelt  13033  0mod  13834  sgnrrp  15026  01sqrexlem2  15178  01sqrexlem4  15180  01sqrexlem6  15182  resqrex  15185  rpsqrtcl  15199  climconst  15478  rlimconst  15479  divrcnv  15787  rprisefaccl  15958  blcntrps  24368  blcntr  24369  stdbdmet  24472  stdbdmopn  24474  prdsxmslem2  24485  metustid  24510  nmoix  24685  metdseq0  24811  lebnumii  24933  itgulm  26385  pilem2  26430  cos02pilt1  26503  tanregt0  26516  logdmnrp  26618  cxple2  26674  asinneg  26864  asin1  26872  reasinsin  26874  atanbndlem  26903  atanbnd  26904  atan1  26906  rlimcnp  26943  chtrpcl  27153  ppiltx  27155  bposlem8  27270  pntlem3  27588  padicabvcxp  27611  0cnop  32066  0cnfn  32067  rpdp2cl  32973  xdivpnfrp  33024  pnfinf  33276  hgt750lem2  34829  taupilem1  37565  itg2gt0cn  37915  areacirclem1  37948  areacirclem4  37951  prdstotbnd  38034  prdsbnd2  38035  aks4d1p1p6  42432  irrapxlem3  43170  xralrple2  45702  constlimc  45973  0cnv  46089  ioodvbdlimc1lem1  46278  fourierdlem103  46556  fourierdlem104  46557  etransclem18  46599  etransclem46  46627  hoidmvlelem3  46944