Theorem rpregt0 13022

Description: A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

Assertion

Ref	Expression
rpregt0	⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Proof of Theorem rpregt0

Step	Hyp	Ref	Expression
1		elrp 13009	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2	1	biimpi 219	1 ⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145   class class class wbr 5105  ℝcr 11087  0cc0 11088   < clt 11231  ℝ⁺crp 13007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-rp 13008

This theorem is referenced by:  rpne0  13024  divlt1lt  13078  divle1le  13079  ledivge1le  13080  nnledivrp  13121  modge0  13903  modlt  13904  modid  13920  modmuladdnn0  13942  expnlbnd  14260  o1fsum  15855  isprm6  16763  gexexlem  19913  lmnn  25383  aaliou2b  26463  harmonicbnd4  27133  logfaclbnd  27344  logfacrlim  27346  chto1ub  27598  vmadivsum  27604  dchrmusumlema  27615  dchrvmasumlem2  27620  dchrisum0lem2a  27639  dchrisum0lem2  27640  dchrisum0lem3  27641  mulogsumlem  27653  mulog2sumlem2  27657  selberg2lem  27672  selberg3lem1  27679  pntrmax  27686  pntrsumo1  27687  pntibndlem3  27714  divge1b  49143  divgt1b  49144