Metamath Proof Explorer

Theorem cos9thpinconstrlem1

Description: The complex number O , representing an angle of ( 2 x. _pi ) / 3 , is constructible. (Contributed by Thierry Arnoux, 14-Nov-2025)

Ref Expression
Hypothesis cos9thpinconstr.1 
|- O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) )
Assertion cos9thpinconstrlem1 
|- O e. Constr

Proof

Step Hyp Ref Expression
1 cos9thpinconstr.1 
 |-  O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) )
2 0zd 
 |-  ( T. -> 0 e. ZZ )
3 2 zconstr 
 |-  ( T. -> 0 e. Constr )
4 1zzd 
 |-  ( T. -> 1 e. ZZ )
5 4 zconstr 
 |-  ( T. -> 1 e. Constr )
6 5 constrnegcl 
 |-  ( T. -> -u 1 e. Constr )
7 ax-icn 
 |-  _i e. CC
8 7 a1i 
 |-  ( T. -> _i e. CC )
9 2cnd 
 |-  ( T. -> 2 e. CC )
10 picn 
 |-  _pi e. CC
11 10 a1i 
 |-  ( T. -> _pi e. CC )
12 9 11 mulcld 
 |-  ( T. -> ( 2 x. _pi ) e. CC )
13 8 12 mulcld 
 |-  ( T. -> ( _i x. ( 2 x. _pi ) ) e. CC )
14 3cn 
 |-  3 e. CC
15 14 a1i 
 |-  ( T. -> 3 e. CC )
16 3ne0 
 |-  3 =/= 0
17 16 a1i 
 |-  ( T. -> 3 =/= 0 )
18 13 15 17 divcld 
 |-  ( T. -> ( ( _i x. ( 2 x. _pi ) ) / 3 ) e. CC )
19 18 efcld 
 |-  ( T. -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) e. CC )
20 1 19 eqeltrid 
 |-  ( T. -> O e. CC )
21 0cnd 
 |-  ( T. -> 0 e. CC )
22 6 constrcn 
 |-  ( T. -> -u 1 e. CC )
23 1cnd 
 |-  ( T. -> 1 e. CC )
24 21 23 subnegd 
 |-  ( T. -> ( 0 - -u 1 ) = ( 0 + 1 ) )
25 23 addlidd 
 |-  ( T. -> ( 0 + 1 ) = 1 )
26 24 25 eqtrd 
 |-  ( T. -> ( 0 - -u 1 ) = 1 )
27 ax-1ne0 
 |-  1 =/= 0
28 27 a1i 
 |-  ( T. -> 1 =/= 0 )
29 26 28 eqnetrd 
 |-  ( T. -> ( 0 - -u 1 ) =/= 0 )
30 21 22 29 subne0ad 
 |-  ( T. -> 0 =/= -u 1 )
31 8 12 15 17 divassd 
 |-  ( T. -> ( ( _i x. ( 2 x. _pi ) ) / 3 ) = ( _i x. ( ( 2 x. _pi ) / 3 ) ) )
32 31 fveq2d 
 |-  ( T. -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) = ( exp ` ( _i x. ( ( 2 x. _pi ) / 3 ) ) ) )
33 32 fveq2d 
 |-  ( T. -> ( abs ` ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ) = ( abs ` ( exp ` ( _i x. ( ( 2 x. _pi ) / 3 ) ) ) ) )
34 2re 
 |-  2 e. RR
35 34 a1i 
 |-  ( T. -> 2 e. RR )
36 pire 
 |-  _pi e. RR
37 36 a1i 
 |-  ( T. -> _pi e. RR )
38 35 37 remulcld 
 |-  ( T. -> ( 2 x. _pi ) e. RR )
39 3re 
 |-  3 e. RR
40 39 a1i 
 |-  ( T. -> 3 e. RR )
41 38 40 17 redivcld 
 |-  ( T. -> ( ( 2 x. _pi ) / 3 ) e. RR )
42 absefi 
 |-  ( ( ( 2 x. _pi ) / 3 ) e. RR -> ( abs ` ( exp ` ( _i x. ( ( 2 x. _pi ) / 3 ) ) ) ) = 1 )
43 41 42 syl 
 |-  ( T. -> ( abs ` ( exp ` ( _i x. ( ( 2 x. _pi ) / 3 ) ) ) ) = 1 )
