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 · 1 ) = 2
2		2t2e4	⊢ ( 2 · 2 ) = 4
3	1 2	oveq12i	⊢ ( ( 2 · 1 ) / ( 2 · 2 ) ) = ( 2 / 4 )
4		ax-1cn	⊢ 1 ∈ ℂ
5		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
6		divcan5	⊢ ( ( 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 2 · 1 ) / ( 2 · 2 ) ) = ( 1 / 2 ) )
7	4 5 5 6	mp3an	⊢ ( ( 2 · 1 ) / ( 2 · 2 ) ) = ( 1 / 2 )
8	3 7	eqtr3i	⊢ ( 2 / 4 ) = ( 1 / 2 )
9	8	oveq2i	⊢ ( - 1 ↑𝑐 ( 2 / 4 ) ) = ( - 1 ↑𝑐 ( 1 / 2 ) )
10		neg1cn	⊢ - 1 ∈ ℂ
11		cxpsqrt	⊢ ( - 1 ∈ ℂ → ( - 1 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ - 1 ) )
12	10 11	ax-mp	⊢ ( - 1 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ - 1 )
13	9 12	eqtri	⊢ ( - 1 ↑𝑐 ( 2 / 4 ) ) = ( √ ‘ - 1 )
14		4nn	⊢ 4 ∈ ℕ
15		bruval2	⊢ ( 4 ∈ ℕ → ( bRoU ‘ 4 ) = ( - 1 ↑𝑐 ( 2 / 4 ) ) )
16	14 15	ax-mp	⊢ ( bRoU ‘ 4 ) = ( - 1 ↑𝑐 ( 2 / 4 ) )
17		sqrtm1	⊢ i = ( √ ‘ - 1 )
18	13 16 17	3eqtr4i	⊢ ( bRoU ‘ 4 ) = i