cos9thpiminply

Description: The polynomial ( ( X ^ 3 ) + ( ( -u 3 x. X ) + 1 ) ) is the minimal polynomial for A over QQ , and its degree is 3 . (Contributed by Thierry Arnoux, 14-Nov-2025)

	Ref	Expression
Hypotheses	cos9thpiminplylem3.1	$⊢ O = e^{\frac{i 2 π}{3}}$
	cos9thpiminplylem4.2	$⊢ Z = O^{\frac{1}{3}}$
	cos9thpiminplylem5.3	$⊢ A = Z + (\frac{1}{Z})$
	cos9thpiminply.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
	cos9thpiminply.4	$⊢ \underset{˙}{+} = +_{P}$
	cos9thpiminply.5	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	cos9thpiminply.6	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	cos9thpiminply.p	$⊢ P = {Poly}_{1} (Q)$
	cos9thpiminply.k	$⊢ K = algSc (P)$
	cos9thpiminply.x	$⊢ X = {var}_{1} (Q)$
	cos9thpiminply.d	$⊢ D = \deg_{1} (Q)$
	cos9thpiminply.f	$⊢ F = (3 \underset{˙}{\times} X) \underset{˙}{+} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1))$
	cos9thpiminply.m	$⊢ M = ℂ_{fld} minPoly ℚ$
Assertion	cos9thpiminply	$⊢ (F = M (A) \land D (F) = 3)$

Proof

