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 = e i ⁢ 2 ⁢ π 3
Assertion cos9thpinconstrlem1 ⊢ O ∈ Constr

Proof

Step Hyp Ref Expression
1 cos9thpinconstr.1 ⊢ O = e i ⁢ 2 ⁢ π 3
2 0zd ⊢ ⊤ → 0 ∈ ℤ
3 2 zconstr ⊢ ⊤ → 0 ∈ Constr
4 1zzd ⊢ ⊤ → 1 ∈ ℤ
5 4 zconstr ⊢ ⊤ → 1 ∈ Constr
6 5 constrnegcl ⊢ ⊤ → − 1 ∈ Constr
7 ax-icn ⊢ i ∈ ℂ
8 7 a1i ⊢ ⊤ → i ∈ ℂ
9 2cnd ⊢ ⊤ → 2 ∈ ℂ
10 picn ⊢ π ∈ ℂ
11 10 a1i ⊢ ⊤ → π ∈ ℂ
12 9 11 mulcld ⊢ ⊤ → 2 ⁢ π ∈ ℂ
13 8 12 mulcld ⊢ ⊤ → i ⁢ 2 ⁢ π ∈ ℂ
14 3cn ⊢ 3 ∈ ℂ
15 14 a1i ⊢ ⊤ → 3 ∈ ℂ
16 3ne0 ⊢ 3 ≠ 0
17 16 a1i ⊢ ⊤ → 3 ≠ 0
18 13 15 17 divcld ⊢ ⊤ → i ⁢ 2 ⁢ π 3 ∈ ℂ
19 18 efcld ⊢ ⊤ → e i ⁢ 2 ⁢ π 3 ∈ ℂ
20 1 19 eqeltrid ⊢ ⊤ → O ∈ ℂ
21 0cnd ⊢ ⊤ → 0 ∈ ℂ
22 6 constrcn ⊢ ⊤ → − 1 ∈ ℂ
23 1cnd ⊢ ⊤ → 1 ∈ ℂ
24 21 23 subnegd ⊢ ⊤ → 0 − -1 = 0 + 1
25 23 addlidd ⊢ ⊤ → 0 + 1 = 1
26 24 25 eqtrd ⊢ ⊤ → 0 − -1 = 1
27 ax-1ne0 ⊢ 1 ≠ 0
28 27 a1i ⊢ ⊤ → 1 ≠ 0
29 26 28 eqnetrd ⊢ ⊤ → 0 − -1 ≠ 0
30 21 22 29 subne0ad ⊢ ⊤ → 0 ≠ − 1
31 8 12 15 17 divassd ⊢ ⊤ → i ⁢ 2 ⁢ π 3 = i ⁢ 2 ⁢ π 3
32 31 fveq2d ⊢ ⊤ → e i ⁢ 2 ⁢ π 3 = e i ⁢ 2 ⁢ π 3
33 32 fveq2d ⊢ ⊤ → e i ⁢ 2 ⁢ π 3 = e i ⁢ 2 ⁢ π 3
34 2re ⊢ 2 ∈ ℝ
35 34 a1i ⊢ ⊤ → 2 ∈ ℝ
36 pire ⊢ π ∈ ℝ
37 36 a1i ⊢ ⊤ → π ∈ ℝ
38 35 37 remulcld ⊢ ⊤ → 2 ⁢ π ∈ ℝ
39 3re ⊢ 3 ∈ ℝ
40 39 a1i ⊢ ⊤ → 3 ∈ ℝ
41 38 40 17 redivcld ⊢ ⊤ → 2 ⁢ π 3 ∈ ℝ
42 absefi ⊢ 2 ⁢ π 3 ∈ ℝ → e i ⁢ 2 ⁢ π 3 = 1
43 41 42 syl ⊢ ⊤ → e i ⁢ 2 ⁢ π 3 = 1
44 33 43 eqtrd ⊢ ⊤ → e i ⁢ 2 ⁢ π 3 = 1
45 1 a1i ⊢ ⊤ → O = e i ⁢ 2 ⁢ π 3
46 45 fveq2d ⊢ ⊤ → O = e i ⁢ 2 ⁢ π 3
47 1red ⊢ ⊤ → 1 ∈ ℝ
48 0le1 ⊢ 0 ≤ 1
49 48 a1i ⊢ ⊤ → 0 ≤ 1
50 47 49 absidd ⊢ ⊤ → 1 = 1
51 44 46 50 3eqtr4d ⊢ ⊤ → O = 1
52 20 subid1d ⊢ ⊤ → O − 0 = O
53 52 fveq2d ⊢ ⊤ → O − 0 = O
54 23 subid1d ⊢ ⊤ → 1 − 0 = 1
55 54 fveq2d ⊢ ⊤ → 1 − 0 = 1
56 51 53 55 3eqtr4d ⊢ ⊤ → O − 0 = 1 − 0
57 20 23 subnegd ⊢ ⊤ → O − -1 = O + 1
58 20 23 addcld ⊢ ⊤ → O + 1 ∈ ℂ
59 20 sqcld ⊢ ⊤ → O 2 ∈ ℂ
60 58 59 addcomd ⊢ ⊤ → O + 1 + O 2 = O 2 + O + 1
61 1 cos9thpiminplylem3 ⊢ O 2 + O + 1 = 0
62 61 a1i ⊢ ⊤ → O 2 + O + 1 = 0
63 60 62 eqtrd ⊢ ⊤ → O + 1 + O 2 = 0
64 addeq0 ⊢ O + 1 ∈ ℂ ∧ O 2 ∈ ℂ → O + 1 + O 2 = 0 ↔ O + 1 = − O 2
65 64 biimpa ⊢ O + 1 ∈ ℂ ∧ O 2 ∈ ℂ ∧ O + 1 + O 2 = 0 → O + 1 = − O 2
66 58 59 63 65 syl21anc ⊢ ⊤ → O + 1 = − O 2
67 57 66 eqtrd ⊢ ⊤ → O − -1 = − O 2
68 67 fveq2d ⊢ ⊤ → O − -1 = − O 2
69 59 absnegd ⊢ ⊤ → − O 2 = O 2
70 2nn0 ⊢ 2 ∈ ℕ 0
71 70 a1i ⊢ ⊤ → 2 ∈ ℕ 0
72 20 71 absexpd ⊢ ⊤ → O 2 = O 2
73 46 44 eqtrd ⊢ ⊤ → O = 1
74 73 oveq1d ⊢ ⊤ → O 2 = 1 2
75 sq1 ⊢ 1 2 = 1
76 55 50 eqtrd ⊢ ⊤ → 1 − 0 = 1
77 75 76 eqtr4id ⊢ ⊤ → 1 2 = 1 − 0
78 72 74 77 3eqtrd ⊢ ⊤ → O 2 = 1 − 0
79 68 69 78 3eqtrd ⊢ ⊤ → O − -1 = 1 − 0
80 3 5 3 6 5 3 20 30 56 79 constrcccl ⊢ ⊤ → O ∈ Constr
81 80 mptru ⊢ O ∈ Constr