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 ⊢ 𝑂 = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) )
cos9thpiminply.2 ⊢ 𝑍 = ( 𝑂 ↑𝑐 ( 1 / 3 ) )
Assertion cos9thpinconstr ( 𝑂 ∈ Constr ∧ 𝑍 ∉ Constr )

Proof

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