Theorem rpregt0 12404

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114   class class class wbr 5066  ℝcr 10536  0cc0 10537   < clt 10675  ℝ⁺crp 12390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-rp 12391

This theorem is referenced by:  rpne0  12406  divlt1lt  12459  divle1le  12460  ledivge1le  12461  nnledivrp  12502  modge0  13248  modlt  13249  modid  13265  modmuladdnn0  13284  expnlbnd  13595  o1fsum  15168  isprm6  16058  gexexlem  18972  lmnn  23866  aaliou2b  24930  harmonicbnd4  25588  logfaclbnd  25798  logfacrlim  25800  chto1ub  26052  vmadivsum  26058  dchrmusumlema  26069  dchrvmasumlem2  26074  dchrisum0lem2a  26093  dchrisum0lem2  26094  dchrisum0lem3  26095  mulogsumlem  26107  mulog2sumlem2  26111  selberg2lem  26126  selberg3lem1  26133  pntrmax  26140  pntrsumo1  26141  pntibndlem3  26168  divge1b  44587  divgt1b  44588