Theorem rpregt0 12946

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ℝcr 11026  0cc0 11027   < clt 11168  ℝ⁺crp 12931

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-rp 12932

This theorem is referenced by:  rpne0  12948  divlt1lt  13002  divle1le  13003  ledivge1le  13004  nnledivrp  13045  modge0  13827  modlt  13828  modid  13844  modmuladdnn0  13866  expnlbnd  14184  o1fsum  15765  isprm6  16673  gexexlem  19816  lmnn  25239  aaliou2b  26320  harmonicbnd4  26992  logfaclbnd  27204  logfacrlim  27206  chto1ub  27458  vmadivsum  27464  dchrmusumlema  27475  dchrvmasumlem2  27480  dchrisum0lem2a  27499  dchrisum0lem2  27500  dchrisum0lem3  27501  mulogsumlem  27513  mulog2sumlem2  27517  selberg2lem  27532  selberg3lem1  27539  pntrmax  27546  pntrsumo1  27547  pntibndlem3  27574  divge1b  48985  divgt1b  48986