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𝑷A

Proof

Step Hyp Ref Expression
1 elnpi A𝑷AVAA𝑸xAyy<𝑸xyAyAx<𝑸y
2 simpl2 AVAA𝑸xAyy<𝑸xyAyAx<𝑸yA
3 1 2 sylbi A𝑷A
4 0pss AA
5 3 4 sylib A𝑷A