Metamath Proof Explorer

Theorem prn0

Description: A positive real is not empty. (Contributed by NM, 15-May-1996) (Revised by Mario Carneiro, 11-May-2013) (New usage is discouraged.)

Ref Expression
Assertion prn0 
|- ( A e. P. -> A =/= (/) )

Proof

Step Hyp Ref Expression
1 elnpi 
 |-  ( A e. P. <-> ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x
2 simpl2 
 |-  ( ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y  y e. A ) /\ E. y e. A x  (/) C. A )
3 1 2 sylbi 
 |-  ( A e. P. -> (/) C. A )
4 0pss 
 |-  ( (/) C. A <-> A =/= (/) )
5 3 4 sylib 
 |-  ( A e. P. -> A =/= (/) )