Theorem rpregt0 12926

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5095  ℝcr 11027  0cc0 11028   < clt 11168  ℝ⁺crp 12911

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-rp 12912

This theorem is referenced by:  rpne0  12928  divlt1lt  12982  divle1le  12983  ledivge1le  12984  nnledivrp  13025  modge0  13801  modlt  13802  modid  13818  modmuladdnn0  13840  expnlbnd  14158  o1fsum  15738  isprm6  16643  gexexlem  19749  lmnn  25179  aaliou2b  26265  harmonicbnd4  26937  logfaclbnd  27149  logfacrlim  27151  chto1ub  27403  vmadivsum  27409  dchrmusumlema  27420  dchrvmasumlem2  27425  dchrisum0lem2a  27444  dchrisum0lem2  27445  dchrisum0lem3  27446  mulogsumlem  27458  mulog2sumlem2  27462  selberg2lem  27477  selberg3lem1  27484  pntrmax  27491  pntrsumo1  27492  pntibndlem3  27519  divge1b  48485  divgt1b  48486