Metamath Proof Explorer

Theorem bruval3

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

Ref Expression
Assertion bruval3 
|- ( N e. NN -> ( bRoU ` N ) = ( ( cos ` ( ( 2 x. _pi ) / N ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / N ) ) ) ) )

Proof

Step Hyp Ref Expression
1 bruval 
 |-  ( N e. NN -> ( bRoU ` N ) = ( exp ` ( ( 2 x. ( _pi x. _i ) ) / N ) ) )
2 picn 
 |-  _pi e. CC
3 ax-icn 
 |-  _i e. CC
4 2 3 mulcomi 
 |-  ( _pi x. _i ) = ( _i x. _pi )
5 4 a1i 
 |-  ( N e. NN -> ( _pi x. _i ) = ( _i x. _pi ) )
6 5 oveq2d 
 |-  ( N e. NN -> ( 2 x. ( _pi x. _i ) ) = ( 2 x. ( _i x. _pi ) ) )
7 2cnd 
 |-  ( N e. NN -> 2 e. CC )
8 3 a1i 
 |-  ( N e. NN -> _i e. CC )
9 2 a1i 
 |-  ( N e. NN -> _pi e. CC )
10 7 8 9 mul12d 
 |-  ( N e. NN -> ( 2 x. ( _i x. _pi ) ) = ( _i x. ( 2 x. _pi ) ) )
11 6 10 eqtrd 
 |-  ( N e. NN -> ( 2 x. ( _pi x. _i ) ) = ( _i x. ( 2 x. _pi ) ) )
12 11 oveq1d 
 |-  ( N e. NN -> ( ( 2 x. ( _pi x. _i ) ) / N ) = ( ( _i x. ( 2 x. _pi ) ) / N ) )
13 2picn 
 |-  ( 2 x. _pi ) e. CC
14 13 a1i 
 |-  ( N e. NN -> ( 2 x. _pi ) e. CC )
15 nncn 
 |-  ( N e. NN -> N e. CC )
16 nnne0 
 |-  ( N e. NN -> N =/= 0 )
17 8 14 15 16 div23d 
 |-  ( N e. NN -> ( ( _i x. ( 2 x. _pi ) ) / N ) = ( ( _i / N ) x. ( 2 x. _pi ) ) )
18 8 15 14 16 div32d 
 |-  ( N e. NN -> ( ( _i / N ) x. ( 2 x. _pi ) ) = ( _i x. ( ( 2 x. _pi ) / N ) ) )
19 12 17 18 3eqtrd 
 |-  ( N e. NN -> ( ( 2 x. ( _pi x. _i ) ) / N ) = ( _i x. ( ( 2 x. _pi ) / N ) ) )
20 19 fveq2d 
 |-  ( N e. NN -> ( exp ` ( ( 2 x. ( _pi x. _i ) ) / N ) ) = ( exp ` ( _i x. ( ( 2 x. _pi ) / N ) ) ) )
21 14 15 16 divcld 
 |-  ( N e. NN -> ( ( 2 x. _pi ) / N ) e. CC )
22 efival 
 |-  ( ( ( 2 x. _pi ) / N ) e. CC -> ( exp ` ( _i x. ( ( 2 x. _pi ) / N ) ) ) = ( ( cos ` ( ( 2 x. _pi ) / N ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / N ) ) ) ) )
23 21 22 syl 
 |-  ( N e. NN -> ( exp ` ( _i x. ( ( 2 x. _pi ) / N ) ) ) = ( ( cos ` ( ( 2 x. _pi ) / N ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / N ) ) ) ) )
24 1 20 23 3eqtrd 
 |-  ( N e. NN -> ( bRoU ` N ) = ( ( cos ` ( ( 2 x. _pi ) / N ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / N ) ) ) ) )