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	$$⊢\neg \varnothing \in 𝑷$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\varnothing =\varnothing$$
2		prn0	$$⊢\varnothing \in 𝑷\to \varnothing \ne \varnothing$$
3	2	necon2bi	$$⊢\varnothing =\varnothing \to \neg \varnothing \in 𝑷$$
4	1 3	ax-mp	$$⊢\neg \varnothing \in 𝑷$$