Metamath Proof Explorer

Theorem brucn

Description: The basic N -th root of unity is a complex number. (Contributed by AV, 24-Oct-2026)

Ref Expression
Assertion brucn 
|- ( N e. NN -> ( bRoU ` N ) e. CC )

Proof

Step Hyp Ref Expression
1 bruval 
 |-  ( N e. NN -> ( bRoU ` N ) = ( exp ` ( ( 2 x. ( _pi x. _i ) ) / N ) ) )
2 2cn 
 |-  2 e. CC
3 picn 
 |-  _pi e. CC
4 ax-icn 
 |-  _i e. CC
5 3 4 mulcli 
 |-  ( _pi x. _i ) e. CC
6 2 5 mulcli 
 |-  ( 2 x. ( _pi x. _i ) ) e. CC
7 6 a1i 
 |-  ( N e. NN -> ( 2 x. ( _pi x. _i ) ) e. CC )
8 nncn 
 |-  ( N e. NN -> N e. CC )
9 nnne0 
 |-  ( N e. NN -> N =/= 0 )
10 7 8 9 divcld 
 |-  ( N e. NN -> ( ( 2 x. ( _pi x. _i ) ) / N ) e. CC )
11 10 efcld 
 |-  ( N e. NN -> ( exp ` ( ( 2 x. ( _pi x. _i ) ) / N ) ) e. CC )
12 1 11 eqeltrd 
 |-  ( N e. NN -> ( bRoU ` N ) e. CC )