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

Metamath Proof Explorer

Theorem rpcndif0

Description: A positive real number is a complex number not being 0. (Contributed by AV, 29-May-2020)

		Ref	Expression
	Assertion	rpcndif0	$⊢ A \in ℝ^{+} \to A \in (ℂ ∖ \{0\})$

Step	Hyp	Ref	Expression
1		rpcnne0	$⊢ A \in ℝ^{+} \to (A \in ℂ \land A \neq 0)$
2		eldifsn	$⊢ A \in (ℂ ∖ \{0\}) \leftrightarrow (A \in ℂ \land A \neq 0)$
3	1 2	sylibr	$⊢ A \in ℝ^{+} \to A \in (ℂ ∖ \{0\})$