Definition df-bj-minfty

Description: Definition of "minus infinity". (Contributed by BJ, 27-Jun-2019)

	Ref	Expression
Assertion	df-bj-minfty	⊢ -∞ = ( +∞ei ‘ π )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cminfty	⊢ -∞
1		cinftyexpi	⊢ +∞ei
2		cpi	⊢ π
3	2 1	cfv	⊢ ( +∞ei ‘ π )
4	0 3	wceq	⊢ -∞ = ( +∞ei ‘ π )