Metamath Proof Explorer

Theorem 2picn

Description: ( 2 x. _pi ) is a complex number. (Contributed by Umit Teoman Dogan, 10-Jun-2026)

Ref Expression
Assertion 2picn 
|- ( 2 x. _pi ) e. CC

Proof

Step Hyp Ref Expression
1 2cn 
 |-  2 e. CC
2 picn 
 |-  _pi e. CC
3 1 2 mulcli 
 |-  ( 2 x. _pi ) e. CC