Theorem cos9thpiminplylem5

Description: The constructed complex number A is a root of the polynomial ( ( X ^ 3 ) + ( ( -u 3 x. X ) + 1 ) ) . (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}}$$
	cos9thpiminplylem5.3	$$⊢A=Z+\left(\frac{1}{Z}\right)$$
Assertion	cos9thpiminplylem5	$$⊢A^3+-3A+1=0$$

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		cos9thpiminplylem5.3	$$⊢A=Z+\left(\frac{1}{Z}\right)$$
4		ax-icn	$$⊢\mathrm{i}\in ℂ$$
5		2cn	$$⊢2\in ℂ$$
6		picn	$$⊢\mathrm{\pi }\in ℂ$$
7	5 6	mulcli	$$⊢2\mathrm{\pi }\in ℂ$$
8	4 7	mulcli	$$⊢\mathrm{i}2\mathrm{\pi }\in ℂ$$
9		3cn	$$⊢3\in ℂ$$
10		3ne0	$$⊢3\ne 0$$
11	8 9 10	divcli	$$⊢\frac{\mathrm{i}2\mathrm{\pi }}{3}\in ℂ$$
12		efcl	$$⊢\frac{\mathrm{i}2\mathrm{\pi }}{3}\in ℂ\to {\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\in ℂ$$
13	11 12	ax-mp	$$⊢{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\in ℂ$$
14	1 13	eqeltri	$$⊢O\in ℂ$$
15		ax-1cn	$$⊢1\in ℂ$$
16	15 9 10	divcli	$$⊢\frac{1}{3}\in ℂ$$
17		cxpcl	$$⊢\left(O\in ℂ\wedge \frac{1}{3}\in ℂ\right)\to O^{\frac{1}{3}}\in ℂ$$
18	14 16 17	mp2an	$$⊢O^{\frac{1}{3}}\in ℂ$$
19	2 18	eqeltri	$$⊢Z\in ℂ$$
20		efne0	$$⊢\frac{\mathrm{i}2\mathrm{\pi }}{3}\in ℂ\to {\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\ne 0$$
21	11 20	ax-mp	$$⊢{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\ne 0$$
22	1 21	eqnetri	$$⊢O\ne 0$$
23		cxpne0	$$⊢\left(O\in ℂ\wedge O\ne 0\wedge \frac{1}{3}\in ℂ\right)\to O^{\frac{1}{3}}\ne 0$$
24	14 22 16 23	mp3an	$$⊢O^{\frac{1}{3}}\ne 0$$
25	2 24	eqnetri	$$⊢Z\ne 0$$
26	15 19 25	divcli	$$⊢\frac{1}{Z}\in ℂ$$
27	19 26	addcli	$$⊢Z+\left(\frac{1}{Z}\right)\in ℂ$$
28	3 27	eqeltri	$$⊢A\in ℂ$$
29		3nn0	$$⊢3\in {\mathbb{N}}_0$$
30		expcl	$$⊢\left(A\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to A^3\in ℂ$$
31	28 29 30	mp2an	$$⊢A^3\in ℂ$$
32	9	negcli	$$⊢-3\in ℂ$$
33	32 28	mulcli	$$⊢-3A\in ℂ$$
34	33 15	addcli	$$⊢-3A+1\in ℂ$$
35	31 34	pm3.2i	$$⊢\left(A^3\in ℂ\wedge -3A+1\in ℂ\right)$$
36		binom3	$$⊢\left(Z\in ℂ\wedge \frac{1}{Z}\in ℂ\right)\to {\left(Z+\left(\frac{1}{Z}\right)\right)}^3=Z^3+3Z^2\left(\frac{1}{Z}\right)+3Z{\left(\frac{1}{Z}\right)}^2+{\left(\frac{1}{Z}\right)}^3$$
37	19 26 36	mp2an	$$⊢{\left(Z+\left(\frac{1}{Z}\right)\right)}^3=Z^3+3Z^2\left(\frac{1}{Z}\right)+3Z{\left(\frac{1}{Z}\right)}^2+{\left(\frac{1}{Z}\right)}^3$$
38	3	oveq1i	$$⊢A^3={\left(Z+\left(\frac{1}{Z}\right)\right)}^3$$
39	33 15	negdii	$$⊢-\left(-3A+1\right)=--3A+-1$$
40	32 28	mulneg1i	$$⊢\left(--3\right)A=--3A$$
41	40	oveq1i	$$⊢\left(--3\right)A+-1=--3A+-1$$
42	9	negnegi	$$⊢--3=3$$
43	42	oveq1i	$$⊢\left(--3\right)A=3A$$
44	43	oveq1i	$$⊢\left(--3\right)A+-1=3A+-1$$
45	41 44	eqtr3i	$$⊢--3A+-1=3A+-1$$
46		6nn0	$$⊢6\in {\mathbb{N}}_0$$
47		expcl	$$⊢\left(Z\in ℂ\wedge 6\in {\mathbb{N}}_0\right)\to Z^6\in ℂ$$
48	19 46 47	mp2an	$$⊢Z^6\in ℂ$$
49		expcl	$$⊢\left(Z\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to Z^3\in ℂ$$
50	19 29 49	mp2an	$$⊢Z^3\in ℂ$$
51	48 50	addcomi	$$⊢Z^6+Z^3=Z^3+Z^6$$
52	1 2	cos9thpiminplylem4	$$⊢Z^6+Z^3=-1$$
53	13	sqcli	$$⊢{{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2\in ℂ$$
54	13 21	pm3.2i	$$⊢\left({\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\in ℂ\wedge {\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\ne 0\right)$$
55	15 53 54	3pm3.2i	$$⊢\left(1\in ℂ\wedge {{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2\in ℂ\wedge \left({\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\in ℂ\wedge {\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\ne 0\right)\right)$$
56	5 15 11	adddiri	$$⊢\left(2+1\right)\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)=2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)+1\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)$$
57		2p1e3	$$⊢2+1=3$$
58	57	oveq1i	$$⊢\left(2+1\right)\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)=3\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)$$
59	8 9 10	divcan2i	$$⊢3\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)=\mathrm{i}2\mathrm{\pi }$$
60	58 59	eqtri	$$⊢\left(2+1\right)\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)=\mathrm{i}2\mathrm{\pi }$$
61	11	mullidi	$$⊢1\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)=\frac{\mathrm{i}2\mathrm{\pi }}{3}$$
62	61	oveq2i	$$⊢2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)+1\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)=2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)+\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)$$
63	56 60 62	3eqtr3ri	$$⊢2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)+\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)=\mathrm{i}2\mathrm{\pi }$$
64	63	fveq2i	$$⊢{\mathrm{e}}^{2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)+\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)}={\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }}$$
65	5 11	mulcli	$$⊢2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)\in ℂ$$
66		efadd	$$⊢\left(2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)\in ℂ\wedge \frac{\mathrm{i}2\mathrm{\pi }}{3}\in ℂ\right)\to {\mathrm{e}}^{2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)+\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)}={\mathrm{e}}^{2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)}{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}$$
67	65 11 66	mp2an	$$⊢{\mathrm{e}}^{2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)+\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)}={\mathrm{e}}^{2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)}{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}$$
68	64 67	eqtr3i	$$⊢{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }}={\mathrm{e}}^{2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)}{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}$$
69		ef2pi	$$⊢{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }}=1$$
70		2z	$$⊢2\in \mathbb{Z}$$
71		efexp	$$⊢\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\in ℂ\wedge 2\in \mathbb{Z}\right)\to {\mathrm{e}}^{2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)}={{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2$$
72	11 70 71	mp2an	$$⊢{\mathrm{e}}^{2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)}={{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2$$
73	72	oveq1i	$$⊢{\mathrm{e}}^{2\left(\frac{\mathrm{i}2\mathrm{\pi }}{3}\right)}{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}={{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}$$
74	68 69 73	3eqtr3i	$$⊢1={{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}$$
75		divmul3	$$⊢\left(1\in ℂ\wedge {{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2\in ℂ\wedge \left({\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\in ℂ\wedge {\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\ne 0\right)\right)\to \left(\frac{1}{{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}={{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2\leftrightarrow 1={{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\right)$$
76	75	biimpar	$$⊢\left(\left(1\in ℂ\wedge {{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2\in ℂ\wedge \left({\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\in ℂ\wedge {\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\ne 0\right)\right)\wedge 1={{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\right)\to \frac{1}{{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}={{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2$$
77	55 74 76	mp2an	$$⊢\frac{1}{{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}={{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2$$
78	1	oveq2i	$$⊢\frac{1}{O}=\frac{1}{{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}$$
79	1	oveq1i	$$⊢O^2={{\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}}^2$$
80	77 78 79	3eqtr4ri	$$⊢O^2=\frac{1}{O}$$
81	2	oveq1i	$$⊢Z^3={\left(O^{\frac{1}{3}}\right)}^3$$
82		3nn	$$⊢3\in \mathbb{N}$$
83		cxproot	$$⊢\left(O\in ℂ\wedge 3\in \mathbb{N}\right)\to {\left(O^{\frac{1}{3}}\right)}^3=O$$
84	14 82 83	mp2an	$$⊢{\left(O^{\frac{1}{3}}\right)}^3=O$$
85	81 84	eqtr2i	$$⊢O=Z^3$$
86	85	oveq1i	$$⊢O^2={\left(Z^3\right)}^2$$
87	85	oveq2i	$$⊢\frac{1}{O}=\frac{1}{Z^3}$$
88	80 86 87	3eqtr3i	$$⊢{\left(Z^3\right)}^2=\frac{1}{Z^3}$$
89		3t2e6	$$⊢3\cdot 2=6$$
90	89	oveq2i	$$⊢Z^{3\cdot 2}=Z^6$$
91		2nn0	$$⊢2\in {\mathbb{N}}_0$$
92		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$$
93	19 29 91 92	mp3an	$$⊢Z^{3\cdot 2}={\left(Z^3\right)}^2$$
94	90 93	eqtr3i	$$⊢Z^6={\left(Z^3\right)}^2$$
95		3z	$$⊢3\in \mathbb{Z}$$
96		exprec	$$⊢\left(Z\in ℂ\wedge Z\ne 0\wedge 3\in \mathbb{Z}\right)\to {\left(\frac{1}{Z}\right)}^3=\frac{1}{Z^3}$$
97	19 25 95 96	mp3an	$$⊢{\left(\frac{1}{Z}\right)}^3=\frac{1}{Z^3}$$
98	88 94 97	3eqtr4i	$$⊢Z^6={\left(\frac{1}{Z}\right)}^3$$
99	98	oveq2i	$$⊢Z^3+Z^6=Z^3+{\left(\frac{1}{Z}\right)}^3$$
100	51 52 99	3eqtr3i	$$⊢-1=Z^3+{\left(\frac{1}{Z}\right)}^3$$
101		sqdivid	$$⊢\left(Z\in ℂ\wedge Z\ne 0\right)\to \frac{Z^2}{Z}=Z$$
102	19 25 101	mp2an	$$⊢\frac{Z^2}{Z}=Z$$
103	19	sqcli	$$⊢Z^2\in ℂ$$
104	103 19 25	divreci	$$⊢\frac{Z^2}{Z}=Z^2\left(\frac{1}{Z}\right)$$
105	102 104	eqtr3i	$$⊢Z=Z^2\left(\frac{1}{Z}\right)$$
106	15 5	negsubi	$$⊢1+-2=1-2$$
107	5 15	negsubdi2i	$$⊢-\left(2-1\right)=1-2$$
108		2m1e1	$$⊢2-1=1$$
109	108	negeqi	$$⊢-\left(2-1\right)=-1$$
110	106 107 109	3eqtr2i	$$⊢1+-2=-1$$
111	110	oveq2i	$$⊢Z^{1+-2}=Z^{-1}$$
112		1z	$$⊢1\in \mathbb{Z}$$
113	91	nn0negzi	$$⊢-2\in \mathbb{Z}$$
114		expaddz	$$⊢\left(\left(Z\in ℂ\wedge Z\ne 0\right)\wedge \left(1\in \mathbb{Z}\wedge -2\in \mathbb{Z}\right)\right)\to Z^{1+-2}=Z^1{Z}^{-2}$$
115	19 25 112 113 114	mp4an	$$⊢Z^{1+-2}=Z^1{Z}^{-2}$$
116		expn1	$$⊢Z\in ℂ\to Z^{-1}=\frac{1}{Z}$$
117	19 116	ax-mp	$$⊢Z^{-1}=\frac{1}{Z}$$
118	111 115 117	3eqtr3i	$$⊢Z^1{Z}^{-2}=\frac{1}{Z}$$
119		exp1	$$⊢Z\in ℂ\to Z^1=Z$$
120	19 119	ax-mp	$$⊢Z^1=Z$$
121		expnegz	$$⊢\left(Z\in ℂ\wedge Z\ne 0\wedge 2\in \mathbb{Z}\right)\to Z^{-2}=\frac{1}{Z^2}$$
122	19 25 70 121	mp3an	$$⊢Z^{-2}=\frac{1}{Z^2}$$
123	19 25	sqrecii	$$⊢{\left(\frac{1}{Z}\right)}^2=\frac{1}{Z^2}$$
124	122 123	eqtr4i	$$⊢Z^{-2}={\left(\frac{1}{Z}\right)}^2$$
125	120 124	oveq12i	$$⊢Z^1{Z}^{-2}=Z{\left(\frac{1}{Z}\right)}^2$$
126	118 125	eqtr3i	$$⊢\frac{1}{Z}=Z{\left(\frac{1}{Z}\right)}^2$$
127	105 126	oveq12i	$$⊢Z+\left(\frac{1}{Z}\right)=Z^2\left(\frac{1}{Z}\right)+Z{\left(\frac{1}{Z}\right)}^2$$
128	3 127	eqtri	$$⊢A=Z^2\left(\frac{1}{Z}\right)+Z{\left(\frac{1}{Z}\right)}^2$$
129	128	oveq2i	$$⊢3A=3\left(Z^2\left(\frac{1}{Z}\right)+Z{\left(\frac{1}{Z}\right)}^2\right)$$
130	103 26	mulcli	$$⊢Z^2\left(\frac{1}{Z}\right)\in ℂ$$
131	26	sqcli	$$⊢{\left(\frac{1}{Z}\right)}^2\in ℂ$$
132	19 131	mulcli	$$⊢Z{\left(\frac{1}{Z}\right)}^2\in ℂ$$
133	9 130 132	adddii	$$⊢3\left(Z^2\left(\frac{1}{Z}\right)+Z{\left(\frac{1}{Z}\right)}^2\right)=3Z^2\left(\frac{1}{Z}\right)+3Z{\left(\frac{1}{Z}\right)}^2$$
134	129 133	eqtri	$$⊢3A=3Z^2\left(\frac{1}{Z}\right)+3Z{\left(\frac{1}{Z}\right)}^2$$
135	100 134	oveq12i	$$⊢-1+3A=Z^3+{\left(\frac{1}{Z}\right)}^3+3Z^2\left(\frac{1}{Z}\right)+3Z{\left(\frac{1}{Z}\right)}^2$$
136	15	negcli	$$⊢-1\in ℂ$$
137	9 28	mulcli	$$⊢3A\in ℂ$$
138	136 137	addcomi	$$⊢-1+3A=3A+-1$$
139		expcl	$$⊢\left(\frac{1}{Z}\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to {\left(\frac{1}{Z}\right)}^3\in ℂ$$
140	26 29 139	mp2an	$$⊢{\left(\frac{1}{Z}\right)}^3\in ℂ$$
141	9 130	mulcli	$$⊢3Z^2\left(\frac{1}{Z}\right)\in ℂ$$
142	9 132	mulcli	$$⊢3Z{\left(\frac{1}{Z}\right)}^2\in ℂ$$
143	50 140 141 142	add42i	$$⊢Z^3+{\left(\frac{1}{Z}\right)}^3+3Z^2\left(\frac{1}{Z}\right)+3Z{\left(\frac{1}{Z}\right)}^2=Z^3+3Z^2\left(\frac{1}{Z}\right)+3Z{\left(\frac{1}{Z}\right)}^2+{\left(\frac{1}{Z}\right)}^3$$
144	135 138 143	3eqtr3i	$$⊢3A+-1=Z^3+3Z^2\left(\frac{1}{Z}\right)+3Z{\left(\frac{1}{Z}\right)}^2+{\left(\frac{1}{Z}\right)}^3$$
145	39 45 144	3eqtri	$$⊢-\left(-3A+1\right)=Z^3+3Z^2\left(\frac{1}{Z}\right)+3Z{\left(\frac{1}{Z}\right)}^2+{\left(\frac{1}{Z}\right)}^3$$
146	37 38 145	3eqtr4i	$$⊢A^3=-\left(-3A+1\right)$$
147		addeq0	$$⊢\left(A^3\in ℂ\wedge -3A+1\in ℂ\right)\to \left(A^3+-3A+1=0\leftrightarrow A^3=-\left(-3A+1\right)\right)$$
148	147	biimpar	$$⊢\left(\left(A^3\in ℂ\wedge -3A+1\in ℂ\right)\wedge A^3=-\left(-3A+1\right)\right)\to A^3+-3A+1=0$$
149	35 146 148	mp2an	$$⊢A^3+-3A+1=0$$