Theorem rpregt0 12998

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2136   class class class wbr 5094  ℝcr 11062  0cc0 11063   < clt 11206  ℝ⁺crp 12983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-br 5095  df-rp 12984

This theorem is referenced by:  rpne0  13000  divlt1lt  13054  divle1le  13055  ledivge1le  13056  nnledivrp  13097  modge0  13879  modlt  13880  modid  13896  modmuladdnn0  13918  expnlbnd  14236  o1fsum  15817  isprm6  16725  gexexlem  19868  lmnn  25298  aaliou2b  26375  harmonicbnd4  27045  logfaclbnd  27256  logfacrlim  27258  chto1ub  27510  vmadivsum  27516  dchrmusumlema  27527  dchrvmasumlem2  27532  dchrisum0lem2a  27551  dchrisum0lem2  27552  dchrisum0lem3  27553  mulogsumlem  27565  mulog2sumlem2  27569  selberg2lem  27584  selberg3lem1  27591  pntrmax  27598  pntrsumo1  27599  pntibndlem3  27626  divge1b  49082  divgt1b  49083