Theorem rpregt0 12673

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801  0cc0 10802   < clt 10940  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-rp 12660

This theorem is referenced by:  rpne0  12675  divlt1lt  12728  divle1le  12729  ledivge1le  12730  nnledivrp  12771  modge0  13527  modlt  13528  modid  13544  modmuladdnn0  13563  expnlbnd  13876  o1fsum  15453  isprm6  16347  gexexlem  19368  lmnn  24332  aaliou2b  25406  harmonicbnd4  26065  logfaclbnd  26275  logfacrlim  26277  chto1ub  26529  vmadivsum  26535  dchrmusumlema  26546  dchrvmasumlem2  26551  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrisum0lem3  26572  mulogsumlem  26584  mulog2sumlem2  26588  selberg2lem  26603  selberg3lem1  26610  pntrmax  26617  pntrsumo1  26618  pntibndlem3  26645  divge1b  45741  divgt1b  45742