Theorem cos9thpinconstrlem2

Description: The complex number A is not constructible. (Contributed by Thierry Arnoux, 15-Nov-2025)

	Ref	Expression
Hypotheses	cos9thpinconstr.1	$$⊢O={\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}$$
	cos9thpiminply.2	$$⊢Z=O^{\frac{1}{3}}$$
	cos9thpiminply.3	$$⊢A=Z+\left(\frac{1}{Z}\right)$$
Assertion	cos9thpinconstrlem2	$$⊢\neg A\in \mathrm{Constr}$$

Proof

Step	Hyp	Ref	Expression
1		cos9thpinconstr.1	$$⊢O={\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}$$
2		cos9thpiminply.2	$$⊢Z=O^{\frac{1}{3}}$$
3		cos9thpiminply.3	$$⊢A=Z+\left(\frac{1}{Z}\right)$$
4		eqid	$$⊢{\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)={\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
5		eqid	$$⊢{ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}={ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}$$
6		ax-icn	$$⊢\mathrm{i}\in ℂ$$
7	6	a1i	$$⊢\top \to \mathrm{i}\in ℂ$$
8		2cnd	$$⊢\top \to 2\in ℂ$$
9		picn	$$⊢\mathrm{\pi }\in ℂ$$
10	9	a1i	$$⊢\top \to \mathrm{\pi }\in ℂ$$
11	8 10	mulcld	$$⊢\top \to 2\mathrm{\pi }\in ℂ$$
12	7 11	mulcld	$$⊢\top \to \mathrm{i}2\mathrm{\pi }\in ℂ$$
13		3cn	$$⊢3\in ℂ$$
14	13	a1i	$$⊢\top \to 3\in ℂ$$
15		3ne0	$$⊢3\ne 0$$
16	15	a1i	$$⊢\top \to 3\ne 0$$
17	12 14 16	divcld	$$⊢\top \to \frac{\mathrm{i}2\mathrm{\pi }}{3}\in ℂ$$
18	17	efcld	$$⊢\top \to {\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\in ℂ$$
19	1 18	eqeltrid	$$⊢\top \to O\in ℂ$$
20	13 15	reccli	$$⊢\frac{1}{3}\in ℂ$$
21	20	a1i	$$⊢\top \to \frac{1}{3}\in ℂ$$
22	19 21	cxpcld	$$⊢\top \to O^{\frac{1}{3}}\in ℂ$$
23	2 22	eqeltrid	$$⊢\top \to Z\in ℂ$$
24	2	a1i	$$⊢\top \to Z=O^{\frac{1}{3}}$$
25	1	a1i	$$⊢\top \to O={\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}$$
26	17	efne0d	$$⊢\top \to {\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}\ne 0$$
27	25 26	eqnetrd	$$⊢\top \to O\ne 0$$
28	19 27 21	cxpne0d	$$⊢\top \to O^{\frac{1}{3}}\ne 0$$
29	24 28	eqnetrd	$$⊢\top \to Z\ne 0$$
30	23 29	reccld	$$⊢\top \to \frac{1}{Z}\in ℂ$$
31	23 30	addcld	$$⊢\top \to Z+\left(\frac{1}{Z}\right)\in ℂ$$
32	3 31	eqeltrid	$$⊢\top \to A\in ℂ$$
33		eqidd	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(A\right)=\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(A\right)$$
34		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
35		eqid	$$⊢{+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}={+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}$$
36		eqid	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}={\cdot }_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}$$
37		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}={\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}$$
38		eqid	$$⊢{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)={\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
39		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)$$
40		eqid	$$⊢{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)={\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
41		eqid	$$⊢\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\left(\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(-3\right){\cdot }_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(1\right)\right)=\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\left(\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(-3\right){\cdot }_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(1\right)\right)$$
42	1 2 3 34 35 36 37 38 39 40 4 41 5	cos9thpiminply	$$⊢\left(\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\left(\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(-3\right){\cdot }_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(1\right)\right)=\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(A\right)\wedge {\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\left(\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(-3\right){\cdot }_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(1\right)\right)\right)=3\right)$$
43	42	simpli	$$⊢\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\left(\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(-3\right){\cdot }_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(1\right)\right)=\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(A\right)$$
44	43	fveq2i	$$⊢{\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\left(\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(-3\right){\cdot }_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(1\right)\right)\right)={\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(A\right)\right)$$
45	42	simpri	$$⊢{\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left(3{\cdot }_{{\mathrm{mulGrp}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\left(\left(\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(-3\right){\cdot }_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}{\mathrm{var}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right){+}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)\left(1\right)\right)\right)=3$$
46	44 45	eqtr3i	$$⊢{\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(A\right)\right)=3$$
47		3nn0	$$⊢3\in {\mathbb{N}}_0$$
48	46 47	eqeltri	$$⊢{\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(A\right)\right)\in {\mathbb{N}}_0$$
49	48	a1i	$$⊢\top \to {\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(A\right)\right)\in {\mathbb{N}}_0$$
50	46	a1i	$$⊢n\in {\mathbb{N}}_0\to {\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(A\right)\right)=3$$
51		3z	$$⊢3\in \mathbb{Z}$$
52		iddvds	$$⊢3\in \mathbb{Z}\to 3\parallel 3$$
53	51 52	ax-mp	$$⊢3\parallel 3$$
54		simpr	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3=2^n\right)\to 3=2^n$$
55	53 54	breqtrid	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3=2^n\right)\to 3\parallel 2^n$$
56		3prm	$$⊢3\in \mathbb{P}$$
57		2prm	$$⊢2\in \mathbb{P}$$
58		prmdvdsexpr	$$⊢\left(3\in \mathbb{P}\wedge 2\in \mathbb{P}\wedge n\in {\mathbb{N}}_0\right)\to \left(3\parallel 2^n\to 3=2\right)$$
59	56 57 58	mp3an12	$$⊢n\in {\mathbb{N}}_0\to \left(3\parallel 2^n\to 3=2\right)$$
60	59	imp	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3\parallel 2^n\right)\to 3=2$$
61	55 60	syldan	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3=2^n\right)\to 3=2$$
62		2re	$$⊢2\in ℝ$$
63		2lt3	$$⊢2<3$$
64	62 63	gtneii	$$⊢3\ne 2$$
65	64	neii	$$⊢\neg 3=2$$
66	65	a1i	$$⊢\left(n\in {\mathbb{N}}_0\wedge 3=2^n\right)\to \neg 3=2$$
67	61 66	pm2.65da	$$⊢n\in {\mathbb{N}}_0\to \neg 3=2^n$$
68	67	neqned	$$⊢n\in {\mathbb{N}}_0\to 3\ne 2^n$$
69	50 68	eqnetrd	$$⊢n\in {\mathbb{N}}_0\to {\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(A\right)\right)\ne 2^n$$
70	69	adantl	$$⊢\left(\top \wedge n\in {\mathbb{N}}_0\right)\to {\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(\left({ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}\right)\left(A\right)\right)\ne 2^n$$
71	4 5 32 33 49 70	constrcon	$$⊢\top \to \neg A\in \mathrm{Constr}$$
72	71	mptru	$$⊢\neg A\in \mathrm{Constr}$$