Theorem bru2

Description: The basic 2nd root of unity is -u 1 . (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Assertion	bru2	⊢ ( bRoU ‘ 2 ) = - 1

Proof

Step	Hyp	Ref	Expression
1		2nn	⊢ 2 ∈ ℕ
2		bruval2	⊢ ( 2 ∈ ℕ → ( bRoU ‘ 2 ) = ( - 1 ↑𝑐 ( 2 / 2 ) ) )
3	1 2	ax-mp	⊢ ( bRoU ‘ 2 ) = ( - 1 ↑𝑐 ( 2 / 2 ) )
4		2div2e1	⊢ ( 2 / 2 ) = 1
5	4	oveq2i	⊢ ( - 1 ↑𝑐 ( 2 / 2 ) ) = ( - 1 ↑𝑐 1 )
6		neg1cn	⊢ - 1 ∈ ℂ
7		cxp1	⊢ ( - 1 ∈ ℂ → ( - 1 ↑𝑐 1 ) = - 1 )
8	6 7	ax-mp	⊢ ( - 1 ↑𝑐 1 ) = - 1
9	3 5 8	3eqtri	⊢ ( bRoU ‘ 2 ) = - 1