Metamath Proof Explorer

Theorem cos9thpinconstrlem2

Description: The complex number A is not constructible. (Contributed by Thierry Arnoux, 15-Nov-2025)

Ref Expression
Hypotheses cos9thpinconstr.1 
|- O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) )
cos9thpiminply.2 
|- Z = ( O ^c ( 1 / 3 ) )
cos9thpiminply.3 
|- A = ( Z + ( 1 / Z ) )
Assertion cos9thpinconstrlem2 
|- -. A e. Constr

Proof

Step Hyp Ref Expression
1 cos9thpinconstr.1 
 |-  O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) )
2 cos9thpiminply.2 
 |-  Z = ( O ^c ( 1 / 3 ) )
3 cos9thpiminply.3 
 |-  A = ( Z + ( 1 / Z ) )
4 eqid 
 |-  ( deg1 ` ( CCfld |`s QQ ) ) = ( deg1 ` ( CCfld |`s QQ ) )
5 eqid 
 |-  ( CCfld minPoly QQ ) = ( CCfld minPoly QQ )
6 ax-icn 
 |-  _i e. CC
7 6 a1i 
 |-  ( T. -> _i e. CC )
8 2cnd 
 |-  ( T. -> 2 e. CC )
9 picn 
 |-  _pi e. CC
10 9 a1i 
 |-  ( T. -> _pi e. CC )
11 8 10 mulcld 
 |-  ( T. -> ( 2 x. _pi ) e. CC )
12 7 11 mulcld 
 |-  ( T. -> ( _i x. ( 2 x. _pi ) ) e. CC )
13 3cn 
 |-  3 e. CC
14 13 a1i 
 |-  ( T. -> 3 e. CC )
15 3ne0 
 |-  3 =/= 0
16 15 a1i 
 |-  ( T. -> 3 =/= 0 )
17 12 14 16 divcld 
 |-  ( T. -> ( ( _i x. ( 2 x. _pi ) ) / 3 ) e. CC )
18 17 efcld 
 |-  ( T. -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) e. CC )
19 1 18 eqeltrid 
 |-  ( T. -> O e. CC )
20 13 15 reccli 
 |-  ( 1 / 3 ) e. CC
21 20 a1i 
 |-  ( T. -> ( 1 / 3 ) e. CC )
22 19 21 cxpcld 
 |-  ( T. -> ( O ^c ( 1 / 3 ) ) e. CC )
23 2 22 eqeltrid 
 |-  ( T. -> Z e. CC )
24 2 a1i 
 |-  ( T. -> Z = ( O ^c ( 1 / 3 ) ) )
25 1 a1i 
 |-  ( T. -> O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) )
26 17 efne0d 
 |-  ( T. -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) =/= 0 )
27 25 26 eqnetrd 
 |-  ( T. -> O =/= 0 )
28 19 27 21 cxpne0d 
 |-  ( T. -> ( O ^c ( 1 / 3 ) ) =/= 0 )
29 24 28 eqnetrd 
 |-  ( T. -> Z =/= 0 )
30 23 29 reccld 
 |-  ( T. -> ( 1 / Z ) e. CC )
31 23 30 addcld 
 |-  ( T. -> ( Z + ( 1 / Z ) ) e. CC )
32 3 31 eqeltrid 
 |-  ( T. -> A e. CC )
33 eqidd 
 |-  ( T. -> ( ( CCfld minPoly QQ ) ` A ) = ( ( CCfld minPoly QQ ) ` A ) )
34 eqid 
 |-  ( CCfld |`s QQ ) = ( CCfld |`s QQ )
35 eqid 
 |-  ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) = ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) )
36 eqid 
 |-  ( .r ` ( Poly1 ` ( CCfld |`s QQ ) ) ) = ( .r ` ( Poly1 ` ( CCfld |`s QQ ) ) )
37 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) )
38 eqid 
 |-  ( Poly1 ` ( CCfld |`s QQ ) ) = ( Poly1 ` ( CCfld |`s QQ ) )
