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

Theorem prn0 7937
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 7936 . . 3
2 simpl2 921 . . 3
31, 2sylbi 185 . 2
4 0pss 3122 . 2
53, 4sylib 186 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   w3a 899  wal 1445   wcel 1533   wne 2207  wral 2299  wrex 2300  cvv 2500   wpss 2811  c0 3085   class class class wbr 3591  cnq 7798   cltq 7804  cnp 7805
This theorem is referenced by:  0npr  7940  npomex  7944  genpn0  7951  prlem934  7981  ltaddpr  7982  prlem936  7995  reclem2pr  7996  suplem1pr  8000
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1451  df-sb 1751  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-ral 2303  df-rex 2304  df-v 2502  df-dif 2813  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3086  df-np 7929
Copyright terms: Public domain