Theorem rpregt0 12744

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   class class class wbr 5074  ℝcr 10870  0cc0 10871   < clt 11009  ℝ⁺crp 12730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-rp 12731

This theorem is referenced by:  rpne0  12746  divlt1lt  12799  divle1le  12800  ledivge1le  12801  nnledivrp  12842  modge0  13599  modlt  13600  modid  13616  modmuladdnn0  13635  expnlbnd  13948  o1fsum  15525  isprm6  16419  gexexlem  19453  lmnn  24427  aaliou2b  25501  harmonicbnd4  26160  logfaclbnd  26370  logfacrlim  26372  chto1ub  26624  vmadivsum  26630  dchrmusumlema  26641  dchrvmasumlem2  26646  dchrisum0lem2a  26665  dchrisum0lem2  26666  dchrisum0lem3  26667  mulogsumlem  26679  mulog2sumlem2  26683  selberg2lem  26698  selberg3lem1  26705  pntrmax  26712  pntrsumo1  26713  pntibndlem3  26740  divge1b  45853  divgt1b  45854