Metamath Proof Explorer

Theorem bruval2

Description: An alternate way to express the basic N -th root of unity, see cxpeq . (Contributed by AV, 24-Oct-2026)

Ref Expression
Assertion bruval2 
|- ( N e. NN -> ( bRoU ` N ) = ( -u 1 ^c ( 2 / N ) ) )

Proof

Step Hyp Ref Expression
1 2cn 
 |-  2 e. CC
2 1 a1i 
 |-  ( N e. NN -> 2 e. CC )
3 picn 
 |-  _pi e. CC
4 ax-icn 
 |-  _i e. CC
5 3 4 mulcli 
 |-  ( _pi x. _i ) e. CC
6 5 a1i 
 |-  ( N e. NN -> ( _pi x. _i ) e. CC )
7 nncn 
 |-  ( N e. NN -> N e. CC )
8 nnne0 
 |-  ( N e. NN -> N =/= 0 )
9 2 6 7 8 div23d 
 |-  ( N e. NN -> ( ( 2 x. ( _pi x. _i ) ) / N ) = ( ( 2 / N ) x. ( _pi x. _i ) ) )
10 logm1 
 |-  ( log ` -u 1 ) = ( _i x. _pi )
11 4 3 mulcomi 
 |-  ( _i x. _pi ) = ( _pi x. _i )
12 10 11 eqtr2i 
 |-  ( _pi x. _i ) = ( log ` -u 1 )
13 12 a1i 
 |-  ( N e. NN -> ( _pi x. _i ) = ( log ` -u 1 ) )
14 13 oveq2d 
 |-  ( N e. NN -> ( ( 2 / N ) x. ( _pi x. _i ) ) = ( ( 2 / N ) x. ( log ` -u 1 ) ) )
15 9 14 eqtrd 
 |-  ( N e. NN -> ( ( 2 x. ( _pi x. _i ) ) / N ) = ( ( 2 / N ) x. ( log ` -u 1 ) ) )
16 15 fveq2d 
 |-  ( N e. NN -> ( exp ` ( ( 2 x. ( _pi x. _i ) ) / N ) ) = ( exp ` ( ( 2 / N ) x. ( log ` -u 1 ) ) ) )
17 bruval 
 |-  ( N e. NN -> ( bRoU ` N ) = ( exp ` ( ( 2 x. ( _pi x. _i ) ) / N ) ) )
18 neg1cn 
 |-  -u 1 e. CC
19 18 a1i 
 |-  ( N e. NN -> -u 1 e. CC )
20 neg1ne0 
 |-  -u 1 =/= 0
21 20 a1i 
 |-  ( N e. NN -> -u 1 =/= 0 )
22 2 7 8 divcld 
 |-  ( N e. NN -> ( 2 / N ) e. CC )
23 19 21 22 cxpefd 
 |-  ( N e. NN -> ( -u 1 ^c ( 2 / N ) ) = ( exp ` ( ( 2 / N ) x. ( log ` -u 1 ) ) ) )
24 16 17 23 3eqtr4d 
 |-  ( N e. NN -> ( bRoU ` N ) = ( -u 1 ^c ( 2 / N ) ) )