Theorem cos9thpiminplylem4

Description: Lemma for cos9thpiminply . (Contributed by Thierry Arnoux, 14-Nov-2025)

	Ref	Expression
Hypotheses	cos9thpiminplylem3.1	$$⊢O={\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}$$
	cos9thpiminplylem4.2	$$⊢Z=O^{\frac{1}{3}}$$
Assertion	cos9thpiminplylem4	$$⊢Z^6+Z^3=-1$$

Proof

Step	Hyp	Ref	Expression
1		cos9thpiminplylem3.1	$$⊢O={\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}$$
2		cos9thpiminplylem4.2	$$⊢Z=O^{\frac{1}{3}}$$
3		ax-icn	$$⊢\mathrm{i}\in ℂ$$
4		2cn	$$⊢2\in ℂ$$
5		picn	$$⊢\mathrm{\pi }\in ℂ$$
6	4 5	mulcli	$$⊢2\mathrm{\pi }\in ℂ$$
7	3 6	mulcli	$$⊢\mathrm{i}2\mathrm{\pi }\in ℂ$$
8		3cn	$$⊢3\in ℂ$$
9		3ne0	$$⊢3\ne 0$$
10	7 8 9	divcli	$$⊢\frac{\mathrm{i}2\mathrm{\pi }}{3}\in ℂ$$
11		efcl	$$⊢\frac{\mathrm{i}2\mathrm{\pi }}{3}\in ℂ\to {\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\in ℂ$$
12	10 11	ax-mp	$$⊢{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\in ℂ$$
13	1 12	eqeltri	$$⊢O\in ℂ$$
14	8 9	reccli	$$⊢\frac{1}{3}\in ℂ$$
15		cxpcl	$$⊢\left(O\in ℂ\wedge \frac{1}{3}\in ℂ\right)\to O^{\frac{1}{3}}\in ℂ$$
16	13 14 15	mp2an	$$⊢O^{\frac{1}{3}}\in ℂ$$
17	2 16	eqeltri	$$⊢Z\in ℂ$$
18		3nn0	$$⊢3\in {\mathbb{N}}_0$$
19		2nn0	$$⊢2\in {\mathbb{N}}_0$$
20		expmul	$$⊢\left(Z\in ℂ\wedge 3\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\to Z^{3\cdot 2}={\left(Z^3\right)}^2$$
21	17 18 19 20	mp3an	$$⊢Z^{3\cdot 2}={\left(Z^3\right)}^2$$
22		3t2e6	$$⊢3\cdot 2=6$$
23	22	oveq2i	$$⊢Z^{3\cdot 2}=Z^6$$
24	2	oveq1i	$$⊢Z^3={\left(O^{\frac{1}{3}}\right)}^3$$
25		cxpmul2	$$⊢\left(O\in ℂ\wedge \frac{1}{3}\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to O^{\left(\frac{1}{3}\right)\cdot 3}={\left(O^{\frac{1}{3}}\right)}^3$$
26	13 14 18 25	mp3an	$$⊢O^{\left(\frac{1}{3}\right)\cdot 3}={\left(O^{\frac{1}{3}}\right)}^3$$
27	24 26	eqtr4i	$$⊢Z^3=O^{\left(\frac{1}{3}\right)\cdot 3}$$
28		ax-1cn	$$⊢1\in ℂ$$
29	28 8 9	divcan1i	$$⊢\left(\frac{1}{3}\right)\cdot 3=1$$
30	29	oveq2i	$$⊢O^{\left(\frac{1}{3}\right)\cdot 3}=O^1$$
31		cxp1	$$⊢O\in ℂ\to O^1=O$$
32	13 31	ax-mp	$$⊢O^1=O$$
33	27 30 32	3eqtri	$$⊢Z^3=O$$
34	33	oveq1i	$$⊢{\left(Z^3\right)}^2=O^2$$
35	21 23 34	3eqtr3i	$$⊢Z^6=O^2$$
36	35 33	oveq12i	$$⊢Z^6+Z^3=O^2+O$$
37	13	sqcli	$$⊢O^2\in ℂ$$
38	37 13	addcli	$$⊢O^2+O\in ℂ$$
39	38 28	pm3.2i	$$⊢\left(O^2+O\in ℂ\wedge 1\in ℂ\right)$$
40	37 13 28	addassi	$$⊢O^2+O+1=O^2+O+1$$
41	1	cos9thpiminplylem3	$$⊢O^2+O+1=0$$
42	40 41	eqtri	$$⊢O^2+O+1=0$$
43		addeq0	$$⊢\left(O^2+O\in ℂ\wedge 1\in ℂ\right)\to \left(O^2+O+1=0\leftrightarrow O^2+O=-1\right)$$
44	43	biimpa	$$⊢\left(\left(O^2+O\in ℂ\wedge 1\in ℂ\right)\wedge O^2+O+1=0\right)\to O^2+O=-1$$
45	39 42 44	mp2an	$$⊢O^2+O=-1$$
46	36 45	eqtri	$$⊢Z^6+Z^3=-1$$