Theorem rpregt0 12973

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074  0cc0 11075   < clt 11215  ℝ⁺crp 12958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-rp 12959

This theorem is referenced by:  rpne0  12975  divlt1lt  13029  divle1le  13030  ledivge1le  13031  nnledivrp  13072  modge0  13848  modlt  13849  modid  13865  modmuladdnn0  13887  expnlbnd  14205  o1fsum  15786  isprm6  16691  gexexlem  19789  lmnn  25170  aaliou2b  26256  harmonicbnd4  26928  logfaclbnd  27140  logfacrlim  27142  chto1ub  27394  vmadivsum  27400  dchrmusumlema  27411  dchrvmasumlem2  27416  dchrisum0lem2a  27435  dchrisum0lem2  27436  dchrisum0lem3  27437  mulogsumlem  27449  mulog2sumlem2  27453  selberg2lem  27468  selberg3lem1  27475  pntrmax  27482  pntrsumo1  27483  pntibndlem3  27510  divge1b  48505  divgt1b  48506