Theorem rpregt0 12924

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5099  ℝcr 11029  0cc0 11030   < clt 11170  ℝ⁺crp 12909

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-rp 12910

This theorem is referenced by:  rpne0  12926  divlt1lt  12980  divle1le  12981  ledivge1le  12982  nnledivrp  13023  modge0  13803  modlt  13804  modid  13820  modmuladdnn0  13842  expnlbnd  14160  o1fsum  15740  isprm6  16645  gexexlem  19785  lmnn  25223  aaliou2b  26309  harmonicbnd4  26981  logfaclbnd  27193  logfacrlim  27195  chto1ub  27447  vmadivsum  27453  dchrmusumlema  27464  dchrvmasumlem2  27469  dchrisum0lem2a  27488  dchrisum0lem2  27489  dchrisum0lem3  27490  mulogsumlem  27502  mulog2sumlem2  27506  selberg2lem  27521  selberg3lem1  27528  pntrmax  27535  pntrsumo1  27536  pntibndlem3  27563  divge1b  48794  divgt1b  48795