Theorem rpregt0 12957

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ℝcr 11037  0cc0 11038   < clt 11179  ℝ⁺crp 12942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-rp 12943

This theorem is referenced by:  rpne0  12959  divlt1lt  13013  divle1le  13014  ledivge1le  13015  nnledivrp  13056  modge0  13838  modlt  13839  modid  13855  modmuladdnn0  13877  expnlbnd  14195  o1fsum  15776  isprm6  16684  gexexlem  19827  lmnn  25230  aaliou2b  26307  harmonicbnd4  26974  logfaclbnd  27185  logfacrlim  27187  chto1ub  27439  vmadivsum  27445  dchrmusumlema  27456  dchrvmasumlem2  27461  dchrisum0lem2a  27480  dchrisum0lem2  27481  dchrisum0lem3  27482  mulogsumlem  27494  mulog2sumlem2  27498  selberg2lem  27513  selberg3lem1  27520  pntrmax  27527  pntrsumo1  27528  pntibndlem3  27555  divge1b  48982  divgt1b  48983