Theorem rpregt0 12391

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111   class class class wbr 5030  ℝcr 10525  0cc0 10526   < clt 10664  ℝ⁺crp 12377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-rp 12378

This theorem is referenced by:  rpne0  12393  divlt1lt  12446  divle1le  12447  ledivge1le  12448  nnledivrp  12489  modge0  13242  modlt  13243  modid  13259  modmuladdnn0  13278  expnlbnd  13590  o1fsum  15160  isprm6  16048  gexexlem  18965  lmnn  23867  aaliou2b  24937  harmonicbnd4  25596  logfaclbnd  25806  logfacrlim  25808  chto1ub  26060  vmadivsum  26066  dchrmusumlema  26077  dchrvmasumlem2  26082  dchrisum0lem2a  26101  dchrisum0lem2  26102  dchrisum0lem3  26103  mulogsumlem  26115  mulog2sumlem2  26119  selberg2lem  26134  selberg3lem1  26141  pntrmax  26148  pntrsumo1  26149  pntibndlem3  26176  divge1b  44921  divgt1b  44922