Step	Hyp	Ref	Expression
1		cos9thpiminplylem3.1	$⊢ O = e^{\frac{i 2 π}{3}}$
2		cos9thpiminplylem4.2	$⊢ Z = O^{\frac{1}{3}}$
3		cos9thpiminplylem5.3	$⊢ A = Z + (\frac{1}{Z})$
4		cos9thpiminply.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
5		cos9thpiminply.4	$⊢ \underset{˙}{+} = +_{P}$
6		cos9thpiminply.5	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
7		cos9thpiminply.6	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
8		cos9thpiminply.p	$⊢ P = {Poly}_{1} (Q)$
9		cos9thpiminply.k	$⊢ K = algSc (P)$
10		cos9thpiminply.x	$⊢ X = {var}_{1} (Q)$
11		cos9thpiminply.d	$⊢ D = \deg_{1} (Q)$
12		cos9thpiminply.f	$⊢ F = (3 \underset{˙}{\times} X) \underset{˙}{+} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1))$
13		cos9thpiminply.m	$⊢ M = ℂ_{fld} minPoly ℚ$
14		eqid	$⊢ ℂ_{fld} {evalSub}_{1} ℚ = ℂ_{fld} {evalSub}_{1} ℚ$
15	4	fveq2i	$⊢ {Poly}_{1} (Q) = {Poly}_{1} (ℂ_{fld} ↾_{𝑠} ℚ)$
16	8 15	eqtri	$⊢ P = {Poly}_{1} (ℂ_{fld} ↾_{𝑠} ℚ)$
17		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
18		cnfldfld	$⊢ ℂ_{fld} \in Field$
19	18	a1i	$⊢ ⊤ \to ℂ_{fld} \in Field$
20		cndrng	$⊢ ℂ_{fld} \in DivRing$
21		qsubdrg	$⊢ (ℚ \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} ℚ \in DivRing)$
22	21	simpli	$⊢ ℚ \in SubRing (ℂ_{fld})$
23	21	simpri	$⊢ ℂ_{fld} ↾_{𝑠} ℚ \in DivRing$
24		issdrg	$⊢ ℚ \in SubDRing (ℂ_{fld}) \leftrightarrow (ℂ_{fld} \in DivRing \land ℚ \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} ℚ \in DivRing)$
25	20 22 23 24	mpbir3an	$⊢ ℚ \in SubDRing (ℂ_{fld})$
26	25	a1i	$⊢ ⊤ \to ℚ \in SubDRing (ℂ_{fld})$
27		ax-icn	$⊢ i \in ℂ$
28	27	a1i	$⊢ ⊤ \to i \in ℂ$
29		2cnd	$⊢ ⊤ \to 2 \in ℂ$
30		picn	$⊢ π \in ℂ$
31	30	a1i	$⊢ ⊤ \to π \in ℂ$
32	29 31	mulcld	$⊢ ⊤ \to 2 π \in ℂ$
33	28 32	mulcld	$⊢ ⊤ \to i 2 π \in ℂ$
34		3cn	$⊢ 3 \in ℂ$
35	34	a1i	$⊢ ⊤ \to 3 \in ℂ$
36		3ne0	$⊢ 3 \neq 0$
37	36	a1i	$⊢ ⊤ \to 3 \neq 0$
38	33 35 37	divcld	$⊢ ⊤ \to \frac{i 2 π}{3} \in ℂ$
39	38	efcld	$⊢ ⊤ \to e^{\frac{i 2 π}{3}} \in ℂ$
40	1 39	eqeltrid	$⊢ ⊤ \to O \in ℂ$
41	35 37	reccld	$⊢ ⊤ \to \frac{1}{3} \in ℂ$
42	40 41	cxpcld	$⊢ ⊤ \to O^{\frac{1}{3}} \in ℂ$
43	2 42	eqeltrid	$⊢ ⊤ \to Z \in ℂ$
44	2	a1i	$⊢ ⊤ \to Z = O^{\frac{1}{3}}$
45	1	a1i	$⊢ ⊤ \to O = e^{\frac{i 2 π}{3}}$
46	38	efne0d	$⊢ ⊤ \to e^{\frac{i 2 π}{3}} \neq 0$
47	45 46	eqnetrd	$⊢ ⊤ \to O \neq 0$
48	40 47 41	cxpne0d	$⊢ ⊤ \to O^{\frac{1}{3}} \neq 0$
49	44 48	eqnetrd	$⊢ ⊤ \to Z \neq 0$
50	43 49	reccld	$⊢ ⊤ \to \frac{1}{Z} \in ℂ$
51	43 50	addcld	$⊢ ⊤ \to Z + (\frac{1}{Z}) \in ℂ$
52	3 51	eqeltrid	$⊢ ⊤ \to A \in ℂ$
53		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
54		eqid	$⊢ 0_{P} = 0_{P}$
55	1 2 3 4 5 6 7 8 9 10 11 12 52	cos9thpiminplylem6	$⊢ ⊤ \to (ℂ_{fld} {evalSub}_{1} ℚ) (F) (A) = A^{3} + -3 A + 1$
56	1 2 3	cos9thpiminplylem5	$⊢ A^{3} + -3 A + 1 = 0$
57	55 56	eqtrdi	$⊢ ⊤ \to (ℂ_{fld} {evalSub}_{1} ℚ) (F) (A) = 0$
58	4	qrng0	$⊢ 0 = 0_{Q}$
59		eqid	$⊢ {eval}_{1} (Q) = {eval}_{1} (Q)$
60		eqid	$⊢ {Base}_{P} = {Base}_{P}$
61	4	qfld	$⊢ Q \in Field$
62	61	a1i	$⊢ ⊤ \to Q \in Field$
63	4	qdrng	$⊢ Q \in DivRing$
64	63	a1i	$⊢ ⊤ \to Q \in DivRing$
65	64	drngringd	$⊢ ⊤ \to Q \in Ring$
66	8	ply1ring	$⊢ Q \in Ring \to P \in Ring$
67	65 66	syl	$⊢ ⊤ \to P \in Ring$
68	67	ringgrpd	$⊢ ⊤ \to P \in Grp$
69		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
70	69 60	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
71	69	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
72	67 71	syl	$⊢ ⊤ \to {mulGrp}_{P} \in Mnd$
73		3nn0	$⊢ 3 \in ℕ_{0}$
74	73	a1i	$⊢ ⊤ \to 3 \in ℕ_{0}$
75	10 8 60	vr1cl	$⊢ Q \in Ring \to X \in {Base}_{P}$
76	65 75	syl	$⊢ ⊤ \to X \in {Base}_{P}$
77	70 7 72 74 76	mulgnn0cld	$⊢ ⊤ \to 3 \underset{˙}{\times} X \in {Base}_{P}$
78	8	ply1sca	$⊢ Q \in DivRing \to Q = Scalar (P)$
79	63 78	ax-mp	$⊢ Q = Scalar (P)$
80	8	ply1lmod	$⊢ Q \in Ring \to P \in LMod$
81	65 80	syl	$⊢ ⊤ \to P \in LMod$
82	4	qrngbas	$⊢ ℚ = {Base}_{Q}$
83	9 79 67 81 82 60	asclf	$⊢ ⊤ \to K : ℚ ⟶ {Base}_{P}$
84	74	nn0zd	$⊢ ⊤ \to 3 \in ℤ$
85		zq	$⊢ 3 \in ℤ \to 3 \in ℚ$
86		qnegcl	$⊢ 3 \in ℚ \to - 3 \in ℚ$
87	84 85 86	3syl	$⊢ ⊤ \to - 3 \in ℚ$
88	83 87	ffvelcdmd	$⊢ ⊤ \to K (- 3) \in {Base}_{P}$
89	60 6 67 88 76	ringcld	$⊢ ⊤ \to K (- 3) \underset{˙}{\cdot} X \in {Base}_{P}$
90		1zzd	$⊢ ⊤ \to 1 \in ℤ$
91		zq	$⊢ 1 \in ℤ \to 1 \in ℚ$
92	90 91	syl	$⊢ ⊤ \to 1 \in ℚ$
93	83 92	ffvelcdmd	$⊢ ⊤ \to K (1) \in {Base}_{P}$
94	60 5 68 89 93	grpcld	$⊢ ⊤ \to (K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1) \in {Base}_{P}$
95	60 5 68 77 94	grpcld	$⊢ ⊤ \to (3 \underset{˙}{\times} X) \underset{˙}{+} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1)) \in {Base}_{P}$
96	12 95	eqeltrid	$⊢ ⊤ \to F \in {Base}_{P}$
97	62	fldcrngd	$⊢ ⊤ \to Q \in CRing$
98	59 8 60 97 82 96	evl1fvf	$⊢ ⊤ \to {eval}_{1} (Q) (F) : ℚ ⟶ ℚ$
99	98	ffnd	$⊢ ⊤ \to {eval}_{1} (Q) (F) Fn ℚ$
100		fniniseg2	$⊢ {eval}_{1} (Q) (F) Fn ℚ \to {{eval}_{1} (Q) (F)}^{-1} [\{0\}] = \{x \in ℚ \| {eval}_{1} (Q) (F) (x) = 0\}$
101	99 100	syl	$⊢ ⊤ \to {{eval}_{1} (Q) (F)}^{-1} [\{0\}] = \{x \in ℚ \| {eval}_{1} (Q) (F) (x) = 0\}$
102	59 82	evl1fval1	$⊢ {eval}_{1} (Q) = Q {evalSub}_{1} ℚ$
103	102	a1i	$⊢ x \in ℚ \to {eval}_{1} (Q) = Q {evalSub}_{1} ℚ$
104	103	fveq1d	$⊢ x \in ℚ \to {eval}_{1} (Q) (F) = (Q {evalSub}_{1} ℚ) (F)$
105	104	fveq1d	$⊢ x \in ℚ \to {eval}_{1} (Q) (F) (x) = (Q {evalSub}_{1} ℚ) (F) (x)$
106		eqid	$⊢ Q {evalSub}_{1} ℚ = Q {evalSub}_{1} ℚ$
107		cncrng	$⊢ ℂ_{fld} \in CRing$
108	107	a1i	$⊢ x \in ℚ \to ℂ_{fld} \in CRing$
109	22	a1i	$⊢ x \in ℚ \to ℚ \in SubRing (ℂ_{fld})$
110	97	mptru	$⊢ Q \in CRing$
111	110	a1i	$⊢ x \in ℚ \to Q \in CRing$
112	111	crngringd	$⊢ x \in ℚ \to Q \in Ring$
113	82	subrgid	$⊢ Q \in Ring \to ℚ \in SubRing (Q)$
114	112 113	syl	$⊢ x \in ℚ \to ℚ \in SubRing (Q)$
115	96	mptru	$⊢ F \in {Base}_{P}$
116	115	a1i	$⊢ x \in ℚ \to F \in {Base}_{P}$
117	4 14 106 8 4 60 108 109 114 116	ressply1evls1	$⊢ x \in ℚ \to (Q {evalSub}_{1} ℚ) (F) = {(ℂ_{fld} {evalSub}_{1} ℚ) (F) ↾}_{ℚ}$
118	117	fveq1d	$⊢ x \in ℚ \to (Q {evalSub}_{1} ℚ) (F) (x) = ({(ℂ_{fld} {evalSub}_{1} ℚ) (F) ↾}_{ℚ}) (x)$
119		fvres	$⊢ x \in ℚ \to ({(ℂ_{fld} {evalSub}_{1} ℚ) (F) ↾}_{ℚ}) (x) = (ℂ_{fld} {evalSub}_{1} ℚ) (F) (x)$
120	118 119	eqtr2d	$⊢ x \in ℚ \to (ℂ_{fld} {evalSub}_{1} ℚ) (F) (x) = (Q {evalSub}_{1} ℚ) (F) (x)$
121		qcn	$⊢ x \in ℚ \to x \in ℂ$
122	1 2 3 4 5 6 7 8 9 10 11 12 121	cos9thpiminplylem6	$⊢ x \in ℚ \to (ℂ_{fld} {evalSub}_{1} ℚ) (F) (x) = x^{3} + -3 x + 1$
123	105 120 122	3eqtr2d	$⊢ x \in ℚ \to {eval}_{1} (Q) (F) (x) = x^{3} + -3 x + 1$
124		id	$⊢ x \in ℚ \to x \in ℚ$
125	124	cos9thpiminplylem2	$⊢ x \in ℚ \to x^{3} + -3 x + 1 \neq 0$
126	123 125	eqnetrd	$⊢ x \in ℚ \to {eval}_{1} (Q) (F) (x) \neq 0$
127	126	neneqd	$⊢ x \in ℚ \to \neg {eval}_{1} (Q) (F) (x) = 0$
128	127	rgen	$⊢ \forall x \in ℚ \neg {eval}_{1} (Q) (F) (x) = 0$
129	128	a1i	$⊢ ⊤ \to \forall x \in ℚ \neg {eval}_{1} (Q) (F) (x) = 0$
130		rabeq0	$⊢ \{x \in ℚ \| {eval}_{1} (Q) (F) (x) = 0\} = \emptyset \leftrightarrow \forall x \in ℚ \neg {eval}_{1} (Q) (F) (x) = 0$
131	129 130	sylibr	$⊢ ⊤ \to \{x \in ℚ \| {eval}_{1} (Q) (F) (x) = 0\} = \emptyset$
132	101 131	eqtrd	$⊢ ⊤ \to {{eval}_{1} (Q) (F)}^{-1} [\{0\}] = \emptyset$
133	12	a1i	$⊢ ⊤ \to F = (3 \underset{˙}{\times} X) \underset{˙}{+} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1))$
134	133	fveq2d	$⊢ ⊤ \to D (F) = D ((3 \underset{˙}{\times} X) \underset{˙}{+} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1)))$
135		1lt3	$⊢ 1 < 3$
136	135	a1i	$⊢ ⊤ \to 1 < 3$
137		0lt1	$⊢ 0 < 1$
138	137	a1i	$⊢ ⊤ \to 0 < 1$
139	138	gt0ne0d	$⊢ ⊤ \to 1 \neq 0$
140	11 8 82 9 58	deg1scl	$⊢ (Q \in Ring \land 1 \in ℚ \land 1 \neq 0) \to D (K (1)) = 0$
141	65 92 139 140	syl3anc	$⊢ ⊤ \to D (K (1)) = 0$
142		drngdomn	$⊢ Q \in DivRing \to Q \in Domn$
143	63 142	mp1i	$⊢ ⊤ \to Q \in Domn$
144	35 37	negne0d	$⊢ ⊤ \to - 3 \neq 0$
145	8 9 58 54 82	ply1scln0	$⊢ (Q \in Ring \land - 3 \in ℚ \land - 3 \neq 0) \to K (- 3) \neq 0_{P}$
146	65 87 144 145	syl3anc	$⊢ ⊤ \to K (- 3) \neq 0_{P}$
147	107	a1i	$⊢ ⊤ \to ℂ_{fld} \in CRing$
148		drngnzr	$⊢ ℂ_{fld} \in DivRing \to ℂ_{fld} \in NzRing$
149	20 148	mp1i	$⊢ ⊤ \to ℂ_{fld} \in NzRing$
150	22	a1i	$⊢ ⊤ \to ℚ \in SubRing (ℂ_{fld})$
151	10 54 4 8 147 149 150	vr1nz	$⊢ ⊤ \to X \neq 0_{P}$
152	11 8 60 6 54 143 88 146 76 151	deg1mul	$⊢ ⊤ \to D (K (- 3) \underset{˙}{\cdot} X) = D (K (- 3)) + D (X)$
153	11 8 82 9 58	deg1scl	$⊢ (Q \in Ring \land - 3 \in ℚ \land - 3 \neq 0) \to D (K (- 3)) = 0$
154	65 87 144 153	syl3anc	$⊢ ⊤ \to D (K (- 3)) = 0$
155		drngnzr	$⊢ Q \in DivRing \to Q \in NzRing$
156	63 155	mp1i	$⊢ ⊤ \to Q \in NzRing$
157	11 8 10 156	deg1vr	$⊢ ⊤ \to D (X) = 1$
158	154 157	oveq12d	$⊢ ⊤ \to D (K (- 3)) + D (X) = 0 + 1$
159		1cnd	$⊢ ⊤ \to 1 \in ℂ$
160	159	addlidd	$⊢ ⊤ \to 0 + 1 = 1$
161	152 158 160	3eqtrd	$⊢ ⊤ \to D (K (- 3) \underset{˙}{\cdot} X) = 1$
162	138 141 161	3brtr4d	$⊢ ⊤ \to D (K (1)) < D (K (- 3) \underset{˙}{\cdot} X)$
163	8 11 65 60 5 89 93 162	deg1add	$⊢ ⊤ \to D ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1)) = D (K (- 3) \underset{˙}{\cdot} X)$
164	163 161	eqtrd	$⊢ ⊤ \to D ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1)) = 1$
165	11 8 10 69 7	deg1pw	$⊢ (Q \in NzRing \land 3 \in ℕ_{0}) \to D (3 \underset{˙}{\times} X) = 3$
166	156 74 165	syl2anc	$⊢ ⊤ \to D (3 \underset{˙}{\times} X) = 3$
167	136 164 166	3brtr4d	$⊢ ⊤ \to D ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1)) < D (3 \underset{˙}{\times} X)$
168	8 11 65 60 5 77 94 167	deg1add	$⊢ ⊤ \to D ((3 \underset{˙}{\times} X) \underset{˙}{+} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1))) = D (3 \underset{˙}{\times} X)$
169	134 168 166	3eqtrd	$⊢ ⊤ \to D (F) = 3$
170	58 59 11 8 60 62 96 132 169	ply1dg3rt0irred	$⊢ ⊤ \to F \in Irred (P)$
171		eqid	$⊢ Irred (P) = Irred (P)$
172	171 54	irredn0	$⊢ (P \in Ring \land F \in Irred (P)) \to F \neq 0_{P}$
173	67 170 172	syl2anc	$⊢ ⊤ \to F \neq 0_{P}$
174	169	fveq2d	$⊢ ⊤ \to {coe}_{1} (F) (D (F)) = {coe}_{1} (F) (3)$
175	133	fveq2d	$⊢ ⊤ \to {coe}_{1} (F) = {coe}_{1} ((3 \underset{˙}{\times} X) \underset{˙}{+} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1)))$
176	175	fveq1d	$⊢ ⊤ \to {coe}_{1} (F) (3) = {coe}_{1} ((3 \underset{˙}{\times} X) \underset{˙}{+} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1))) (3)$
177		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
178	4 177	ressplusg	$⊢ ℚ \in SubRing (ℂ_{fld}) \to + = +_{Q}$
179	22 178	ax-mp	$⊢ + = +_{Q}$
180	8 60 5 179	coe1addfv	$⊢ ((Q \in Ring \land 3 \underset{˙}{\times} X \in {Base}_{P} \land (K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1) \in {Base}_{P}) \land 3 \in ℕ_{0}) \to {coe}_{1} ((3 \underset{˙}{\times} X) \underset{˙}{+} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1))) (3) = {coe}_{1} (3 \underset{˙}{\times} X) (3) + {coe}_{1} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1)) (3)$
181	65 77 94 74 180	syl31anc	$⊢ ⊤ \to {coe}_{1} ((3 \underset{˙}{\times} X) \underset{˙}{+} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1))) (3) = {coe}_{1} (3 \underset{˙}{\times} X) (3) + {coe}_{1} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1)) (3)$
182		iftrue	$⊢ i = 3 \to if (i = 3, 1, 0) = 1$
183	4	qrng1	$⊢ 1 = 1_{Q}$
184	8 10 7 65 74 58 183	coe1mon	$⊢ ⊤ \to {coe}_{1} (3 \underset{˙}{\times} X) = (i \in ℕ_{0} ⟼ if (i = 3, 1, 0))$
185	182 184 74 159	fvmptd4	$⊢ ⊤ \to {coe}_{1} (3 \underset{˙}{\times} X) (3) = 1$
186	8 60 5 179	coe1addfv	$⊢ ((Q \in Ring \land K (- 3) \underset{˙}{\cdot} X \in {Base}_{P} \land K (1) \in {Base}_{P}) \land 3 \in ℕ_{0}) \to {coe}_{1} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1)) (3) = {coe}_{1} (K (- 3) \underset{˙}{\cdot} X) (3) + {coe}_{1} (K (1)) (3)$
187	65 89 93 74 186	syl31anc	$⊢ ⊤ \to {coe}_{1} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1)) (3) = {coe}_{1} (K (- 3) \underset{˙}{\cdot} X) (3) + {coe}_{1} (K (1)) (3)$
188	8	ply1assa	$⊢ Q \in CRing \to P \in AssAlg$
189	97 188	syl	$⊢ ⊤ \to P \in AssAlg$
190		eqid	$⊢ \cdot_{P} = \cdot_{P}$
191	9 79 82 60 6 190	asclmul1	$⊢ (P \in AssAlg \land - 3 \in ℚ \land X \in {Base}_{P}) \to K (- 3) \underset{˙}{\cdot} X = -3 \cdot_{P} X$
192	189 87 76 191	syl3anc	$⊢ ⊤ \to K (- 3) \underset{˙}{\cdot} X = -3 \cdot_{P} X$
193	70 7	mulg1	$⊢ X \in {Base}_{P} \to 1 \underset{˙}{\times} X = X$
194	76 193	syl	$⊢ ⊤ \to 1 \underset{˙}{\times} X = X$
195	194	oveq2d	$⊢ ⊤ \to -3 \cdot_{P} (1 \underset{˙}{\times} X) = -3 \cdot_{P} X$
196	192 195	eqtr4d	$⊢ ⊤ \to K (- 3) \underset{˙}{\cdot} X = -3 \cdot_{P} (1 \underset{˙}{\times} X)$
197	196	fveq2d	$⊢ ⊤ \to {coe}_{1} (K (- 3) \underset{˙}{\cdot} X) = {coe}_{1} (-3 \cdot_{P} (1 \underset{˙}{\times} X))$
198	197	fveq1d	$⊢ ⊤ \to {coe}_{1} (K (- 3) \underset{˙}{\cdot} X) (3) = {coe}_{1} (-3 \cdot_{P} (1 \underset{˙}{\times} X)) (3)$
199		1nn0	$⊢ 1 \in ℕ_{0}$
200	199	a1i	$⊢ ⊤ \to 1 \in ℕ_{0}$
201		1red	$⊢ ⊤ \to 1 \in ℝ$
202	201 136	ltned	$⊢ ⊤ \to 1 \neq 3$
203	58 82 8 10 190 69 7 65 87 200 74 202	coe1tmfv2	$⊢ ⊤ \to {coe}_{1} (-3 \cdot_{P} (1 \underset{˙}{\times} X)) (3) = 0$
204	198 203	eqtrd	$⊢ ⊤ \to {coe}_{1} (K (- 3) \underset{˙}{\cdot} X) (3) = 0$
205	8 9 82 58	coe1scl	$⊢ (Q \in Ring \land 1 \in ℚ) \to {coe}_{1} (K (1)) = (i \in ℕ_{0} ⟼ if (i = 0, 1, 0))$
206	65 92 205	syl2anc	$⊢ ⊤ \to {coe}_{1} (K (1)) = (i \in ℕ_{0} ⟼ if (i = 0, 1, 0))$
207		simpr	$⊢ (⊤ \land i = 3) \to i = 3$
208	36	a1i	$⊢ (⊤ \land i = 3) \to 3 \neq 0$
209	207 208	eqnetrd	$⊢ (⊤ \land i = 3) \to i \neq 0$
210	209	neneqd	$⊢ (⊤ \land i = 3) \to \neg i = 0$
211	210	iffalsed	$⊢ (⊤ \land i = 3) \to if (i = 0, 1, 0) = 0$
212		0zd	$⊢ ⊤ \to 0 \in ℤ$
213	206 211 74 212	fvmptd	$⊢ ⊤ \to {coe}_{1} (K (1)) (3) = 0$
214	204 213	oveq12d	$⊢ ⊤ \to {coe}_{1} (K (- 3) \underset{˙}{\cdot} X) (3) + {coe}_{1} (K (1)) (3) = 0 + 0$
215		00id	$⊢ 0 + 0 = 0$
216	215	a1i	$⊢ ⊤ \to 0 + 0 = 0$
217	187 214 216	3eqtrd	$⊢ ⊤ \to {coe}_{1} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1)) (3) = 0$
218	185 217	oveq12d	$⊢ ⊤ \to {coe}_{1} (3 \underset{˙}{\times} X) (3) + {coe}_{1} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1)) (3) = 1 + 0$
219	159	addridd	$⊢ ⊤ \to 1 + 0 = 1$
220	218 219	eqtrd	$⊢ ⊤ \to {coe}_{1} (3 \underset{˙}{\times} X) (3) + {coe}_{1} ((K (- 3) \underset{˙}{\cdot} X) \underset{˙}{+} K (1)) (3) = 1$
221	176 181 220	3eqtrd	$⊢ ⊤ \to {coe}_{1} (F) (3) = 1$
222	174 221	eqtrd	$⊢ ⊤ \to {coe}_{1} (F) (D (F)) = 1$
223	4	fveq2i	$⊢ {Monic}_{1p} (Q) = {Monic}_{1p} (ℂ_{fld} ↾_{𝑠} ℚ)$
224	223	eqcomi	$⊢ {Monic}_{1p} (ℂ_{fld} ↾_{𝑠} ℚ) = {Monic}_{1p} (Q)$
225	8 60 54 11 224 183	ismon1p	$⊢ F \in {Monic}_{1p} (ℂ_{fld} ↾_{𝑠} ℚ) \leftrightarrow (F \in {Base}_{P} \land F \neq 0_{P} \land {coe}_{1} (F) (D (F)) = 1)$
226	96 173 222 225	syl3anbrc	$⊢ ⊤ \to F \in {Monic}_{1p} (ℂ_{fld} ↾_{𝑠} ℚ)$
227	14 16 17 19 26 52 53 13 54 57 170 226	irredminply	$⊢ ⊤ \to F = M (A)$
228	227 169	jca	$⊢ ⊤ \to (F = M (A) \land D (F) = 3)$
229	228	mptru	$⊢ (F = M (A) \land D (F) = 3)$

Metamath Proof Explorer

Theorem cos9thpiminply

Proof