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

Theorem prn0 6881
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 6880 . . 3
2 simpl2 934 . . 3
31, 2sylbi 185 . 2
4 0pss 2936 . 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 2635  c0 2899   class class class wbr 3358  cnq 6741   cltq 6747  cnp 6748
This theorem is referenced by:  0npr 6884  npomex 6888  genpn0 6895  prlem934 6925  ltaddpr 6926  prlem936 6939  reclem2pr 6940  suplem1pr 6944
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 2637  df-in 2641  df-ss 2643  df-pss 2645  df-nul 2900  df-np 6873
Copyright terms: Public domain