Theorem bru1

Description: The basic (and only) 1st root of unity is 1. (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Assertion	bru1	⊢ ( bRoU ‘ 1 ) = 1

Proof

Step	Hyp	Ref	Expression
1		1nn	⊢ 1 ∈ ℕ
2		bruval2	⊢ ( 1 ∈ ℕ → ( bRoU ‘ 1 ) = ( - 1 ↑𝑐 ( 2 / 1 ) ) )
3	1 2	ax-mp	⊢ ( bRoU ‘ 1 ) = ( - 1 ↑𝑐 ( 2 / 1 ) )
4		2cn	⊢ 2 ∈ ℂ
5	4	div1i	⊢ ( 2 / 1 ) = 2
6	5	oveq2i	⊢ ( - 1 ↑𝑐 ( 2 / 1 ) ) = ( - 1 ↑𝑐 2 )
7		neg1cn	⊢ - 1 ∈ ℂ
8		neg1ne0	⊢ - 1 ≠ 0
9		2z	⊢ 2 ∈ ℤ
10		cxpexpz	⊢ ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ∧ 2 ∈ ℤ ) → ( - 1 ↑𝑐 2 ) = ( - 1 ↑ 2 ) )
11	7 8 9 10	mp3an	⊢ ( - 1 ↑𝑐 2 ) = ( - 1 ↑ 2 )
12		neg1sqe1	⊢ ( - 1 ↑ 2 ) = 1
13	11 12	eqtri	⊢ ( - 1 ↑𝑐 2 ) = 1
14	6 13	eqtri	⊢ ( - 1 ↑𝑐 ( 2 / 1 ) ) = 1
15	3 14	eqtri	⊢ ( bRoU ‘ 1 ) = 1