Theorem bj-minftynrr

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

	Ref	Expression
Assertion	bj-minftynrr	⊢ ¬ -∞ ∈ ℂ

Proof

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