Theorem rpregt0 13028

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098   class class class wbr 5149  ℝcr 11144  0cc0 11145   < clt 11285  ℝ⁺crp 13014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-rp 13015

This theorem is referenced by:  rpne0  13030  divlt1lt  13083  divle1le  13084  ledivge1le  13085  nnledivrp  13126  modge0  13885  modlt  13886  modid  13902  modmuladdnn0  13921  expnlbnd  14236  o1fsum  15800  isprm6  16693  gexexlem  19824  lmnn  25240  aaliou2b  26326  harmonicbnd4  26993  logfaclbnd  27205  logfacrlim  27207  chto1ub  27459  vmadivsum  27465  dchrmusumlema  27476  dchrvmasumlem2  27481  dchrisum0lem2a  27500  dchrisum0lem2  27501  dchrisum0lem3  27502  mulogsumlem  27514  mulog2sumlem2  27518  selberg2lem  27533  selberg3lem1  27540  pntrmax  27547  pntrsumo1  27548  pntibndlem3  27575  divge1b  47768  divgt1b  47769