Theorem bru1

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

	Ref	Expression
Assertion	bru1	Could not format assertion : No typesetting found for |- ( bRoU ` 1 ) = 1 with typecode |-

Proof

Step	Hyp	Ref	Expression
1		1nn	$$⊢1\in \mathbb{N}$$
2		bruval2	Could not format ( 1 e. NN -> ( bRoU ` 1 ) = ( -u 1 ^c ( 2 / 1 ) ) ) : No typesetting found for |- ( 1 e. NN -> ( bRoU ` 1 ) = ( -u 1 ^c ( 2 / 1 ) ) ) with typecode |-
3	1 2	ax-mp	Could not format ( bRoU ` 1 ) = ( -u 1 ^c ( 2 / 1 ) ) : No typesetting found for |- ( bRoU ` 1 ) = ( -u 1 ^c ( 2 / 1 ) ) with typecode |-
4		2cn	$$⊢2\in ℂ$$
5	4	div1i	$$⊢\frac{2}{1}=2$$
6	5	oveq2i	$$⊢{\left(-1\right)}^{\frac{2}{1}}={\left(-1\right)}^2$$
7		neg1cn	$$⊢-1\in ℂ$$
8		neg1ne0	$$⊢-1\ne 0$$
9		2z	$$⊢2\in \mathbb{Z}$$
10		cxpexpz	$$⊢\left(-1\in ℂ\wedge -1\ne 0\wedge 2\in \mathbb{Z}\right)\to {\left(-1\right)}^2={\left(-1\right)}^2$$
11	7 8 9 10	mp3an	$$⊢{\left(-1\right)}^2={\left(-1\right)}^2$$
12		neg1sqe1	$$⊢{\left(-1\right)}^2=1$$
13	11 12	eqtri	$$⊢{\left(-1\right)}^2=1$$
14	6 13	eqtri	$$⊢{\left(-1\right)}^{\frac{2}{1}}=1$$
15	3 14	eqtri	Could not format ( bRoU ` 1 ) = 1 : No typesetting found for |- ( bRoU ` 1 ) = 1 with typecode |-