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

Theorem prn0 6897
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 6896 . . 3
2 simpl2 934 . . 3
31, 2sylbi 185 . 2
4 0pss 2940 . 2
53, 4sylib 186 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 360   w3a 912  wal 1341   wcel 1427   wne 2047  wral 2138  wrex 2139  cvv 2335   wpss 2639  c0 2903   class class class wbr 3362  cnq 6757   cltq 6763  cnp 6764
This theorem is referenced by:  0npr 6900  npomex 6904  genpn0 6911  prlem934 6941  ltaddpr 6942  prlem936 6955  reclem2pr 6956  suplem1pr 6960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3an 914  df-ex 1347  df-sb 1602  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-ral 2142  df-rex 2143  df-v 2337  df-dif 2641  df-in 2645  df-ss 2647  df-pss 2649  df-nul 2904  df-np 6889
Copyright terms: Public domain