Theorem rpregt0 13136

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   class class class wbr 5102  ℝcr 11200  0cc0 11201   < clt 11344  ℝ⁺crp 13121

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-rp 13122

This theorem is used by:  rpne0  13138  divlt1lt  13192  divle1le  13193  ledivge1le  13194  nnledivrp  13235  modge0  14020  modlt  14021  modid  14037  modmuladdnn0  14059  expnlbnd  14378  o1fsum  15981  isprm6  16891  gexexlem  20067  lmnn  25585  aaliou2b  26669  harmonicbnd4  27339  logfaclbnd  27550  logfacrlim  27552  chto1ub  27804  vmadivsum  27810  dchrmusumlema  27821  dchrvmasumlem2  27826  dchrisum0lem2a  27845  dchrisum0lem2  27846  dchrisum0lem3  27847  mulogsumlem  27859  mulog2sumlem2  27863  selberg2lem  27878  selberg3lem1  27885  pntrmax  27892  pntrsumo1  27893  pntibndlem3  27920  divge1b  49700  divgt1b  49701