Theorem 2sqr3minply

Description: The polynomial ( ( X ^ 3 ) - 2 ) is the minimal polynomial for ( 2 ^c ( 1 / 3 ) ) over QQ , and its degree is 3 . (Contributed by Thierry Arnoux, 14-Jun-2025)

	Ref	Expression
Hypotheses	2sqr3minply.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
	2sqr3minply.1	$$⊢\underset{\dot{}}{-}={-}_P$$
	2sqr3minply.2	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	2sqr3minply.p	$$⊢P={\mathrm{Poly}}_1\left(Q\right)$$
	2sqr3minply.k	$$⊢K=\mathrm{algSc}\left(P\right)$$
	2sqr3minply.x	$$⊢X={\mathrm{var}}_1\left(Q\right)$$
	2sqr3minply.d	$$⊢D={\mathrm{deg}}_1\left(Q\right)$$
	2sqr3minply.f	$$⊢F=\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)$$
	2sqr3minply.a	$$⊢A=2^{\frac{1}{3}}$$
	2sqr3minply.m	$$⊢M={ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}$$
Assertion	2sqr3minply	$$⊢\left(F=M\left(A\right)\wedge D\left(F\right)=3\right)$$

Proof

Step	Hyp	Ref	Expression
1		2sqr3minply.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
2		2sqr3minply.1	$$⊢\underset{\dot{}}{-}={-}_P$$
3		2sqr3minply.2	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
4		2sqr3minply.p	$$⊢P={\mathrm{Poly}}_1\left(Q\right)$$
5		2sqr3minply.k	$$⊢K=\mathrm{algSc}\left(P\right)$$
6		2sqr3minply.x	$$⊢X={\mathrm{var}}_1\left(Q\right)$$
7		2sqr3minply.d	$$⊢D={\mathrm{deg}}_1\left(Q\right)$$
8		2sqr3minply.f	$$⊢F=\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)$$
9		2sqr3minply.a	$$⊢A=2^{\frac{1}{3}}$$
10		2sqr3minply.m	$$⊢M={ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}$$
11		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}={ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}$$
12	1	fveq2i	$$⊢{\mathrm{Poly}}_1\left(Q\right)={\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
13	4 12	eqtri	$$⊢P={\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
14		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
15		cndrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
16		cncrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
17		isfld	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Field}\leftrightarrow \left({ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge {ℂ}_{\mathrm{fld}}\in \mathrm{CRing}\right)$$
18	15 16 17	mpbir2an	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Field}$$
19	18	a1i	$$⊢\top \to {ℂ}_{\mathrm{fld}}\in \mathrm{Field}$$
20		qsubdrg	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$
21	20	simpli	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
22	20	simpri	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}$$
23		issdrg	$$⊢\mathbb{Q}\in \mathrm{SubDRing}\left({ℂ}_{\mathrm{fld}}\right)\leftrightarrow \left({ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge \mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$
24	15 21 22 23	mpbir3an	$$⊢\mathbb{Q}\in \mathrm{SubDRing}\left({ℂ}_{\mathrm{fld}}\right)$$
25	24	a1i	$$⊢\top \to \mathbb{Q}\in \mathrm{SubDRing}\left({ℂ}_{\mathrm{fld}}\right)$$
26		2cn	$$⊢2\in ℂ$$
27		3cn	$$⊢3\in ℂ$$
28		3ne0	$$⊢3\ne 0$$
29	27 28	reccli	$$⊢\frac{1}{3}\in ℂ$$
30		cxpcl	$$⊢\left(2\in ℂ\wedge \frac{1}{3}\in ℂ\right)\to 2^{\frac{1}{3}}\in ℂ$$
31	26 29 30	mp2an	$$⊢2^{\frac{1}{3}}\in ℂ$$
32	9 31	eqeltri	$$⊢A\in ℂ$$
33	32	a1i	$$⊢\top \to A\in ℂ$$
34		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
35		eqid	$$⊢0_P=0_P$$
36	8	fveq2i	$$⊢\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(F\right)=\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)$$
37	36	fveq1i	$$⊢\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(F\right)\left(A\right)=\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(A\right)$$
38	37	a1i	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(F\right)\left(A\right)=\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(A\right)$$
39		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
40		cnfldsub	$$⊢-={-}_{{ℂ}_{\mathrm{fld}}}$$
41	16	a1i	$$⊢\top \to {ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
42	21	a1i	$$⊢\top \to \mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
43		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
44	43 39	mgpbas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_{{\mathrm{mulGrp}}_P}$$
45	1	qdrng	$$⊢Q\in \mathrm{DivRing}$$
46	45	a1i	$$⊢\top \to Q\in \mathrm{DivRing}$$
47	46	drngringd	$$⊢\top \to Q\in \mathrm{Ring}$$
48	4	ply1ring	$$⊢Q\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
49	47 48	syl	$$⊢\top \to P\in \mathrm{Ring}$$
50	43	ringmgp	$$⊢P\in \mathrm{Ring}\to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
51	49 50	syl	$$⊢\top \to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
52		3nn0	$$⊢3\in {\mathbb{N}}_0$$
53	52	a1i	$$⊢\top \to 3\in {\mathbb{N}}_0$$
54	6 4 39	vr1cl	$$⊢Q\in \mathrm{Ring}\to X\in {\mathrm{Base}}_P$$
55	47 54	syl	$$⊢\top \to X\in {\mathrm{Base}}_P$$
56	44 3 51 53 55	mulgnn0cld	$$⊢\top \to 3\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P$$
57	47	mptru	$$⊢Q\in \mathrm{Ring}$$
58	4	ply1sca	$$⊢Q\in \mathrm{Ring}\to Q=\mathrm{Scalar}\left(P\right)$$
59	57 58	ax-mp	$$⊢Q=\mathrm{Scalar}\left(P\right)$$
60	4	ply1lmod	$$⊢Q\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
61	47 60	syl	$$⊢\top \to P\in \mathrm{LMod}$$
62	1	qrngbas	$$⊢\mathbb{Q}={\mathrm{Base}}_Q$$
63	5 59 49 61 62 39	asclf	$$⊢\top \to K:\mathbb{Q}⟶{\mathrm{Base}}_P$$
64		2z	$$⊢2\in \mathbb{Z}$$
65		zq	$$⊢2\in \mathbb{Z}\to 2\in \mathbb{Q}$$
66	64 65	mp1i	$$⊢\top \to 2\in \mathbb{Q}$$
67	63 66	ffvelcdmd	$$⊢\top \to K\left(2\right)\in {\mathrm{Base}}_P$$
68	11 14 4 1 39 2 40 41 42 56 67 33	evls1subd	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(A\right)=\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(3\underset{\dot{}}{\times }X\right)\left(A\right)-\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(2\right)\right)\left(A\right)$$
69		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}={\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
70	11 14 4 1 39 41 42 3 69 53 55 33	evls1expd	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(3\underset{\dot{}}{\times }X\right)\left(A\right)=3{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(X\right)\left(A\right)$$
71	11 6 1 14 41 42	evls1var	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(X\right)={\mathrm{I}\upharpoonright }_{ℂ}$$
72	71	fveq1d	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(X\right)\left(A\right)=\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\left(A\right)$$
73		fvresi	$$⊢A\in ℂ\to \left({\mathrm{I}\upharpoonright }_{ℂ}\right)\left(A\right)=A$$
74	32 73	mp1i	$$⊢\top \to \left({\mathrm{I}\upharpoonright }_{ℂ}\right)\left(A\right)=A$$
75	72 74	eqtrd	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(X\right)\left(A\right)=A$$
76	75	oveq2d	$$⊢\top \to 3{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(X\right)\left(A\right)=3{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A$$
77		cnfldexp	$$⊢\left(A\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to 3{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^3$$
78	33 53 77	syl2anc	$$⊢\top \to 3{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}A=A^3$$
79	70 76 78	3eqtrd	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(3\underset{\dot{}}{\times }X\right)\left(A\right)=A^3$$
80	9	oveq1i	$$⊢A^3={\left(2^{\frac{1}{3}}\right)}^3$$
81		3nn	$$⊢3\in \mathbb{N}$$
82		cxproot	$$⊢\left(2\in ℂ\wedge 3\in \mathbb{N}\right)\to {\left(2^{\frac{1}{3}}\right)}^3=2$$
83	26 81 82	mp2an	$$⊢{\left(2^{\frac{1}{3}}\right)}^3=2$$
84	80 83	eqtri	$$⊢A^3=2$$
85	79 84	eqtrdi	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(3\underset{\dot{}}{\times }X\right)\left(A\right)=2$$
86	11 4 1 14 5 41 42 66 33	evls1scafv	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(2\right)\right)\left(A\right)=2$$
87	85 86	oveq12d	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(3\underset{\dot{}}{\times }X\right)\left(A\right)-\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(2\right)\right)\left(A\right)=2-2$$
88	26	subidi	$$⊢2-2=0$$
89	87 88	eqtrdi	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(3\underset{\dot{}}{\times }X\right)\left(A\right)-\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(2\right)\right)\left(A\right)=0$$
90	38 68 89	3eqtrd	$$⊢\top \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(F\right)\left(A\right)=0$$
91	1	qrng0	$$⊢0=0_Q$$
92		eqid	$$⊢{\mathrm{eval}}_1\left(Q\right)={\mathrm{eval}}_1\left(Q\right)$$
93		fldsdrgfld	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Field}\wedge \mathbb{Q}\in \mathrm{SubDRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{Field}$$
94	18 24 93	mp2an	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{Field}$$
95	1 94	eqeltri	$$⊢Q\in \mathrm{Field}$$
96	95	a1i	$$⊢\top \to Q\in \mathrm{Field}$$
97	49	ringgrpd	$$⊢\top \to P\in \mathrm{Grp}$$
98	39 2	grpsubcl	$$⊢\left(P\in \mathrm{Grp}\wedge 3\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P\wedge K\left(2\right)\in {\mathrm{Base}}_P\right)\to \left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\in {\mathrm{Base}}_P$$
99	97 56 67 98	syl3anc	$$⊢\top \to \left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\in {\mathrm{Base}}_P$$
100	8 99	eqeltrid	$$⊢\top \to F\in {\mathrm{Base}}_P$$
101	96	fldcrngd	$$⊢\top \to Q\in \mathrm{CRing}$$
102	92 4 39 101 62 100	evl1fvf	$$⊢\top \to {\mathrm{eval}}_1\left(Q\right)\left(F\right):\mathbb{Q}⟶\mathbb{Q}$$
103	102	ffnd	$$⊢\top \to {\mathrm{eval}}_1\left(Q\right)\left(F\right)Fn\mathbb{Q}$$
104		fniniseg2	$$⊢{\mathrm{eval}}_1\left(Q\right)\left(F\right)Fn\mathbb{Q}\to {{\mathrm{eval}}_1\left(Q\right)\left(F\right)}^{-1}\left[\left\{0\right\}\right]=\left\{x\in \mathbb{Q}|{\mathrm{eval}}_1\left(Q\right)\left(F\right)\left(x\right)=0\right\}$$
105	103 104	syl	$$⊢\top \to {{\mathrm{eval}}_1\left(Q\right)\left(F\right)}^{-1}\left[\left\{0\right\}\right]=\left\{x\in \mathbb{Q}|{\mathrm{eval}}_1\left(Q\right)\left(F\right)\left(x\right)=0\right\}$$
106		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
107	1 106	ressmulr	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \times ={\cdot }_Q$$
108	21 107	ax-mp	$$⊢\times ={\cdot }_Q$$
109		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
110	1 109	ressplusg	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to +={+}_Q$$
111	21 110	ax-mp	$$⊢+={+}_Q$$
112		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_Q}={\cdot }_{{\mathrm{mulGrp}}_Q}$$
113		eqid	$$⊢{\mathrm{coe}}_1\left(F\right)={\mathrm{coe}}_1\left(F\right)$$
114	8	fveq2i	$$⊢{\mathrm{coe}}_1\left(F\right)={\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)$$
115	114	a1i	$$⊢\top \to {\mathrm{coe}}_1\left(F\right)={\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)$$
116	8	fveq2i	$$⊢D\left(F\right)=D\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)$$
117	116	a1i	$$⊢\top \to D\left(F\right)=D\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)$$
118		3pos	$$⊢0<3$$
119	118	a1i	$$⊢\top \to 0<3$$
120		2ne0	$$⊢2\ne 0$$
121	120	a1i	$$⊢\top \to 2\ne 0$$
122	7 4 62 5 91	deg1scl	$$⊢\left(Q\in \mathrm{Ring}\wedge 2\in \mathbb{Q}\wedge 2\ne 0\right)\to D\left(K\left(2\right)\right)=0$$
123	47 66 121 122	syl3anc	$$⊢\top \to D\left(K\left(2\right)\right)=0$$
124		drngnzr	$$⊢Q\in \mathrm{DivRing}\to Q\in \mathrm{NzRing}$$
125	45 124	mp1i	$$⊢\top \to Q\in \mathrm{NzRing}$$
126	7 4 6 43 3	deg1pw	$$⊢\left(Q\in \mathrm{NzRing}\wedge 3\in {\mathbb{N}}_0\right)\to D\left(3\underset{\dot{}}{\times }X\right)=3$$
127	125 53 126	syl2anc	$$⊢\top \to D\left(3\underset{\dot{}}{\times }X\right)=3$$
128	119 123 127	3brtr4d	$$⊢\top \to D\left(K\left(2\right)\right)<D\left(3\underset{\dot{}}{\times }X\right)$$
129	4 7 47 39 2 56 67 128	deg1sub	$$⊢\top \to D\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)=D\left(3\underset{\dot{}}{\times }X\right)$$
130	117 129 127	3eqtrd	$$⊢\top \to D\left(F\right)=3$$
131	115 130	fveq12d	$$⊢\top \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)={\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(3\right)$$
132		eqid	$$⊢{-}_Q={-}_Q$$
133	4 39 2 132	coe1subfv	$$⊢\left(\left(Q\in \mathrm{Ring}\wedge 3\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P\wedge K\left(2\right)\in {\mathrm{Base}}_P\right)\wedge 3\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(3\right)={\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(3\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(3\right)$$
134	47 56 67 53 133	syl31anc	$$⊢\top \to {\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(3\right)={\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(3\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(3\right)$$
135		subrgsubg	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \mathbb{Q}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
136	21 135	mp1i	$$⊢\top \to \mathbb{Q}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
137		eqid	$$⊢{\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)={\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)$$
138	137 39 4 62	coe1fvalcl	$$⊢\left(3\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P\wedge 3\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(3\right)\in \mathbb{Q}$$
139	56 53 138	syl2anc	$$⊢\top \to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(3\right)\in \mathbb{Q}$$
140		eqid	$$⊢{\mathrm{coe}}_1\left(K\left(2\right)\right)={\mathrm{coe}}_1\left(K\left(2\right)\right)$$
141	140 39 4 62	coe1fvalcl	$$⊢\left(K\left(2\right)\in {\mathrm{Base}}_P\wedge 3\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(K\left(2\right)\right)\left(3\right)\in \mathbb{Q}$$
142	67 53 141	syl2anc	$$⊢\top \to {\mathrm{coe}}_1\left(K\left(2\right)\right)\left(3\right)\in \mathbb{Q}$$
143	40 1 132	subgsub	$$⊢\left(\mathbb{Q}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(3\right)\in \mathbb{Q}\wedge {\mathrm{coe}}_1\left(K\left(2\right)\right)\left(3\right)\in \mathbb{Q}\right)\to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(3\right)-{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(3\right)={\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(3\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(3\right)$$
144	136 139 142 143	syl3anc	$$⊢\top \to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(3\right)-{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(3\right)={\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(3\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(3\right)$$
145		iftrue	$$⊢i=3\to if\left(i=3,1,0\right)=1$$
146	1	qrng1	$$⊢1=1_Q$$
147	4 6 3 47 53 91 146	coe1mon	$$⊢\top \to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)=\left(i\in {\mathbb{N}}_0⟼if\left(i=3,1,0\right)\right)$$
148		1cnd	$$⊢\top \to 1\in ℂ$$
149	145 147 53 148	fvmptd4	$$⊢\top \to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(3\right)=1$$
150	28	neii	$$⊢\neg 3=0$$
151		eqeq1	$$⊢i=3\to \left(i=0\leftrightarrow 3=0\right)$$
152	150 151	mtbiri	$$⊢i=3\to \neg i=0$$
153	152	iffalsed	$$⊢i=3\to if\left(i=0,2,0\right)=0$$
154	4 5 62 91	coe1scl	$$⊢\left(Q\in \mathrm{Ring}\wedge 2\in \mathbb{Q}\right)\to {\mathrm{coe}}_1\left(K\left(2\right)\right)=\left(i\in {\mathbb{N}}_0⟼if\left(i=0,2,0\right)\right)$$
155	47 66 154	syl2anc	$$⊢\top \to {\mathrm{coe}}_1\left(K\left(2\right)\right)=\left(i\in {\mathbb{N}}_0⟼if\left(i=0,2,0\right)\right)$$
156		0nn0	$$⊢0\in {\mathbb{N}}_0$$
157	156	a1i	$$⊢\top \to 0\in {\mathbb{N}}_0$$
158	153 155 53 157	fvmptd4	$$⊢\top \to {\mathrm{coe}}_1\left(K\left(2\right)\right)\left(3\right)=0$$
159	149 158	oveq12d	$$⊢\top \to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(3\right)-{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(3\right)=1-0$$
160		1m0e1	$$⊢1-0=1$$
161	159 160	eqtrdi	$$⊢\top \to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(3\right)-{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(3\right)=1$$
162	144 161	eqtr3d	$$⊢\top \to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(3\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(3\right)=1$$
163	131 134 162	3eqtrd	$$⊢\top \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=1$$
164	130	fveq2d	$$⊢\top \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)={\mathrm{coe}}_1\left(F\right)\left(3\right)$$
165	163 164	eqtr3d	$$⊢\top \to 1={\mathrm{coe}}_1\left(F\right)\left(3\right)$$
166	165	mptru	$$⊢1={\mathrm{coe}}_1\left(F\right)\left(3\right)$$
167	115	fveq1d	$$⊢\top \to {\mathrm{coe}}_1\left(F\right)\left(2\right)={\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(2\right)$$
168		2nn0	$$⊢2\in {\mathbb{N}}_0$$
169	168	a1i	$$⊢\top \to 2\in {\mathbb{N}}_0$$
170	4 39 2 132	coe1subfv	$$⊢\left(\left(Q\in \mathrm{Ring}\wedge 3\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P\wedge K\left(2\right)\in {\mathrm{Base}}_P\right)\wedge 2\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(2\right)={\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(2\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(2\right)$$
171	47 56 67 169 170	syl31anc	$$⊢\top \to {\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(2\right)={\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(2\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(2\right)$$
172		2re	$$⊢2\in ℝ$$
173		2lt3	$$⊢2<3$$
174	172 173	ltneii	$$⊢2\ne 3$$
175		neeq1	$$⊢i=2\to \left(i\ne 3\leftrightarrow 2\ne 3\right)$$
176	174 175	mpbiri	$$⊢i=2\to i\ne 3$$
177	176	adantl	$$⊢\left(\top \wedge i=2\right)\to i\ne 3$$
178	177	neneqd	$$⊢\left(\top \wedge i=2\right)\to \neg i=3$$
179	178	iffalsed	$$⊢\left(\top \wedge i=2\right)\to if\left(i=3,1,0\right)=0$$
180	147 179 169 157	fvmptd	$$⊢\top \to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(2\right)=0$$
181		neeq1	$$⊢i=2\to \left(i\ne 0\leftrightarrow 2\ne 0\right)$$
182	120 181	mpbiri	$$⊢i=2\to i\ne 0$$
183	182	neneqd	$$⊢i=2\to \neg i=0$$
184	183	adantl	$$⊢\left(\top \wedge i=2\right)\to \neg i=0$$
185	184	iffalsed	$$⊢\left(\top \wedge i=2\right)\to if\left(i=0,2,0\right)=0$$
186	155 185 169 157	fvmptd	$$⊢\top \to {\mathrm{coe}}_1\left(K\left(2\right)\right)\left(2\right)=0$$
187	180 186	oveq12d	$$⊢\top \to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(2\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(2\right)=0{-}_{Q}0$$
188	171 187	eqtrd	$$⊢\top \to {\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(2\right)=0{-}_{Q}0$$
189	158 142	eqeltrrd	$$⊢\top \to 0\in \mathbb{Q}$$
190	40 1 132	subgsub	$$⊢\left(\mathbb{Q}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge 0\in \mathbb{Q}\wedge 0\in \mathbb{Q}\right)\to 0-0=0{-}_{Q}0$$
191	136 189 189 190	syl3anc	$$⊢\top \to 0-0=0{-}_{Q}0$$
192		0m0e0	$$⊢0-0=0$$
193	191 192	eqtr3di	$$⊢\top \to 0{-}_{Q}0=0$$
194	167 188 193	3eqtrrd	$$⊢\top \to 0={\mathrm{coe}}_1\left(F\right)\left(2\right)$$
195	194	mptru	$$⊢0={\mathrm{coe}}_1\left(F\right)\left(2\right)$$
196	115	fveq1d	$$⊢\top \to {\mathrm{coe}}_1\left(F\right)\left(1\right)={\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(1\right)$$
197		1nn0	$$⊢1\in {\mathbb{N}}_0$$
198	197	a1i	$$⊢\top \to 1\in {\mathbb{N}}_0$$
199	4 39 2 132	coe1subfv	$$⊢\left(\left(Q\in \mathrm{Ring}\wedge 3\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P\wedge K\left(2\right)\in {\mathrm{Base}}_P\right)\wedge 1\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(1\right)={\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(1\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(1\right)$$
200	47 56 67 198 199	syl31anc	$$⊢\top \to {\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(1\right)={\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(1\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(1\right)$$
201		1re	$$⊢1\in ℝ$$
202		1lt3	$$⊢1<3$$
203	201 202	ltneii	$$⊢1\ne 3$$
204		neeq1	$$⊢i=1\to \left(i\ne 3\leftrightarrow 1\ne 3\right)$$
205	203 204	mpbiri	$$⊢i=1\to i\ne 3$$
206	205	neneqd	$$⊢i=1\to \neg i=3$$
207	206	adantl	$$⊢\left(\top \wedge i=1\right)\to \neg i=3$$
208	207	iffalsed	$$⊢\left(\top \wedge i=1\right)\to if\left(i=3,1,0\right)=0$$
209	147 208 198 157	fvmptd	$$⊢\top \to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(1\right)=0$$
210		ax-1ne0	$$⊢1\ne 0$$
211		neeq1	$$⊢i=1\to \left(i\ne 0\leftrightarrow 1\ne 0\right)$$
212	210 211	mpbiri	$$⊢i=1\to i\ne 0$$
213	212	neneqd	$$⊢i=1\to \neg i=0$$
214	213	adantl	$$⊢\left(\top \wedge i=1\right)\to \neg i=0$$
215	214	iffalsed	$$⊢\left(\top \wedge i=1\right)\to if\left(i=0,2,0\right)=0$$
216	155 215 198 157	fvmptd	$$⊢\top \to {\mathrm{coe}}_1\left(K\left(2\right)\right)\left(1\right)=0$$
217	209 216	oveq12d	$$⊢\top \to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(1\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(1\right)=0{-}_{Q}0$$
218	200 217	eqtrd	$$⊢\top \to {\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(1\right)=0{-}_{Q}0$$
219	196 218 193	3eqtrrd	$$⊢\top \to 0={\mathrm{coe}}_1\left(F\right)\left(1\right)$$
220	219	mptru	$$⊢0={\mathrm{coe}}_1\left(F\right)\left(1\right)$$
221	115	fveq1d	$$⊢\top \to {\mathrm{coe}}_1\left(F\right)\left(0\right)={\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(0\right)$$
222	4 39 2 132	coe1subfv	$$⊢\left(\left(Q\in \mathrm{Ring}\wedge 3\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P\wedge K\left(2\right)\in {\mathrm{Base}}_P\right)\wedge 0\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(0\right)={\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(0\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(0\right)$$
223	47 56 67 157 222	syl31anc	$$⊢\top \to {\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(0\right)={\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(0\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(0\right)$$
224	28	necomi	$$⊢0\ne 3$$
225		neeq1	$$⊢i=0\to \left(i\ne 3\leftrightarrow 0\ne 3\right)$$
226	224 225	mpbiri	$$⊢i=0\to i\ne 3$$
227	226	neneqd	$$⊢i=0\to \neg i=3$$
228	227	adantl	$$⊢\left(\top \wedge i=0\right)\to \neg i=3$$
229	228	iffalsed	$$⊢\left(\top \wedge i=0\right)\to if\left(i=3,1,0\right)=0$$
230	147 229 157 157	fvmptd	$$⊢\top \to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(0\right)=0$$
231		simpr	$$⊢\left(\top \wedge i=0\right)\to i=0$$
232	231	iftrued	$$⊢\left(\top \wedge i=0\right)\to if\left(i=0,2,0\right)=2$$
233	155 232 157 169	fvmptd	$$⊢\top \to {\mathrm{coe}}_1\left(K\left(2\right)\right)\left(0\right)=2$$
234	230 233	oveq12d	$$⊢\top \to {\mathrm{coe}}_1\left(3\underset{\dot{}}{\times }X\right)\left(0\right){-}_Q{\mathrm{coe}}_1\left(K\left(2\right)\right)\left(0\right)=0{-}_{Q}2$$
235	223 234	eqtrd	$$⊢\top \to {\mathrm{coe}}_1\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{-}K\left(2\right)\right)\left(0\right)=0{-}_{Q}2$$
236		df-neg	$$⊢-2=0-2$$
237	40 1 132	subgsub	$$⊢\left(\mathbb{Q}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge 0\in \mathbb{Q}\wedge 2\in \mathbb{Q}\right)\to 0-2=0{-}_{Q}2$$
238	136 189 66 237	syl3anc	$$⊢\top \to 0-2=0{-}_{Q}2$$
239	236 238	eqtr2id	$$⊢\top \to 0{-}_{Q}2=-2$$
240	221 235 239	3eqtrrd	$$⊢\top \to -2={\mathrm{coe}}_1\left(F\right)\left(0\right)$$
241	240	mptru	$$⊢-2={\mathrm{coe}}_1\left(F\right)\left(0\right)$$
242	95	a1i	$$⊢x\in \mathbb{Q}\to Q\in \mathrm{Field}$$
243	242	fldcrngd	$$⊢x\in \mathbb{Q}\to Q\in \mathrm{CRing}$$
244	100	mptru	$$⊢F\in {\mathrm{Base}}_P$$
245	244	a1i	$$⊢x\in \mathbb{Q}\to F\in {\mathrm{Base}}_P$$
246	130	mptru	$$⊢D\left(F\right)=3$$
247	246	a1i	$$⊢x\in \mathbb{Q}\to D\left(F\right)=3$$
248		id	$$⊢x\in \mathbb{Q}\to x\in \mathbb{Q}$$
249	4 92 62 39 108 111 112 113 7 166 195 220 241 243 245 247 248	evl1deg3	$$⊢x\in \mathbb{Q}\to {\mathrm{eval}}_1\left(Q\right)\left(F\right)\left(x\right)=1\left(3{\cdot }_{{\mathrm{mulGrp}}_Q}x\right)+0\cdot \left(2{\cdot }_{{\mathrm{mulGrp}}_Q}x\right)+0\cdot x+-2$$
250		qsscn	$$⊢\mathbb{Q}\subseteq ℂ$$
251		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Q}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
252		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
253	252 14	mgpbas	$$⊢ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
254	251 253	ressbas2	$$⊢\mathbb{Q}\subseteq ℂ\to \mathbb{Q}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}$$
255	250 254	ax-mp	$$⊢\mathbb{Q}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}$$
256	1 252	mgpress	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}\wedge \mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Q}={\mathrm{mulGrp}}_Q$$
257	15 21 256	mp2an	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Q}={\mathrm{mulGrp}}_Q$$
258	257	fveq2i	$$⊢{\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}={\mathrm{Base}}_{{\mathrm{mulGrp}}_Q}$$
259	255 258	eqtri	$$⊢\mathbb{Q}={\mathrm{Base}}_{{\mathrm{mulGrp}}_Q}$$
260		eqid	$$⊢{\mathrm{mulGrp}}_Q={\mathrm{mulGrp}}_Q$$
261	260	ringmgp	$$⊢Q\in \mathrm{Ring}\to {\mathrm{mulGrp}}_Q\in \mathrm{Mnd}$$
262	57 261	mp1i	$$⊢x\in \mathbb{Q}\to {\mathrm{mulGrp}}_Q\in \mathrm{Mnd}$$
263	52	a1i	$$⊢x\in \mathbb{Q}\to 3\in {\mathbb{N}}_0$$
264	259 112 262 263 248	mulgnn0cld	$$⊢x\in \mathbb{Q}\to 3{\cdot }_{{\mathrm{mulGrp}}_Q}x\in \mathbb{Q}$$
265	250 264	sselid	$$⊢x\in \mathbb{Q}\to 3{\cdot }_{{\mathrm{mulGrp}}_Q}x\in ℂ$$
266	265	mullidd	$$⊢x\in \mathbb{Q}\to 1\left(3{\cdot }_{{\mathrm{mulGrp}}_Q}x\right)=3{\cdot }_{{\mathrm{mulGrp}}_Q}x$$
267	257	eqcomi	$$⊢{\mathrm{mulGrp}}_Q={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
268	250 253	sseqtri	$$⊢\mathbb{Q}\subseteq {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
269	268	a1i	$$⊢x\in \mathbb{Q}\to \mathbb{Q}\subseteq {\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
270	81	a1i	$$⊢x\in \mathbb{Q}\to 3\in \mathbb{N}$$
271	267 269 248 270	ressmulgnnd	$$⊢x\in \mathbb{Q}\to 3{\cdot }_{{\mathrm{mulGrp}}_Q}x=3{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}x$$
272		qcn	$$⊢x\in \mathbb{Q}\to x\in ℂ$$
273		cnfldexp	$$⊢\left(x\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to 3{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}x=x^3$$
274	272 263 273	syl2anc	$$⊢x\in \mathbb{Q}\to 3{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}x=x^3$$
275	266 271 274	3eqtrd	$$⊢x\in \mathbb{Q}\to 1\left(3{\cdot }_{{\mathrm{mulGrp}}_Q}x\right)=x^3$$
276	168	a1i	$$⊢x\in \mathbb{Q}\to 2\in {\mathbb{N}}_0$$
277	259 112 262 276 248	mulgnn0cld	$$⊢x\in \mathbb{Q}\to 2{\cdot }_{{\mathrm{mulGrp}}_Q}x\in \mathbb{Q}$$
278	250 277	sselid	$$⊢x\in \mathbb{Q}\to 2{\cdot }_{{\mathrm{mulGrp}}_Q}x\in ℂ$$
279	278	mul02d	$$⊢x\in \mathbb{Q}\to 0\cdot \left(2{\cdot }_{{\mathrm{mulGrp}}_Q}x\right)=0$$
280	275 279	oveq12d	$$⊢x\in \mathbb{Q}\to 1\left(3{\cdot }_{{\mathrm{mulGrp}}_Q}x\right)+0\cdot \left(2{\cdot }_{{\mathrm{mulGrp}}_Q}x\right)=x^3+0$$
281	272 263	expcld	$$⊢x\in \mathbb{Q}\to x^3\in ℂ$$
282	281	addridd	$$⊢x\in \mathbb{Q}\to x^3+0=x^3$$
283	280 282	eqtrd	$$⊢x\in \mathbb{Q}\to 1\left(3{\cdot }_{{\mathrm{mulGrp}}_Q}x\right)+0\cdot \left(2{\cdot }_{{\mathrm{mulGrp}}_Q}x\right)=x^3$$
284	272	mul02d	$$⊢x\in \mathbb{Q}\to 0\cdot x=0$$
285	284	oveq1d	$$⊢x\in \mathbb{Q}\to 0\cdot x+-2=0+-2$$
286	26	a1i	$$⊢x\in \mathbb{Q}\to 2\in ℂ$$
287	286	negcld	$$⊢x\in \mathbb{Q}\to -2\in ℂ$$
288	287	addlidd	$$⊢x\in \mathbb{Q}\to 0+-2=-2$$
289	285 288	eqtrd	$$⊢x\in \mathbb{Q}\to 0\cdot x+-2=-2$$
290	283 289	oveq12d	$$⊢x\in \mathbb{Q}\to 1\left(3{\cdot }_{{\mathrm{mulGrp}}_Q}x\right)+0\cdot \left(2{\cdot }_{{\mathrm{mulGrp}}_Q}x\right)+0\cdot x+-2=x^3+-2$$
291	281 286	negsubd	$$⊢x\in \mathbb{Q}\to x^3+-2=x^3-2$$
292	249 290 291	3eqtrd	$$⊢x\in \mathbb{Q}\to {\mathrm{eval}}_1\left(Q\right)\left(F\right)\left(x\right)=x^3-2$$
293		2prm	$$⊢2\in \mathbb{P}$$
294		3z	$$⊢3\in \mathbb{Z}$$
295		3re	$$⊢3\in ℝ$$
296	172 295 173	ltleii	$$⊢2\le 3$$
297	64	eluz1i	$$⊢3\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(3\in \mathbb{Z}\wedge 2\le 3\right)$$
298	294 296 297	mpbir2an	$$⊢3\in {\mathbb{Z}}_{\ge 2}$$
299		rtprmirr	$$⊢\left(2\in \mathbb{P}\wedge 3\in {\mathbb{Z}}_{\ge 2}\right)\to 2^{\frac{1}{3}}\in \left(ℝ\setminus \mathbb{Q}\right)$$
300	293 298 299	mp2an	$$⊢2^{\frac{1}{3}}\in \left(ℝ\setminus \mathbb{Q}\right)$$
301		eldifn	$$⊢2^{\frac{1}{3}}\in \left(ℝ\setminus \mathbb{Q}\right)\to \neg 2^{\frac{1}{3}}\in \mathbb{Q}$$
302	300 301	ax-mp	$$⊢\neg 2^{\frac{1}{3}}\in \mathbb{Q}$$
303		nelne2	$$⊢\left(x\in \mathbb{Q}\wedge \neg 2^{\frac{1}{3}}\in \mathbb{Q}\right)\to x\ne 2^{\frac{1}{3}}$$
304	302 303	mpan2	$$⊢x\in \mathbb{Q}\to x\ne 2^{\frac{1}{3}}$$
305		qre	$$⊢x\in \mathbb{Q}\to x\in ℝ$$
306	305	adantr	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to x\in ℝ$$
307		2pos	$$⊢0<2$$
308	281 286	subeq0ad	$$⊢x\in \mathbb{Q}\to \left(x^3-2=0\leftrightarrow x^3=2\right)$$
309	308	biimpa	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to x^3=2$$
310	307 309	breqtrrid	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to 0<x^3$$
311	81	a1i	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to 3\in \mathbb{N}$$
312		n2dvds3	$$⊢\neg 2\parallel 3$$
313	312	a1i	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to \neg 2\parallel 3$$
314	306 311 313	expgt0b	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to \left(0<x\leftrightarrow 0<x^3\right)$$
315	310 314	mpbird	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to 0<x$$
316	306 315	elrpd	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to x\in {ℝ}^{+}$$
317	295	a1i	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to 3\in ℝ$$
318	29	a1i	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to \frac{1}{3}\in ℂ$$
319	316 317 318	cxpmuld	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to x^{3\left(\frac{1}{3}\right)}={\left(x^3\right)}^{\frac{1}{3}}$$
320	27	a1i	$$⊢x\in \mathbb{Q}\to 3\in ℂ$$
321	28	a1i	$$⊢x\in \mathbb{Q}\to 3\ne 0$$
322	320 321	recidd	$$⊢x\in \mathbb{Q}\to 3\left(\frac{1}{3}\right)=1$$
323	322	oveq2d	$$⊢x\in \mathbb{Q}\to x^{3\left(\frac{1}{3}\right)}=x^1$$
324	272	cxp1d	$$⊢x\in \mathbb{Q}\to x^1=x$$
325	323 324	eqtrd	$$⊢x\in \mathbb{Q}\to x^{3\left(\frac{1}{3}\right)}=x$$
326	325	adantr	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to x^{3\left(\frac{1}{3}\right)}=x$$
327		cxpexp	$$⊢\left(x\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to x^3=x^3$$
328	272 263 327	syl2anc	$$⊢x\in \mathbb{Q}\to x^3=x^3$$
329	328	oveq1d	$$⊢x\in \mathbb{Q}\to {\left(x^3\right)}^{\frac{1}{3}}={\left(x^3\right)}^{\frac{1}{3}}$$
330	329	adantr	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to {\left(x^3\right)}^{\frac{1}{3}}={\left(x^3\right)}^{\frac{1}{3}}$$
331	319 326 330	3eqtr3rd	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to {\left(x^3\right)}^{\frac{1}{3}}=x$$
332	309	oveq1d	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to {\left(x^3\right)}^{\frac{1}{3}}=2^{\frac{1}{3}}$$
333	331 332	eqtr3d	$$⊢\left(x\in \mathbb{Q}\wedge x^3-2=0\right)\to x=2^{\frac{1}{3}}$$
334	304 333	mteqand	$$⊢x\in \mathbb{Q}\to x^3-2\ne 0$$
335	292 334	eqnetrd	$$⊢x\in \mathbb{Q}\to {\mathrm{eval}}_1\left(Q\right)\left(F\right)\left(x\right)\ne 0$$
336	335	neneqd	$$⊢x\in \mathbb{Q}\to \neg {\mathrm{eval}}_1\left(Q\right)\left(F\right)\left(x\right)=0$$
337	336	rgen	$$⊢\forall x\in \mathbb{Q}\neg {\mathrm{eval}}_1\left(Q\right)\left(F\right)\left(x\right)=0$$
338	337	a1i	$$⊢\top \to \forall x\in \mathbb{Q}\neg {\mathrm{eval}}_1\left(Q\right)\left(F\right)\left(x\right)=0$$
339		rabeq0	$$⊢\left\{x\in \mathbb{Q}|{\mathrm{eval}}_1\left(Q\right)\left(F\right)\left(x\right)=0\right\}=\varnothing \leftrightarrow \forall x\in \mathbb{Q}\neg {\mathrm{eval}}_1\left(Q\right)\left(F\right)\left(x\right)=0$$
340	338 339	sylibr	$$⊢\top \to \left\{x\in \mathbb{Q}|{\mathrm{eval}}_1\left(Q\right)\left(F\right)\left(x\right)=0\right\}=\varnothing$$
341	105 340	eqtrd	$$⊢\top \to {{\mathrm{eval}}_1\left(Q\right)\left(F\right)}^{-1}\left[\left\{0\right\}\right]=\varnothing$$
342	91 92 7 4 39 96 100 341 130	ply1dg3rt0irred	$$⊢\top \to F\in \mathrm{Irred}\left(P\right)$$
343		eqid	$$⊢\mathrm{Irred}\left(P\right)=\mathrm{Irred}\left(P\right)$$
344	343 35	irredn0	$$⊢\left(P\in \mathrm{Ring}\wedge F\in \mathrm{Irred}\left(P\right)\right)\to F\ne 0_P$$
345	49 342 344	syl2anc	$$⊢\top \to F\ne 0_P$$
346	1	fveq2i	$$⊢{\mathrm{deg}}_1\left(Q\right)={\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
347	7 346	eqtri	$$⊢D={\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
348		eqid	$$⊢{Monic}_{\mathrm{1p}}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)={Monic}_{\mathrm{1p}}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
349		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
350	349	qrng1	$$⊢1=1_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}$$
351	13 39 35 347 348 350	ismon1p	$$⊢F\in {Monic}_{\mathrm{1p}}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\leftrightarrow \left(F\in {\mathrm{Base}}_P\wedge F\ne 0_P\wedge {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=1\right)$$
352	100 345 163 351	syl3anbrc	$$⊢\top \to F\in {Monic}_{\mathrm{1p}}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
353	11 13 14 19 25 33 34 10 35 90 342 352	irredminply	$$⊢\top \to F=M\left(A\right)$$
354	353 130	jca	$$⊢\top \to \left(F=M\left(A\right)\wedge D\left(F\right)=3\right)$$
355	354	mptru	$$⊢\left(F=M\left(A\right)\wedge D\left(F\right)=3\right)$$