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 =/= (/) )