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	⊢ ( 𝑁 ∈ ℕ → ( ( bRoU ‘ 𝑁 ) ↑ 𝑁 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		bruval2	⊢ ( 𝑁 ∈ ℕ → ( bRoU ‘ 𝑁 ) = ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) )
2	1	oveq1d	⊢ ( 𝑁 ∈ ℕ → ( ( bRoU ‘ 𝑁 ) ↑ 𝑁 ) = ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑁 ) )
3		root1id	⊢ ( 𝑁 ∈ ℕ → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑁 ) = 1 )
4	2 3	eqtrd	⊢ ( 𝑁 ∈ ℕ → ( ( bRoU ‘ 𝑁 ) ↑ 𝑁 ) = 1 )