Metamath Proof Explorer

Theorem cos9thpinconstr

Description: Trisecting an angle is an impossible construction. Given for example O = ( exp( (i x. ( 2 x. pi ) ) / 3 ) ) , which represents an angle of ( ( 2 x. _pi ) / 3 ) , the cube root of O is not constructible with straightedge and compass, while O itself is constructible. This is the second part of Metamath 100 proof #8. Theorem 7.14 of Stewart p. 99. (Contributed by Thierry Arnoux and Saveliy Skresanov, 15-Nov-2025)

Ref Expression
Hypotheses cos9thpinconstr.1 
|- O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) )
cos9thpiminply.2 
|- Z = ( O ^c ( 1 / 3 ) )
Assertion cos9thpinconstr 
|- ( O e. Constr /\ Z 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 1 cos9thpinconstrlem1 
 |-  O e. Constr
4 eqid 
 |-  ( Z + ( 1 / Z ) ) = ( Z + ( 1 / Z ) )
5 1 2 4 cos9thpinconstrlem2 
 |-  -. ( Z + ( 1 / Z ) ) e. Constr
6 id 
 |-  ( Z e. Constr -> Z e. Constr )
7 2 a1i 
 |-  ( Z e. Constr -> Z = ( O ^c ( 1 / 3 ) ) )
8 ax-icn 
 |-  _i e. CC
9 8 a1i 
 |-  ( Z e. Constr -> _i e. CC )
10 2cnd 
 |-  ( Z e. Constr -> 2 e. CC )
11 picn 
 |-  _pi e. CC
12 11 a1i 
 |-  ( Z e. Constr -> _pi e. CC )
13 10 12 mulcld 
 |-  ( Z e. Constr -> ( 2 x. _pi ) e. CC )
14 9 13 mulcld 
 |-  ( Z e. Constr -> ( _i x. ( 2 x. _pi ) ) e. CC )
15 3cn 
 |-  3 e. CC
16 15 a1i 
 |-  ( Z e. Constr -> 3 e. CC )
17 3ne0 
 |-  3 =/= 0
18 17 a1i 
 |-  ( Z e. Constr -> 3 =/= 0 )
19 14 16 18 divcld 
 |-  ( Z e. Constr -> ( ( _i x. ( 2 x. _pi ) ) / 3 ) e. CC )
20 19 efcld 
 |-  ( Z e. Constr -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) e. CC )
21 1 20 eqeltrid 
 |-  ( Z e. Constr -> O e. CC )
22 1 a1i 
 |-  ( Z e. Constr -> O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) )
23 19 efne0d 
 |-  ( Z e. Constr -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) =/= 0 )
24 22 23 eqnetrd 
 |-  ( Z e. Constr -> O =/= 0 )
25 16 18 reccld 
 |-  ( Z e. Constr -> ( 1 / 3 ) e. CC )
26 21 24 25 cxpne0d 
 |-  ( Z e. Constr -> ( O ^c ( 1 / 3 ) ) =/= 0 )
27 7 26 eqnetrd 
 |-  ( Z e. Constr -> Z =/= 0 )
28 6 27 constrinvcl 
 |-  ( Z e. Constr -> ( 1 / Z ) e. Constr )
29 6 28 constraddcl 
 |-  ( Z e. Constr -> ( Z + ( 1 / Z ) ) e. Constr )
30 5 29 mto 
 |-  -. Z e. Constr
31 30 nelir 
 |-  Z e/ Constr
32 3 31 pm3.2i 
 |-  ( O e. Constr /\ Z e/ Constr )