Metamath Proof Explorer

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

Proof

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