Theorem constrcon

Description: Contradiction of constuctibility: If a complex number A has minimal polynomial F over QQ of a degree that is not a power of 2 , then A is not constructible. (Contributed by Thierry Arnoux, 26-Oct-2025)

	Ref	Expression
Hypotheses	constrcon.d	$$⊢D={\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
	constrcon.m	$$⊢M={ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}$$
	constrcon.a	$$⊢\phi \to A\in ℂ$$
	constrcon.f	$$⊢\phi \to F=M\left(A\right)$$
	constrcon.1	$$⊢\phi \to D\left(F\right)\in {\mathbb{N}}_0$$
	constrcon.2	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to D\left(F\right)\ne 2^n$$
Assertion	constrcon	$$⊢\phi \to \neg A\in \mathrm{Constr}$$

Proof

Step	Hyp	Ref	Expression
1		constrcon.d	$$⊢D={\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
2		constrcon.m	$$⊢M={ℂ}_{\mathrm{fld}}\mathrm{minPoly}\mathbb{Q}$$
3		constrcon.a	$$⊢\phi \to A\in ℂ$$
4		constrcon.f	$$⊢\phi \to F=M\left(A\right)$$
5		constrcon.1	$$⊢\phi \to D\left(F\right)\in {\mathbb{N}}_0$$
6		constrcon.2	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to D\left(F\right)\ne 2^n$$
7	6	neneqd	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \neg D\left(F\right)=2^n$$
8		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
9		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\left({ℂ}_{\mathrm{fld}}\mathrm{fldGen}\left(\mathbb{Q}\cup \left\{A\right\}\right)\right)={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\left({ℂ}_{\mathrm{fld}}\mathrm{fldGen}\left(\mathbb{Q}\cup \left\{A\right\}\right)\right)$$
10		eqid	$$⊢{\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}\right)={\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}\right)$$
11		cnfldfld	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Field}$$
12	11	a1i	$$⊢\phi \to {ℂ}_{\mathrm{fld}}\in \mathrm{Field}$$
13		cndrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
14		qsubdrg	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$
15	14	simpli	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
16	8	qdrng	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}$$
17		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)$$
18	13 15 16 17	mpbir3an	$$⊢\mathbb{Q}\in \mathrm{SubDRing}\left({ℂ}_{\mathrm{fld}}\right)$$
19	18	a1i	$$⊢\phi \to \mathbb{Q}\in \mathrm{SubDRing}\left({ℂ}_{\mathrm{fld}}\right)$$
20		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
21		eqidd	$$⊢\phi \to D=D$$
22	21 4	fveq12d	$$⊢\phi \to D\left(F\right)=D\left(M\left(A\right)\right)$$
23	22 5	eqeltrrd	$$⊢\phi \to D\left(M\left(A\right)\right)\in {\mathbb{N}}_0$$
24	20 2 1 12 19 3 23	minplyelirng	$$⊢\phi \to A\in \left({ℂ}_{\mathrm{fld}}\mathrm{IntgRing}\mathbb{Q}\right)$$
25	8 9 10 2 12 19 24	algextdeg	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\left({ℂ}_{\mathrm{fld}}\mathrm{fldGen}\left(\mathbb{Q}\cup \left\{A\right\}\right)\right)\right)\left[.:.\right]\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)={\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}\right)\left(M\left(A\right)\right)$$
26		eqid	$$⊢{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)={\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
27		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}$$
28		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}={ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}$$
29		eqid	$$⊢0_{{ℂ}_{\mathrm{fld}}}=0_{{ℂ}_{\mathrm{fld}}}$$
30		eqid	$$⊢\left\{q\in \mathrm{dom}\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)|\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(q\right)\left(A\right)=0_{{ℂ}_{\mathrm{fld}}}\right\}=\left\{q\in \mathrm{dom}\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)|\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(q\right)\left(A\right)=0_{{ℂ}_{\mathrm{fld}}}\right\}$$
31		eqid	$$⊢\mathrm{RSpan}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)=\mathrm{RSpan}\left({\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\right)$$
32		eqid	$$⊢{idlGen}_{\mathrm{1p}}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)={idlGen}_{\mathrm{1p}}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)$$
33	28 26 20 12 19 3 29 30 31 32 2	minplycl	$$⊢\phi \to M\left(A\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)}$$
34	15	a1i	$$⊢\phi \to \mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
35	8 10 26 27 33 34	ressdeg1	$$⊢\phi \to {\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}\right)\left(M\left(A\right)\right)={\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(M\left(A\right)\right)$$
36	1 21	eqtr3id	$$⊢\phi \to {\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)=D$$
37	4	eqcomd	$$⊢\phi \to M\left(A\right)=F$$
38	36 37	fveq12d	$$⊢\phi \to {\mathrm{deg}}_1\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)\left(M\left(A\right)\right)=D\left(F\right)$$
39	25 35 38	3eqtrd	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\left({ℂ}_{\mathrm{fld}}\mathrm{fldGen}\left(\mathbb{Q}\cup \left\{A\right\}\right)\right)\right)\left[.:.\right]\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)=D\left(F\right)$$
40	39	eqeq1d	$$⊢\phi \to \left(\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\left({ℂ}_{\mathrm{fld}}\mathrm{fldGen}\left(\mathbb{Q}\cup \left\{A\right\}\right)\right)\right)\left[.:.\right]\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)=2^n\leftrightarrow D\left(F\right)=2^n\right)$$
41	40	adantr	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \left(\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\left({ℂ}_{\mathrm{fld}}\mathrm{fldGen}\left(\mathbb{Q}\cup \left\{A\right\}\right)\right)\right)\left[.:.\right]\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)=2^n\leftrightarrow D\left(F\right)=2^n\right)$$
42	7 41	mtbird	$$⊢\left(\phi \wedge n\in {\mathbb{N}}_0\right)\to \neg \left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\left({ℂ}_{\mathrm{fld}}\mathrm{fldGen}\left(\mathbb{Q}\cup \left\{A\right\}\right)\right)\right)\left[.:.\right]\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)=2^n$$
43	42	nrexdv	$$⊢\phi \to \neg \exists n\in {\mathbb{N}}_0\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\left({ℂ}_{\mathrm{fld}}\mathrm{fldGen}\left(\mathbb{Q}\cup \left\{A\right\}\right)\right)\right)\left[.:.\right]\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)=2^n$$
44		eqid	$$⊢{ℂ}_{\mathrm{fld}}\mathrm{fldGen}\left(\mathbb{Q}\cup \left\{A\right\}\right)={ℂ}_{\mathrm{fld}}\mathrm{fldGen}\left(\mathbb{Q}\cup \left\{A\right\}\right)$$
45		simpr	$$⊢\left(\phi \wedge A\in \mathrm{Constr}\right)\to A\in \mathrm{Constr}$$
46	8 9 44 45	constrext2chn	$$⊢\left(\phi \wedge A\in \mathrm{Constr}\right)\to \exists n\in {\mathbb{N}}_0\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\left({ℂ}_{\mathrm{fld}}\mathrm{fldGen}\left(\mathbb{Q}\cup \left\{A\right\}\right)\right)\right)\left[.:.\right]\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\right)=2^n$$
47	43 46	mtand	$$⊢\phi \to \neg A\in \mathrm{Constr}$$