Theorem rpregt0 13162

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   class class class wbr 5106  ℝcr 11226  0cc0 11227   < clt 11370  ℝ⁺crp 13147

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-rp 13148

This theorem is used by:  rpne0  13164  divlt1lt  13218  divle1le  13219  ledivge1le  13220  nnledivrp  13261  modge0  14046  modlt  14047  modid  14063  modmuladdnn0  14085  expnlbnd  14404  o1fsum  16009  isprm6  16919  gexexlem  20096  lmnn  25614  aaliou2b  26698  harmonicbnd4  27368  logfaclbnd  27579  logfacrlim  27581  chto1ub  27833  vmadivsum  27839  dchrmusumlema  27850  dchrvmasumlem2  27855  dchrisum0lem2a  27874  dchrisum0lem2  27875  dchrisum0lem3  27876  mulogsumlem  27888  mulog2sumlem2  27892  selberg2lem  27907  selberg3lem1  27914  pntrmax  27921  pntrsumo1  27922  pntibndlem3  27949  divge1b  49829  divgt1b  49830