Metamath Proof Explorer

Theorem picn

Description: _pi is a complex number. (Contributed by David A. Wheeler, 6-Dec-2018)

Ref Expression
Assertion picn 
|- _pi e. CC

Proof

Step Hyp Ref Expression
1 pire 
 |-  _pi e. RR
2 1 recni 
 |-  _pi e. CC