Description: The empty set is not a positive real. (Contributed by NM, 15-Nov-1995) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | 0npr | ⊢ ¬ ∅ ∈ P |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ∅ = ∅ | |
2 | prn0 | ⊢ ( ∅ ∈ P → ∅ ≠ ∅ ) | |
3 | 2 | necon2bi | ⊢ ( ∅ = ∅ → ¬ ∅ ∈ P ) |
4 | 1 3 | ax-mp | ⊢ ¬ ∅ ∈ P |