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 
|- D = ( deg1 ` ( CCfld |`s QQ ) )
constrcon.m 
|- M = ( CCfld minPoly QQ )
constrcon.a 
|- ( ph -> A e. CC )
constrcon.f 
|- ( ph -> F = ( M ` A ) )
constrcon.1 
|- ( ph -> ( D ` F ) e. NN0 )
constrcon.2 
|- ( ( ph /\ n e. NN0 ) -> ( D ` F ) =/= ( 2 ^ n ) )
Assertion constrcon 
|- ( ph -> -. A e. Constr )

Proof

Step Hyp Ref Expression
1 constrcon.d 
 |-  D = ( deg1 ` ( CCfld |`s QQ ) )
2 constrcon.m 
 |-  M = ( CCfld minPoly QQ )
3 constrcon.a 
 |-  ( ph -> A e. CC )
4 constrcon.f 
 |-  ( ph -> F = ( M ` A ) )
5 constrcon.1 
 |-  ( ph -> ( D ` F ) e. NN0 )
6 constrcon.2 
 |-  ( ( ph /\ n e. NN0 ) -> ( D ` F ) =/= ( 2 ^ n ) )
7 6 neneqd 
 |-  ( ( ph /\ n e. NN0 ) -> -. ( D ` F ) = ( 2 ^ n ) )
8 eqid 
 |-  ( CCfld |`s QQ ) = ( CCfld |`s QQ )
9 eqid 
 |-  ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) = ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) )
10 eqid 
 |-  ( deg1 ` CCfld ) = ( deg1 ` CCfld )
11 cnfldfld 
 |-  CCfld e. Field
12 11 a1i 
 |-  ( ph -> CCfld e. Field )
13 cndrng 
 |-  CCfld e. DivRing
14 qsubdrg 
 |-  ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing )
15 14 simpli 
 |-  QQ e. ( SubRing ` CCfld )
16 8 qdrng 
 |-  ( CCfld |`s QQ ) e. DivRing
17 issdrg 
 |-  ( QQ e. ( SubDRing ` CCfld ) <-> ( CCfld e. DivRing /\ QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing ) )
18 13 15 16 17 mpbir3an 
 |-  QQ e. ( SubDRing ` CCfld )
19 18 a1i 
 |-  ( ph -> QQ e. ( SubDRing ` CCfld ) )
20 cnfldbas 
 |-  CC = ( Base ` CCfld )
21 eqidd 
 |-  ( ph -> D = D )
22 21 4 fveq12d 
 |-  ( ph -> ( D ` F ) = ( D ` ( M ` A ) ) )
23 22 5 eqeltrrd 
 |-  ( ph -> ( D ` ( M ` A ) ) e. NN0 )
24 20 2 1 12 19 3 23 minplyelirng 
 |-  ( ph -> A e. ( CCfld IntgRing QQ ) )
25 8 9 10 2 12 19 24 algextdeg 
 |-  ( ph -> ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) = ( ( deg1 ` CCfld ) ` ( M ` A ) ) )
26 eqid 
 |-  ( Poly1 ` ( CCfld |`s QQ ) ) = ( Poly1 ` ( CCfld |`s QQ ) )
27 eqid 
 |-  ( Base ` ( Poly1 ` ( CCfld |`s QQ ) ) ) = ( Base ` ( Poly1 ` ( CCfld |`s QQ ) ) )
28 eqid 
 |-  ( CCfld evalSub1 QQ ) = ( CCfld evalSub1 QQ )
29 eqid 
 |-  ( 0g ` CCfld ) = ( 0g ` CCfld )
30 eqid 
 |-  { q e. dom ( CCfld evalSub1 QQ ) | ( ( ( CCfld evalSub1 QQ ) ` q ) ` A ) = ( 0g ` CCfld ) } = { q e. dom ( CCfld evalSub1 QQ ) | ( ( ( CCfld evalSub1 QQ ) ` q ) ` A ) = ( 0g ` CCfld ) }
31 eqid 
 |-  ( RSpan ` ( Poly1 ` ( CCfld |`s QQ ) ) ) = ( RSpan ` ( Poly1 ` ( CCfld |`s QQ ) ) )
32 eqid 
 |-  ( idlGen1p ` ( CCfld |`s QQ ) ) = ( idlGen1p ` ( CCfld |`s QQ ) )
33 28 26 20 12 19 3 29 30 31 32 2 minplycl 
 |-  ( ph -> ( M ` A ) e. ( Base ` ( Poly1 ` ( CCfld |`s QQ ) ) ) )
34 15 a1i 
 |-  ( ph -> QQ e. ( SubRing ` CCfld ) )
35 8 10 26 27 33 34 ressdeg1 
 |-  ( ph -> ( ( deg1 ` CCfld ) ` ( M ` A ) ) = ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( M ` A ) ) )
36 1 21 eqtr3id 
 |-  ( ph -> ( deg1 ` ( CCfld |`s QQ ) ) = D )
37 4 eqcomd 
 |-  ( ph -> ( M ` A ) = F )
38 36 37 fveq12d 
 |-  ( ph -> ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( M ` A ) ) = ( D ` F ) )
39 25 35 38 3eqtrd 
 |-  ( ph -> ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) = ( D ` F ) )
40 39 eqeq1d 
 |-  ( ph -> ( ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ n ) <-> ( D ` F ) = ( 2 ^ n ) ) )
41 40 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ n ) <-> ( D ` F ) = ( 2 ^ n ) ) )
42 7 41 mtbird 
 |-  ( ( ph /\ n e. NN0 ) -> -. ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ n ) )
43 42 nrexdv 
 |-  ( ph -> -. E. n e. NN0 ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ n ) )
44 eqid 
 |-  ( CCfld fldGen ( QQ u. { A } ) ) = ( CCfld fldGen ( QQ u. { A } ) )
45 simpr 
 |-  ( ( ph /\ A e. Constr ) -> A e. Constr )
46 8 9 44 45 constrext2chn 
 |-  ( ( ph /\ A e. Constr ) -> E. n e. NN0 ( ( CCfld |`s ( CCfld fldGen ( QQ u. { A } ) ) ) [:] ( CCfld |`s QQ ) ) = ( 2 ^ n ) )
47 43 46 mtand 
 |-  ( ph -> -. A e. Constr )