Theorem rpregt0 13105

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   class class class wbr 5102  ℝcr 11171  0cc0 11172   < clt 11315  ℝ⁺crp 13090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-rp 13091

This theorem is used by:  rpne0  13107  divlt1lt  13161  divle1le  13162  ledivge1le  13163  nnledivrp  13204  modge0  13988  modlt  13989  modid  14005  modmuladdnn0  14027  expnlbnd  14345  o1fsum  15948  isprm6  16853  gexexlem  20028  lmnn  25546  aaliou2b  26632  harmonicbnd4  27302  logfaclbnd  27513  logfacrlim  27515  chto1ub  27767  vmadivsum  27773  dchrmusumlema  27784  dchrvmasumlem2  27789  dchrisum0lem2a  27808  dchrisum0lem2  27809  dchrisum0lem3  27810  mulogsumlem  27822  mulog2sumlem2  27826  selberg2lem  27841  selberg3lem1  27848  pntrmax  27855  pntrsumo1  27856  pntibndlem3  27883  divge1b  49546  divgt1b  49547