Theorem rpcndif0

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

	Ref	Expression
Assertion	rpcndif0	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ( ℂ ∖ { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		rpcnne0	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
2		eldifsn	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
3	1 2	sylibr	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ( ℂ ∖ { 0 } ) )