Theorem rpregt0 13050

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107   class class class wbr 5142  ℝcr 11155  0cc0 11156   < clt 11296  ℝ⁺crp 13035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-rp 13036

This theorem is referenced by:  rpne0  13052  divlt1lt  13105  divle1le  13106  ledivge1le  13107  nnledivrp  13148  modge0  13920  modlt  13921  modid  13937  modmuladdnn0  13957  expnlbnd  14273  o1fsum  15850  isprm6  16752  gexexlem  19871  lmnn  25298  aaliou2b  26384  harmonicbnd4  27055  logfaclbnd  27267  logfacrlim  27269  chto1ub  27521  vmadivsum  27527  dchrmusumlema  27538  dchrvmasumlem2  27543  dchrisum0lem2a  27562  dchrisum0lem2  27563  dchrisum0lem3  27564  mulogsumlem  27576  mulog2sumlem2  27580  selberg2lem  27595  selberg3lem1  27602  pntrmax  27609  pntrsumo1  27610  pntibndlem3  27637  divge1b  48434  divgt1b  48435