ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rpregt0d Unicode version

Theorem rpregt0d 9516
Description: A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1  |-  ( ph  ->  A  e.  RR+ )
Assertion
Ref Expression
rpregt0d  |-  ( ph  ->  ( A  e.  RR  /\  0  <  A ) )

Proof of Theorem rpregt0d
StepHypRef Expression
1 rpred.1 . . 3  |-  ( ph  ->  A  e.  RR+ )
21rpred 9509 . 2  |-  ( ph  ->  A  e.  RR )
31rpgt0d 9512 . 2  |-  ( ph  ->  0  <  A )
42, 3jca 304 1  |-  ( ph  ->  ( A  e.  RR  /\  0  <  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 1481   class class class wbr 3933   RRcr 7639   0cc0 7640    < clt 7820   RR+crp 9466
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rab 2426  df-v 2689  df-un 3076  df-in 3078  df-ss 3085  df-sn 3534  df-pr 3535  df-op 3537  df-br 3934  df-rp 9467
This theorem is referenced by:  reclt1d  9523  recgt1d  9524  ltrecd  9528  lerecd  9529  ltrec1d  9530  lerec2d  9531  lediv2ad  9532  ltdiv2d  9533  lediv2d  9534  ledivdivd  9535  divge0d  9550  ltmul1d  9551  ltmul2d  9552  lemul1d  9553  lemul2d  9554  ltdiv1d  9555  lediv1d  9556  ltmuldivd  9557  ltmuldiv2d  9558  lemuldivd  9559  lemuldiv2d  9560  ltdivmuld  9561  ltdivmul2d  9562  ledivmuld  9563  ledivmul2d  9564  ltdiv23d  9570  lediv23d  9571  lt2mul2divd  9578  mertenslemi1  11332  isprm6  11852
  Copyright terms: Public domain W3C validator