Theorem rpgt0 12913

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5095  ℝcr 11015  0cc0 11016   < clt 11156  ℝ⁺crp 12900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-rp 12901

This theorem is referenced by:  rpge0  12914  neglt  12920  rpgecl  12930  0nrp  12937  rpgt0d  12947  addlelt  13016  0mod  13816  sgnrrp  15008  01sqrexlem2  15160  01sqrexlem4  15162  01sqrexlem6  15164  resqrex  15167  rpsqrtcl  15181  climconst  15460  rlimconst  15461  divrcnv  15769  rprisefaccl  15940  blcntrps  24337  blcntr  24338  stdbdmet  24441  stdbdmopn  24443  prdsxmslem2  24454  metustid  24479  nmoix  24654  metdseq0  24780  lebnumii  24902  itgulm  26354  pilem2  26399  cos02pilt1  26472  tanregt0  26485  logdmnrp  26587  cxple2  26643  asinneg  26833  asin1  26841  reasinsin  26843  atanbndlem  26872  atanbnd  26873  atan1  26875  rlimcnp  26912  chtrpcl  27122  ppiltx  27124  bposlem8  27239  pntlem3  27557  padicabvcxp  27580  0cnop  31970  0cnfn  31971  rpdp2cl  32873  xdivpnfrp  32924  pnfinf  33163  hgt750lem2  34676  taupilem1  37376  itg2gt0cn  37725  areacirclem1  37758  areacirclem4  37761  prdstotbnd  37844  prdsbnd2  37845  aks4d1p1p6  42176  irrapxlem3  42931  xralrple2  45467  constlimc  45738  0cnv  45854  ioodvbdlimc1lem1  46043  fourierdlem103  46321  fourierdlem104  46322  etransclem18  46364  etransclem46  46392  hoidmvlelem3  46709