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	Could not format assertion : No typesetting found for |- ( N e. NN -> ( ( bRoU ` N ) ^ N ) = 1 ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bruval2	Could not format ( N e. NN -> ( bRoU ` N ) = ( -u 1 ^c ( 2 / N ) ) ) : No typesetting found for |- ( N e. NN -> ( bRoU ` N ) = ( -u 1 ^c ( 2 / N ) ) ) with typecode |-
2	1	oveq1d	Could not format ( N e. NN -> ( ( bRoU ` N ) ^ N ) = ( ( -u 1 ^c ( 2 / N ) ) ^ N ) ) : No typesetting found for |- ( N e. NN -> ( ( bRoU ` N ) ^ N ) = ( ( -u 1 ^c ( 2 / N ) ) ^ N ) ) with typecode |-
3		root1id	$$⊢N\in \mathbb{N}\to {\left({-1}^{\frac{2}{N}}\right)}^N=1$$
4	2 3	eqtrd	Could not format ( N e. NN -> ( ( bRoU ` N ) ^ N ) = 1 ) : No typesetting found for |- ( N e. NN -> ( ( bRoU ` N ) ^ N ) = 1 ) with typecode |-