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

Theorem prn0 6839
Description: A positive real is not empty. (Revised by Mario Carneiro, 11-May-2013.)
Assertion
Ref Expression
prn0 |- (A e. P. -> A =/= (/))

Proof of Theorem prn0
StepHypRef Expression
1 elnpi 6838 . . 3 |- (A e. P. <-> ((A e. _V /\ (/) C. A /\ A C. Q.) /\ A.x e. A (A.y(y <Q x -> y e. A) /\ E.y e. A x <Q y)))
2 simpl2 968 . . 3 |- (((A e. _V /\ (/) C. A /\ A C. Q.) /\ A.x e. A (A.y(y <Q x -> y e. A) /\ E.y e. A x <Q y)) -> (/) C. A)
31, 2sylbi 200 . 2 |- (A e. P. -> (/) C. A)
4 0pss 2961 . 2 |- ((/) C. A <-> A =/= (/))
53, 4sylib 201 1 |- (A e. P. -> A =/= (/))
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 382   /\ w3a 946  A.wal 1375   e. wcel 1459   =/= wne 2078  A.wral 2169  E.wrex 2170  _Vcvv 2365   C. wpss 2663  (/)c0 2926   class class class wbr 3378  Q.cnq 6699   <Q cltq 6705  P.cnp 6706
This theorem is referenced by:  0npr 6842  npomex 6846  genpn0 6853  prlem934 6883  ltaddpr 6884  prlem936 6897  reclem2pr 6898  suplem1pr 6902
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1671  ax-ext 1942
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3an 948  df-ex 1381  df-sb 1633  df-clab 1948  df-cleq 1953  df-clel 1956  df-ne 2080  df-ral 2173  df-rex 2174  df-v 2367  df-dif 2665  df-in 2669  df-ss 2671  df-pss 2673  df-nul 2927  df-np 6831
Copyright terms: Public domain