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 = e i ⁢ 2 ⁢ π 3
cos9thpiminply.2 ⊢ Z = O 1 3
Assertion cos9thpinconstr ⊢ O ∈ Constr ∧ Z ∉ Constr

Proof

Step Hyp Ref Expression
1 cos9thpinconstr.1 ⊢ O = e i ⁢ 2 ⁢ π 3
2 cos9thpiminply.2 ⊢ Z = O 1 3
3 1 cos9thpinconstrlem1 ⊢ O ∈ Constr
4 eqid ⊢ Z + 1 Z = Z + 1 Z
5 1 2 4 cos9thpinconstrlem2 ⊢ ¬ Z + 1 Z ∈ Constr
6 id ⊢ Z ∈ Constr → Z ∈ Constr
7 2 a1i ⊢ Z ∈ Constr → Z = O 1 3
8 ax-icn ⊢ i ∈ ℂ
9 8 a1i ⊢ Z ∈ Constr → i ∈ ℂ
10 2cnd ⊢ Z ∈ Constr → 2 ∈ ℂ
11 picn ⊢ π ∈ ℂ
12 11 a1i ⊢ Z ∈ Constr → π ∈ ℂ
13 10 12 mulcld ⊢ Z ∈ Constr → 2 ⁢ π ∈ ℂ
14 9 13 mulcld ⊢ Z ∈ Constr → i ⁢ 2 ⁢ π ∈ ℂ
15 3cn ⊢ 3 ∈ ℂ
16 15 a1i ⊢ Z ∈ Constr → 3 ∈ ℂ
17 3ne0 ⊢ 3 ≠ 0
18 17 a1i ⊢ Z ∈ Constr → 3 ≠ 0
19 14 16 18 divcld ⊢ Z ∈ Constr → i ⁢ 2 ⁢ π 3 ∈ ℂ
20 19 efcld ⊢ Z ∈ Constr → e i ⁢ 2 ⁢ π 3 ∈ ℂ
21 1 20 eqeltrid ⊢ Z ∈ Constr → O ∈ ℂ
22 1 a1i ⊢ Z ∈ Constr → O = e i ⁢ 2 ⁢ π 3
23 19 efne0d ⊢ Z ∈ Constr → e i ⁢ 2 ⁢ π 3 ≠ 0
24 22 23 eqnetrd ⊢ Z ∈ Constr → O ≠ 0
25 16 18 reccld ⊢ Z ∈ Constr → 1 3 ∈ ℂ
26 21 24 25 cxpne0d ⊢ Z ∈ Constr → O 1 3 ≠ 0
27 7 26 eqnetrd ⊢ Z ∈ Constr → Z ≠ 0
28 6 27 constrinvcl ⊢ Z ∈ Constr → 1 Z ∈ Constr
29 6 28 constraddcl ⊢ Z ∈ Constr → Z + 1 Z ∈ Constr
30 5 29 mto ⊢ ¬ Z ∈ Constr
31 30 nelir ⊢ Z ∉ Constr
32 3 31 pm3.2i ⊢ O ∈ Constr ∧ Z ∉ Constr