Theorem rpregt0 12966

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5107  ℝcr 11067  0cc0 11068   < clt 11208  ℝ⁺crp 12951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-rp 12952

This theorem is referenced by:  rpne0  12968  divlt1lt  13022  divle1le  13023  ledivge1le  13024  nnledivrp  13065  modge0  13841  modlt  13842  modid  13858  modmuladdnn0  13880  expnlbnd  14198  o1fsum  15779  isprm6  16684  gexexlem  19782  lmnn  25163  aaliou2b  26249  harmonicbnd4  26921  logfaclbnd  27133  logfacrlim  27135  chto1ub  27387  vmadivsum  27393  dchrmusumlema  27404  dchrvmasumlem2  27409  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0lem3  27430  mulogsumlem  27442  mulog2sumlem2  27446  selberg2lem  27461  selberg3lem1  27468  pntrmax  27475  pntrsumo1  27476  pntibndlem3  27503  divge1b  48501  divgt1b  48502