Theorem rpregt0 13059

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   class class class wbr 5107  ℝcr 11126  0cc0 11127   < clt 11270  ℝ⁺crp 13044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-rp 13045

This theorem is used by:  rpne0  13061  divlt1lt  13115  divle1le  13116  ledivge1le  13117  nnledivrp  13158  modge0  13942  modlt  13943  modid  13959  modmuladdnn0  13981  expnlbnd  14299  o1fsum  15902  isprm6  16809  gexexlem  19983  lmnn  25495  aaliou2b  26577  harmonicbnd4  27248  logfaclbnd  27459  logfacrlim  27461  chto1ub  27713  vmadivsum  27719  dchrmusumlema  27730  dchrvmasumlem2  27735  dchrisum0lem2a  27754  dchrisum0lem2  27755  dchrisum0lem3  27756  mulogsumlem  27768  mulog2sumlem2  27772  selberg2lem  27787  selberg3lem1  27794  pntrmax  27801  pntrsumo1  27802  pntibndlem3  27829  divge1b  49444  divgt1b  49445