39 eqid 
 |-  ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) = ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) )
40 eqid 
 |-  ( var1 ` ( CCfld |`s QQ ) ) = ( var1 ` ( CCfld |`s QQ ) )
41 eqid 
 |-  ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` -u 3 ) ( .r ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 1 ) ) ) = ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` -u 3 ) ( .r ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 1 ) ) )
42 1 2 3 34 35 36 37 38 39 40 4 41 5 cos9thpiminply 
 |-  ( ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` -u 3 ) ( .r ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 1 ) ) ) = ( ( CCfld minPoly QQ ) ` A ) /\ ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` -u 3 ) ( .r ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 1 ) ) ) ) = 3 )
43 42 simpli 
 |-  ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` -u 3 ) ( .r ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 1 ) ) ) = ( ( CCfld minPoly QQ ) ` A )
44 43 fveq2i 
 |-  ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` -u 3 ) ( .r ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 1 ) ) ) ) = ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` A ) )
45 42 simpri 
 |-  ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( 3 ( .g ` ( mulGrp ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` -u 3 ) ( .r ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( var1 ` ( CCfld |`s QQ ) ) ) ( +g ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ( ( algSc ` ( Poly1 ` ( CCfld |`s QQ ) ) ) ` 1 ) ) ) ) = 3
46 44 45 eqtr3i 
 |-  ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` A ) ) = 3
47 3nn0 
 |-  3 e. NN0
48 46 47 eqeltri 
 |-  ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` A ) ) e. NN0
49 48 a1i 
 |-  ( T. -> ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` A ) ) e. NN0 )
50 46 a1i 
 |-  ( n e. NN0 -> ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` A ) ) = 3 )
51 3z 
 |-  3 e. ZZ
52 iddvds 
 |-  ( 3 e. ZZ -> 3 || 3 )
53 51 52 ax-mp 
 |-  3 || 3
54 simpr 
 |-  ( ( n e. NN0 /\ 3 = ( 2 ^ n ) ) -> 3 = ( 2 ^ n ) )
55 53 54 breqtrid 
 |-  ( ( n e. NN0 /\ 3 = ( 2 ^ n ) ) -> 3 || ( 2 ^ n ) )
56 3prm 
 |-  3 e. Prime
57 2prm 
 |-  2 e. Prime
58 prmdvdsexpr 
 |-  ( ( 3 e. Prime /\ 2 e. Prime /\ n e. NN0 ) -> ( 3 || ( 2 ^ n ) -> 3 = 2 ) )
59 56 57 58 mp3an12 
 |-  ( n e. NN0 -> ( 3 || ( 2 ^ n ) -> 3 = 2 ) )
60 59 imp 
 |-  ( ( n e. NN0 /\ 3 || ( 2 ^ n ) ) -> 3 = 2 )
61 55 60 syldan 
 |-  ( ( n e. NN0 /\ 3 = ( 2 ^ n ) ) -> 3 = 2 )
62 2re 
 |-  2 e. RR
63 2lt3 
 |-  2 < 3
64 62 63 gtneii 
 |-  3 =/= 2
65 64 neii 
 |-  -. 3 = 2
66 65 a1i 
 |-  ( ( n e. NN0 /\ 3 = ( 2 ^ n ) ) -> -. 3 = 2 )
67 61 66 pm2.65da 
 |-  ( n e. NN0 -> -. 3 = ( 2 ^ n ) )
68 67 neqned 
 |-  ( n e. NN0 -> 3 =/= ( 2 ^ n ) )
69 50 68 eqnetrd 
 |-  ( n e. NN0 -> ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` A ) ) =/= ( 2 ^ n ) )
70 69 adantl 
 |-  ( ( T. /\ n e. NN0 ) -> ( ( deg1 ` ( CCfld |`s QQ ) ) ` ( ( CCfld minPoly QQ ) ` A ) ) =/= ( 2 ^ n ) )
71 4 5 32 33 49 70 constrcon 
 |-  ( T. -> -. A e. Constr )
72 71 mptru 
 |-  -. A e. Constr