44 33 43 eqtrd 
 |-  ( T. -> ( abs ` ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ) = 1 )
45 1 a1i 
 |-  ( T. -> O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) )
46 45 fveq2d 
 |-  ( T. -> ( abs ` O ) = ( abs ` ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ) )
47 1red 
 |-  ( T. -> 1 e. RR )
48 0le1 
 |-  0 <_ 1
49 48 a1i 
 |-  ( T. -> 0 <_ 1 )
50 47 49 absidd 
 |-  ( T. -> ( abs ` 1 ) = 1 )
51 44 46 50 3eqtr4d 
 |-  ( T. -> ( abs ` O ) = ( abs ` 1 ) )
52 20 subid1d 
 |-  ( T. -> ( O - 0 ) = O )
53 52 fveq2d 
 |-  ( T. -> ( abs ` ( O - 0 ) ) = ( abs ` O ) )
54 23 subid1d 
 |-  ( T. -> ( 1 - 0 ) = 1 )
55 54 fveq2d 
 |-  ( T. -> ( abs ` ( 1 - 0 ) ) = ( abs ` 1 ) )
56 51 53 55 3eqtr4d 
 |-  ( T. -> ( abs ` ( O - 0 ) ) = ( abs ` ( 1 - 0 ) ) )
57 20 23 subnegd 
 |-  ( T. -> ( O - -u 1 ) = ( O + 1 ) )
58 20 23 addcld 
 |-  ( T. -> ( O + 1 ) e. CC )
59 20 sqcld 
 |-  ( T. -> ( O ^ 2 ) e. CC )
60 58 59 addcomd 
 |-  ( T. -> ( ( O + 1 ) + ( O ^ 2 ) ) = ( ( O ^ 2 ) + ( O + 1 ) ) )
61 1 cos9thpiminplylem3 
 |-  ( ( O ^ 2 ) + ( O + 1 ) ) = 0
62 61 a1i 
 |-  ( T. -> ( ( O ^ 2 ) + ( O + 1 ) ) = 0 )
63 60 62 eqtrd 
 |-  ( T. -> ( ( O + 1 ) + ( O ^ 2 ) ) = 0 )
64 addeq0 
 |-  ( ( ( O + 1 ) e. CC /\ ( O ^ 2 ) e. CC ) -> ( ( ( O + 1 ) + ( O ^ 2 ) ) = 0 <-> ( O + 1 ) = -u ( O ^ 2 ) ) )
65 64 biimpa 
 |-  ( ( ( ( O + 1 ) e. CC /\ ( O ^ 2 ) e. CC ) /\ ( ( O + 1 ) + ( O ^ 2 ) ) = 0 ) -> ( O + 1 ) = -u ( O ^ 2 ) )
66 58 59 63 65 syl21anc 
 |-  ( T. -> ( O + 1 ) = -u ( O ^ 2 ) )
67 57 66 eqtrd 
 |-  ( T. -> ( O - -u 1 ) = -u ( O ^ 2 ) )
68 67 fveq2d 
 |-  ( T. -> ( abs ` ( O - -u 1 ) ) = ( abs ` -u ( O ^ 2 ) ) )
69 59 absnegd 
 |-  ( T. -> ( abs ` -u ( O ^ 2 ) ) = ( abs ` ( O ^ 2 ) ) )
70 2nn0 
 |-  2 e. NN0
71 70 a1i 
 |-  ( T. -> 2 e. NN0 )
72 20 71 absexpd 
 |-  ( T. -> ( abs ` ( O ^ 2 ) ) = ( ( abs ` O ) ^ 2 ) )
73 46 44 eqtrd 
 |-  ( T. -> ( abs ` O ) = 1 )
74 73 oveq1d 
 |-  ( T. -> ( ( abs ` O ) ^ 2 ) = ( 1 ^ 2 ) )
75 sq1 
 |-  ( 1 ^ 2 ) = 1
76 55 50 eqtrd 
 |-  ( T. -> ( abs ` ( 1 - 0 ) ) = 1 )
77 75 76 eqtr4id 
 |-  ( T. -> ( 1 ^ 2 ) = ( abs ` ( 1 - 0 ) ) )
78 72 74 77 3eqtrd 
 |-  ( T. -> ( abs ` ( O ^ 2 ) ) = ( abs ` ( 1 - 0 ) ) )
79 68 69 78 3eqtrd 
 |-  ( T. -> ( abs ` ( O - -u 1 ) ) = ( abs ` ( 1 - 0 ) ) )
80 3 5 3 6 5 3 20 30 56 79 constrcccl 
 |-  ( T. -> O e. Constr )
81 80 mptru 
 |-  O e. Constr