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

Theorem prn0 6859
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 6858 . . 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 937 . . 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 185 . 2 |- (A e. P. -> (/) C. A)
4 0pss 2935 . 2 |- ((/) C. A <-> A =/= (/))
53, 4sylib 186 1 |- (A e. P. -> A =/= (/))
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 357   /\ w3a 915  A.wal 1344   e. wcel 1430   =/= wne 2050  A.wral 2141  E.wrex 2142  _Vcvv 2337   C. wpss 2637  (/)c0 2900   class class class wbr 3354  Q.cnq 6719   <Q cltq 6725  P.cnp 6726
This theorem is referenced by:  0npr 6862  npomex 6866  genpn0 6873  prlem934 6903  ltaddpr 6904  prlem936 6917  reclem2pr 6918  suplem1pr 6922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1345  ax-6 1346  ax-7 1347  ax-gen 1348  ax-8 1432  ax-10 1433  ax-11 1434  ax-12 1435  ax-17 1444  ax-9 1459  ax-4 1465  ax-16 1643  ax-ext 1914
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 917  df-ex 1350  df-sb 1605  df-clab 1920  df-cleq 1925  df-clel 1928  df-ne 2052  df-ral 2145  df-rex 2146  df-v 2339  df-dif 2639  df-in 2643  df-ss 2645  df-pss 2647  df-nul 2901  df-np 6851
Copyright terms: Public domain