Metamath Proof Explorer


Theorem 0npr

Description: The empty set is not a positive real. (Contributed by NM, 15-Nov-1995) (New usage is discouraged.)

Ref Expression
Assertion 0npr
|- -. (/) e. P.

Proof

Step Hyp Ref Expression
1 eqid
 |-  (/) = (/)
2 prn0
 |-  ( (/) e. P. -> (/) =/= (/) )
3 2 necon2bi
 |-  ( (/) = (/) -> -. (/) e. P. )
4 1 3 ax-mp
 |-  -. (/) e. P.