Theorem rpgt0 13134

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  ℝcr 11200  0cc0 11201   < clt 11344  ℝ⁺crp 13121

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-rp 13122

This theorem is used by:  rpge0  13135  neglt  13141  rpgecl  13151  0nrp  13158  rpgt0d  13168  addlelt  13237  0mod  14043  sgnrrp  15245  01sqrexlem2  15411  01sqrexlem4  15413  01sqrexlem6  15415  resqrex  15418  rpsqrtcl  15432  climconst  15711  rlimconst  15712  divrcnv  16022  rprisefaccl  16191  blcntrps  24732  blcntr  24733  stdbdmet  24836  stdbdmopn  24838  prdsxmslem2  24849  metustid  24874  nmoix  25049  metdseq0  25175  lebnumii  25288  itgulm  26736  pilem2  26780  cos02pilt1  26855  tanregt0  26868  logdmnrp  26970  cxple2  27026  asinneg  27215  asin1  27223  reasinsin  27225  atanbndlem  27254  atanbnd  27255  atan1  27257  rlimcnp  27294  chtrpcl  27503  ppiltx  27505  bposlem8  27619  pntlem3  27937  padicabvcxp  27960  0cnop  32582  0cnfn  32583  rpdp2cl  33491  xdivpnfrp  33542  pnfinf  33787  hgt750lem2  35324  taupilem1  38318  itg2gt0cn  38669  areacirclem1  38702  areacirclem4  38705  prdstotbnd  38804  prdsbnd2  38805  aks4d1p1p6  43199  irrapxlem3  43907  xralrple2  46442  constlimc  46712  0cnv  46828  ioodvbdlimc1lem1  47017  fourierdlem103  47295  fourierdlem104  47296  etransclem18  47338  etransclem46  47366  hoidmvlelem3  47683