Theorem rpregt0 12988

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   class class class wbr 5149  ℝcr 11109  0cc0 11110   < clt 11248  ℝ⁺crp 12974

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-rp 12975

This theorem is referenced by:  rpne0  12990  divlt1lt  13043  divle1le  13044  ledivge1le  13045  nnledivrp  13086  modge0  13844  modlt  13845  modid  13861  modmuladdnn0  13880  expnlbnd  14196  o1fsum  15759  isprm6  16651  gexexlem  19720  lmnn  24780  aaliou2b  25854  harmonicbnd4  26515  logfaclbnd  26725  logfacrlim  26727  chto1ub  26979  vmadivsum  26985  dchrmusumlema  26996  dchrvmasumlem2  27001  dchrisum0lem2a  27020  dchrisum0lem2  27021  dchrisum0lem3  27022  mulogsumlem  27034  mulog2sumlem2  27038  selberg2lem  27053  selberg3lem1  27060  pntrmax  27067  pntrsumo1  27068  pntibndlem3  27095  divge1b  47193  divgt1b  47194