Metamath Proof Explorer

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 ⊢ 𝐷 = ( 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 )