This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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