Theorem bru4

Description: The basic 4th root of unity is _i . (Contributed by AV, 27-Oct-2026)

	Ref	Expression
Assertion	bru4	|- ( bRoU ` 4 ) = _i

Proof

Step	Hyp	Ref	Expression
1		2t1e2	|- ( 2 x. 1 ) = 2
2		2t2e4	|- ( 2 x. 2 ) = 4
3	1 2	oveq12i	|- ( ( 2 x. 1 ) / ( 2 x. 2 ) ) = ( 2 / 4 )
4		ax-1cn	|- 1 e. CC
5		2cnne0	|- ( 2 e. CC /\ 2 =/= 0 )
6		divcan5	|- ( ( 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 2 x. 1 ) / ( 2 x. 2 ) ) = ( 1 / 2 ) )
7	4 5 5 6	mp3an	|- ( ( 2 x. 1 ) / ( 2 x. 2 ) ) = ( 1 / 2 )
8	3 7	eqtr3i	|- ( 2 / 4 ) = ( 1 / 2 )
9	8	oveq2i	|- ( -u 1 ^c ( 2 / 4 ) ) = ( -u 1 ^c ( 1 / 2 ) )
10		neg1cn	|- -u 1 e. CC
11		cxpsqrt	|- ( -u 1 e. CC -> ( -u 1 ^c ( 1 / 2 ) ) = ( sqrt ` -u 1 ) )
12	10 11	ax-mp	|- ( -u 1 ^c ( 1 / 2 ) ) = ( sqrt ` -u 1 )
13	9 12	eqtri	|- ( -u 1 ^c ( 2 / 4 ) ) = ( sqrt ` -u 1 )
14		4nn	|- 4 e. NN
15		bruval2	|- ( 4 e. NN -> ( bRoU ` 4 ) = ( -u 1 ^c ( 2 / 4 ) ) )
16	14 15	ax-mp	|- ( bRoU ` 4 ) = ( -u 1 ^c ( 2 / 4 ) )
17		sqrtm1	|- _i = ( sqrt ` -u 1 )
18	13 16 17	3eqtr4i	|- ( bRoU ` 4 ) = _i