Metamath Proof Explorer

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 
|- -. minfty e. CC

Proof

Step Hyp Ref Expression
1 df-bj-minfty 
 |-  minfty = ( inftyexpi ` _pi )
2 bj-inftyexpidisj 
 |-  -. ( inftyexpi ` _pi ) e. CC
3 1 2 eqneltri 
 |-  -. minfty e. CC