Theorem rpregt0 12915

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ 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:  rpne0  12917  divlt1lt  12971  divle1le  12972  ledivge1le  12973  nnledivrp  13014  modge0  13793  modlt  13794  modid  13810  modmuladdnn0  13832  expnlbnd  14150  o1fsum  15730  isprm6  16635  gexexlem  19774  lmnn  25200  aaliou2b  26286  harmonicbnd4  26958  logfaclbnd  27170  logfacrlim  27172  chto1ub  27424  vmadivsum  27430  dchrmusumlema  27441  dchrvmasumlem2  27446  dchrisum0lem2a  27465  dchrisum0lem2  27466  dchrisum0lem3  27467  mulogsumlem  27479  mulog2sumlem2  27483  selberg2lem  27498  selberg3lem1  27505  pntrmax  27512  pntrsumo1  27513  pntibndlem3  27540  divge1b  48627  divgt1b  48628