Theorem bru2

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

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

Proof

Step	Hyp	Ref	Expression
1		2nn	$$⊢2\in \mathbb{N}$$
2		bruval2	Could not format ( 2 e. NN -> ( bRoU ` 2 ) = ( -u 1 ^c ( 2 / 2 ) ) ) : No typesetting found for |- ( 2 e. NN -> ( bRoU ` 2 ) = ( -u 1 ^c ( 2 / 2 ) ) ) with typecode |-
3	1 2	ax-mp	Could not format ( bRoU ` 2 ) = ( -u 1 ^c ( 2 / 2 ) ) : No typesetting found for |- ( bRoU ` 2 ) = ( -u 1 ^c ( 2 / 2 ) ) with typecode |-
4		2div2e1	$$⊢\frac{2}{2}=1$$
5	4	oveq2i	$$⊢{\left(-1\right)}^{\frac{2}{2}}={\left(-1\right)}^1$$
6		neg1cn	$$⊢-1\in ℂ$$
7		cxp1	$$⊢-1\in ℂ\to {\left(-1\right)}^1=-1$$
8	6 7	ax-mp	$$⊢{\left(-1\right)}^1=-1$$
9	3 5 8	3eqtri	Could not format ( bRoU ` 2 ) = -u 1 : No typesetting found for |- ( bRoU ` 2 ) = -u 1 with typecode |-