Theorem bru4

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

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

Proof

Step	Hyp	Ref	Expression
1		2t1e2	$$⊢2\cdot 1=2$$
2		2t2e4	$$⊢2\cdot 2=4$$
3	1 2	oveq12i	$$⊢\frac{2\cdot 1}{2\cdot 2}=\frac{2}{4}$$
4		ax-1cn	$$⊢1\in ℂ$$
5		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
6		divcan5	$$⊢\left(1\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{2\cdot 1}{2\cdot 2}=\frac{1}{2}$$
7	4 5 5 6	mp3an	$$⊢\frac{2\cdot 1}{2\cdot 2}=\frac{1}{2}$$
8	3 7	eqtr3i	$$⊢\frac{2}{4}=\frac{1}{2}$$
9	8	oveq2i	$$⊢{\left(-1\right)}^{\frac{2}{4}}={\left(-1\right)}^{\frac{1}{2}}$$
10		neg1cn	$$⊢-1\in ℂ$$
11		cxpsqrt	$$⊢-1\in ℂ\to {\left(-1\right)}^{\frac{1}{2}}=\sqrt{-1}$$
12	10 11	ax-mp	$$⊢{\left(-1\right)}^{\frac{1}{2}}=\sqrt{-1}$$
13	9 12	eqtri	$$⊢{\left(-1\right)}^{\frac{2}{4}}=\sqrt{-1}$$
14		4nn	$$⊢4\in \mathbb{N}$$
15		bruval2	Could not format ( 4 e. NN -> ( bRoU ` 4 ) = ( -u 1 ^c ( 2 / 4 ) ) ) : No typesetting found for |- ( 4 e. NN -> ( bRoU ` 4 ) = ( -u 1 ^c ( 2 / 4 ) ) ) with typecode |-
16	14 15	ax-mp	Could not format ( bRoU ` 4 ) = ( -u 1 ^c ( 2 / 4 ) ) : No typesetting found for |- ( bRoU ` 4 ) = ( -u 1 ^c ( 2 / 4 ) ) with typecode |-
17		sqrtm1	$$⊢\mathrm{i}=\sqrt{-1}$$
18	13 16 17	3eqtr4i	Could not format ( bRoU ` 4 ) = _i : No typesetting found for |- ( bRoU ` 4 ) = _i with typecode |-