Theorem bj-pinftynrr

Description: The extended complex number pinfty is not a complex number. (Contributed by BJ, 27-Jun-2019)

	Ref	Expression
Assertion	bj-pinftynrr	⊢ ¬ +∞ ∈ ℂ

Proof

Step	Hyp	Ref	Expression
1		df-bj-pinfty	⊢ +∞ = ( +∞ei ‘ 0 )
2		bj-inftyexpidisj	⊢ ¬ ( +∞ei ‘ 0 ) ∈ ℂ
3	1 2	eqneltri	⊢ ¬ +∞ ∈ ℂ