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

Theorem prn0 6964
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 6963 . . 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 1040 . . 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 214 . 2 |- (A e. P. -> (/) C. A)
4 0pss 3082 . 2 |- ((/) C. A <-> A =/= (/))
53, 4sylib 215 1 |- (A e. P. -> A =/= (/))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 412   /\ w3a 1018  A.wal 1496   e. wcel 1575   =/= wne 2201  A.wral 2293  E.wrex 2294  _Vcvv 2482   C. wpss 2785  (/)c0 3048   class class class wbr 3492  Q.cnq 6824   <Q cltq 6830  P.cnp 6831
This theorem is referenced by:  0npr 6967  npomex 6971  genpn0 6978  prlem934 7008  ltaddpr 7009  prlem936 7022  reclem2pr 7023  suplem1pr 7027
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1497  ax-6 1498  ax-7 1499  ax-gen 1500  ax-8 1577  ax-10 1578  ax-11 1579  ax-12 1580  ax-17 1589  ax-9 1603  ax-4 1609  ax-16 1786  ax-ext 2057
This theorem depends on definitions:  df-bi 204  df-or 413  df-an 414  df-3an 1020  df-ex 1502  df-sb 1748  df-clab 2063  df-cleq 2068  df-clel 2071  df-ne 2203  df-ral 2297  df-rex 2298  df-v 2484  df-dif 2787  df-in 2791  df-ss 2793  df-pss 2795  df-nul 3049  df-np 6956
Copyright terms: Public domain