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

Theorem prn0 6982
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 6981 . . 3
2 simpl2 920 . . 3
31, 2sylbi 184 . 2
4 0pss 2935 . 2
53, 4sylib 185 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 356   w3a 898  wal 1329   wcel 1415   wne 2034  wral 2125  wrex 2126  cvv 2322   wpss 2633  c0 2898   class class class wbr 3358  cnq 6842   cltq 6848  cnp 6849
This theorem is referenced by:  0npr 6985  npomex 6989  genpn0 6996  prlem934 7026  ltaddpr 7027  prlem936 7040  reclem2pr 7041  suplem1pr 7045
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3an 900  df-ex 1335  df-sb 1590  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-ral 2129  df-rex 2130  df-v 2324  df-dif 2635  df-in 2639  df-ss 2641  df-pss 2643  df-nul 2899  df-np 6974
Copyright terms: Public domain