Theorem rpregt0 13031

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107   class class class wbr 5123  ℝcr 11136  0cc0 11137   < clt 11277  ℝ⁺crp 13016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5124  df-rp 13017

This theorem is referenced by:  rpne0  13033  divlt1lt  13086  divle1le  13087  ledivge1le  13088  nnledivrp  13129  modge0  13901  modlt  13902  modid  13918  modmuladdnn0  13938  expnlbnd  14254  o1fsum  15831  isprm6  16733  gexexlem  19838  lmnn  25233  aaliou2b  26319  harmonicbnd4  26990  logfaclbnd  27202  logfacrlim  27204  chto1ub  27456  vmadivsum  27462  dchrmusumlema  27473  dchrvmasumlem2  27478  dchrisum0lem2a  27497  dchrisum0lem2  27498  dchrisum0lem3  27499  mulogsumlem  27511  mulog2sumlem2  27515  selberg2lem  27530  selberg3lem1  27537  pntrmax  27544  pntrsumo1  27545  pntibndlem3  27572  divge1b  48387  divgt1b  48388