Theorem constrcon

Description: Contradiction of constructibility: 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	⊢ 𝐷 = ( deg1 ‘ ( ℂfld ↾s ℚ ) )
	constrcon.m	⊢ 𝑀 = ( ℂfld minPoly ℚ )
	constrcon.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	constrcon.f	⊢ ( 𝜑 → 𝐹 = ( 𝑀 ‘ 𝐴 ) )
	constrcon.1	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
	constrcon.2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐷 ‘ 𝐹 ) ≠ ( 2 ↑ 𝑛 ) )
Assertion	constrcon	⊢ ( 𝜑 → ¬ 𝐴 ∈ Constr )

Proof

Step	Hyp	Ref	Expression
1		constrcon.d	⊢ 𝐷 = ( deg1 ‘ ( ℂfld ↾s ℚ ) )
2		constrcon.m	⊢ 𝑀 = ( ℂfld minPoly ℚ )
3		constrcon.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4		constrcon.f	⊢ ( 𝜑 → 𝐹 = ( 𝑀 ‘ 𝐴 ) )
5		constrcon.1	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
6		constrcon.2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐷 ‘ 𝐹 ) ≠ ( 2 ↑ 𝑛 ) )
7	6	neneqd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ¬ ( 𝐷 ‘ 𝐹 ) = ( 2 ↑ 𝑛 ) )
8		eqid	⊢ ( ℂfld ↾s ℚ ) = ( ℂfld ↾s ℚ )
9		eqid	⊢ ( ℂfld ↾s ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) ) ) = ( ℂfld ↾s ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) ) )
10		eqid	⊢ ( deg1 ‘ ℂfld ) = ( deg1 ‘ ℂfld )
11		cnfldfld	⊢ ℂfld ∈ Field
12	11	a1i	⊢ ( 𝜑 → ℂfld ∈ Field )
13		cndrng	⊢ ℂfld ∈ DivRing
14		qsubdrg	⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing )
15	14	simpli	⊢ ℚ ∈ ( SubRing ‘ ℂfld )
16	8	qdrng	⊢ ( ℂfld ↾s ℚ ) ∈ DivRing
17		issdrg	⊢ ( ℚ ∈ ( SubDRing ‘ ℂfld ) ↔ ( ℂfld ∈ DivRing ∧ ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing ) )
18	13 15 16 17	mpbir3an	⊢ ℚ ∈ ( SubDRing ‘ ℂfld )
19	18	a1i	⊢ ( 𝜑 → ℚ ∈ ( SubDRing ‘ ℂfld ) )
20		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
21		eqidd	⊢ ( 𝜑 → 𝐷 = 𝐷 )
22	21 4	fveq12d	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) )
23	22 5	eqeltrrd	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ∈ ℕ0 )
24	20 2 1 12 19 3 23	minplyelirng	⊢ ( 𝜑 → 𝐴 ∈ ( ℂfld IntgRing ℚ ) )
25	8 9 10 2 12 19 24	algextdeg	⊢ ( 𝜑 → ( ( ℂfld ↾s ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂfld ↾s ℚ ) ) = ( ( deg1 ‘ ℂfld ) ‘ ( 𝑀 ‘ 𝐴 ) ) )
26		eqid	⊢ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) = ( Poly1 ‘ ( ℂfld ↾s ℚ ) )
27		eqid	⊢ ( Base ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) = ( Base ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) )
28		eqid	⊢ ( ℂfld evalSub1 ℚ ) = ( ℂfld evalSub1 ℚ )
29		eqid	⊢ ( 0g ‘ ℂfld ) = ( 0g ‘ ℂfld )
30		eqid	⊢ { 𝑞 ∈ dom ( ℂfld evalSub1 ℚ ) ∣ ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ ℂfld ) } = { 𝑞 ∈ dom ( ℂfld evalSub1 ℚ ) ∣ ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ ℂfld ) }
31		eqid	⊢ ( RSpan ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) = ( RSpan ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) )
32		eqid	⊢ ( idlGen1p ‘ ( ℂfld ↾s ℚ ) ) = ( idlGen1p ‘ ( ℂfld ↾s ℚ ) )
33	28 26 20 12 19 3 29 30 31 32 2	minplycl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) )
34	15	a1i	⊢ ( 𝜑 → ℚ ∈ ( SubRing ‘ ℂfld ) )
35	8 10 26 27 33 34	ressdeg1	⊢ ( 𝜑 → ( ( deg1 ‘ ℂfld ) ‘ ( 𝑀 ‘ 𝐴 ) ) = ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( 𝑀 ‘ 𝐴 ) ) )
36	1 21	eqtr3id	⊢ ( 𝜑 → ( deg1 ‘ ( ℂfld ↾s ℚ ) ) = 𝐷 )
37	4	eqcomd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = 𝐹 )
38	36 37	fveq12d	⊢ ( 𝜑 → ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝐷 ‘ 𝐹 ) )
39	25 35 38	3eqtrd	⊢ ( 𝜑 → ( ( ℂfld ↾s ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂfld ↾s ℚ ) ) = ( 𝐷 ‘ 𝐹 ) )
40	39	eqeq1d	⊢ ( 𝜑 → ( ( ( ℂfld ↾s ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂfld ↾s ℚ ) ) = ( 2 ↑ 𝑛 ) ↔ ( 𝐷 ‘ 𝐹 ) = ( 2 ↑ 𝑛 ) ) )
41	40	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( ( ℂfld ↾s ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂfld ↾s ℚ ) ) = ( 2 ↑ 𝑛 ) ↔ ( 𝐷 ‘ 𝐹 ) = ( 2 ↑ 𝑛 ) ) )
42	7 41	mtbird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ¬ ( ( ℂfld ↾s ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂfld ↾s ℚ ) ) = ( 2 ↑ 𝑛 ) )
43	42	nrexdv	⊢ ( 𝜑 → ¬ ∃ 𝑛 ∈ ℕ0 ( ( ℂfld ↾s ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂfld ↾s ℚ ) ) = ( 2 ↑ 𝑛 ) )
44		eqid	⊢ ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) ) = ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) )
45		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ Constr ) → 𝐴 ∈ Constr )
46	8 9 44 45	constrext2chn	⊢ ( ( 𝜑 ∧ 𝐴 ∈ Constr ) → ∃ 𝑛 ∈ ℕ0 ( ( ℂfld ↾s ( ℂfld fldGen ( ℚ ∪ { 𝐴 } ) ) ) [:] ( ℂfld ↾s ℚ ) ) = ( 2 ↑ 𝑛 ) )
47	43 46	mtand	⊢ ( 𝜑 → ¬ 𝐴 ∈ Constr )