HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem prn0 7783
Description: A positive real is not empty. (Revised by Mario Carneiro, 11-May-2013.)
Assertion
Ref Expression
prn0

Proof of Theorem prn0
StepHypRef Expression
1 elnpi 7782 . . 3
2 simpl2 921 . . 3
31, 2sylbi 185 . 2
4 0pss 3062 . 2
53, 4sylib 186 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   w3a 899  wal 1442   wcel 1528   wne 2147  wral 2239  wrex 2240  cvv 2440   wpss 2751  c0 3025   class class class wbr 3531  cnq 7643   cltq 7649  cnp 7650
This theorem is referenced by:  0npr 7786  npomex 7790  genpn0 7797  prlem934 7827  ltaddpr 7828  prlem936 7841  reclem2pr 7842  suplem1pr 7846
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1448  df-sb 1703  df-clab 2018  df-cleq 2023  df-clel 2026  df-ne 2149  df-ral 2243  df-rex 2244  df-v 2442  df-dif 2753  df-in 2757  df-ss 2761  df-pss 2763  df-nul 3026  df-np 7775
Copyright terms: Public domain