Theorem rpregt0 13028

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5124  ℝcr 11133  0cc0 11134   < clt 11274  ℝ⁺crp 13013

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  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 5125  df-rp 13014

This theorem is referenced by:  rpne0  13030  divlt1lt  13083  divle1le  13084  ledivge1le  13085  nnledivrp  13126  modge0  13901  modlt  13902  modid  13918  modmuladdnn0  13938  expnlbnd  14256  o1fsum  15834  isprm6  16738  gexexlem  19838  lmnn  25220  aaliou2b  26306  harmonicbnd4  26978  logfaclbnd  27190  logfacrlim  27192  chto1ub  27444  vmadivsum  27450  dchrmusumlema  27461  dchrvmasumlem2  27466  dchrisum0lem2a  27485  dchrisum0lem2  27486  dchrisum0lem3  27487  mulogsumlem  27499  mulog2sumlem2  27503  selberg2lem  27518  selberg3lem1  27525  pntrmax  27532  pntrsumo1  27533  pntibndlem3  27560  divge1b  48468  divgt1b  48469