Theorem rpregt0 13030

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2141   class class class wbr 5108  ℝcr 11098  0cc0 11099   < clt 11242  ℝ⁺crp 13015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-rp 13016

This theorem is referenced by:  rpne0  13032  divlt1lt  13086  divle1le  13087  ledivge1le  13088  nnledivrp  13129  modge0  13912  modlt  13913  modid  13929  modmuladdnn0  13951  expnlbnd  14269  o1fsum  15865  isprm6  16772  gexexlem  19921  lmnn  25401  aaliou2b  26481  harmonicbnd4  27151  logfaclbnd  27362  logfacrlim  27364  chto1ub  27616  vmadivsum  27622  dchrmusumlema  27633  dchrvmasumlem2  27638  dchrisum0lem2a  27657  dchrisum0lem2  27658  dchrisum0lem3  27659  mulogsumlem  27671  mulog2sumlem2  27675  selberg2lem  27690  selberg3lem1  27697  pntrmax  27704  pntrsumo1  27705  pntibndlem3  27732  divge1b  49259  divgt1b  49260