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

Theorem prn0 7087
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 7086 . . 3
2 simpl2 921 . . 3
31, 2sylbi 185 . 2
4 0pss 2941 . 2
53, 4sylib 186 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   w3a 899  wal 1330   wcel 1416   wne 2035  wral 2127  wrex 2128  cvv 2326   wpss 2637  c0 2904   class class class wbr 3383  cnq 6947   cltq 6953  cnp 6954
This theorem is referenced by:  0npr 7090  npomex 7094  genpn0 7101  prlem934 7131  ltaddpr 7132  prlem936 7145  reclem2pr 7146  suplem1pr 7150
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1336  df-sb 1591  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-ral 2131  df-rex 2132  df-v 2328  df-dif 2639  df-in 2643  df-ss 2647  df-pss 2649  df-nul 2905  df-np 7079
Copyright terms: Public domain