MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rpregt0 Structured version   Unicode version

Theorem rpregt0 11222
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  |-  ( A  e.  RR+  ->  ( A  e.  RR  /\  0  <  A ) )

Proof of Theorem rpregt0
StepHypRef Expression
1 elrp 11211 . 2  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
21biimpi 194 1  |-  ( A  e.  RR+  ->  ( A  e.  RR  /\  0  <  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1762   class class class wbr 4440   RRcr 9480   0cc0 9481    < clt 9617   RR+crp 11209
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-rp 11210
This theorem is referenced by:  rpne0  11224  modge0  11961  modlt  11962  modid  11976  expnlbnd  12251  o1fsum  13576  isprm6  14098  gexexlem  16644  lmnn  21430  aaliou2b  22464  harmonicbnd4  23061  logfaclbnd  23218  logfacrlim  23220  chto1ub  23382  vmadivsum  23388  dchrmusumlema  23399  dchrvmasumlem2  23404  dchrisum0lem2a  23423  dchrisum0lem2  23424  dchrisum0lem3  23425  mulogsumlem  23437  mulog2sumlem2  23441  selberg2lem  23456  selberg3lem1  23463  pntrmax  23470  pntrsumo1  23471  pntibndlem3  23498
  Copyright terms: Public domain W3C validator