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.