Metamath Proof Explorer

Theorem bruvalexp

Description: The N -th power of the basic N -th root of unity is 1. (Contributed by AV, 24-Oct-2026)

Ref Expression
Assertion bruvalexp 
|- ( N e. NN -> ( ( bRoU ` N ) ^ N ) = 1 )

Proof

Step Hyp Ref Expression
1 bruval2 
 |-  ( N e. NN -> ( bRoU ` N ) = ( -u 1 ^c ( 2 / N ) ) )
2 1 oveq1d 
 |-  ( N e. NN -> ( ( bRoU ` N ) ^ N ) = ( ( -u 1 ^c ( 2 / N ) ) ^ N ) )
3 root1id 
 |-  ( N e. NN -> ( ( -u 1 ^c ( 2 / N ) ) ^ N ) = 1 )
4 2 3 eqtrd 
 |-  ( N e. NN -> ( ( bRoU ` N ) ^ N ) = 1 )