Theorem rpregt0 12135

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

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2164   class class class wbr 4875  ℝcr 10258  0cc0 10259   < clt 10398  ℝ⁺crp 12119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-br 4876  df-rp 12120

This theorem is referenced by:  rpne0  12137  divlt1lt  12190  divle1le  12191  ledivge1le  12192  nnledivrp  12233  modge0  12980  modlt  12981  modid  12997  modmuladdnn0  13016  expnlbnd  13295  o1fsum  14926  isprm6  15804  gexexlem  18615  lmnn  23438  aaliou2b  24502  harmonicbnd4  25157  logfaclbnd  25367  logfacrlim  25369  chto1ub  25585  vmadivsum  25591  dchrmusumlema  25602  dchrvmasumlem2  25607  dchrisum0lem2a  25626  dchrisum0lem2  25627  dchrisum0lem3  25628  mulogsumlem  25640  mulog2sumlem2  25644  selberg2lem  25659  selberg3lem1  25666  pntrmax  25673  pntrsumo1  25674  pntibndlem3  25701  divge1b  43163  divgt1b  43164