Theorem rpregt0 12955

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   class class class wbr 5079  ℝcr 11035  0cc0 11036   < clt 11177  ℝ⁺crp 12940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-rp 12941

This theorem is referenced by:  rpne0  12957  divlt1lt  13011  divle1le  13012  ledivge1le  13013  nnledivrp  13054  modge0  13836  modlt  13837  modid  13853  modmuladdnn0  13875  expnlbnd  14193  o1fsum  15774  isprm6  16682  gexexlem  19825  lmnn  25255  aaliou2b  26332  harmonicbnd4  26999  logfaclbnd  27210  logfacrlim  27212  chto1ub  27464  vmadivsum  27470  dchrmusumlema  27481  dchrvmasumlem2  27486  dchrisum0lem2a  27505  dchrisum0lem2  27506  dchrisum0lem3  27507  mulogsumlem  27519  mulog2sumlem2  27523  selberg2lem  27538  selberg3lem1  27545  pntrmax  27552  pntrsumo1  27553  pntibndlem3  27580  divge1b  49004  divgt1b  49005