Theorem rpregt0 12925

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5099  ℝcr 11030  0cc0 11031   < clt 11171  ℝ⁺crp 12910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-rp 12911

This theorem is referenced by:  rpne0  12927  divlt1lt  12981  divle1le  12982  ledivge1le  12983  nnledivrp  13024  modge0  13804  modlt  13805  modid  13821  modmuladdnn0  13843  expnlbnd  14161  o1fsum  15741  isprm6  16646  gexexlem  19786  lmnn  25224  aaliou2b  26310  harmonicbnd4  26982  logfaclbnd  27194  logfacrlim  27196  chto1ub  27448  vmadivsum  27454  dchrmusumlema  27465  dchrvmasumlem2  27470  dchrisum0lem2a  27489  dchrisum0lem2  27490  dchrisum0lem3  27491  mulogsumlem  27503  mulog2sumlem2  27507  selberg2lem  27522  selberg3lem1  27529  pntrmax  27536  pntrsumo1  27537  pntibndlem3  27564  divge1b  48835  divgt1b  48836