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 ⊢ 𝑂 = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) )
Assertion cos9thpinconstrlem1 𝑂 ∈ Constr

Proof

Step Hyp Ref Expression
1 cos9thpinconstr.1 ⊢ 𝑂 = ( exp ‘ ( ( 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 ⊢ ( ⊤ → ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ ℂ )
20 1 19 eqeltrid ⊢ ( ⊤ → 𝑂 ∈ ℂ )
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 ⊢ ( ⊤ → ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) = ( exp ‘ ( i · ( ( 2 · π ) / 3 ) ) ) )
33 32 fveq2d ⊢ ( ⊤ → ( abs ‘ ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( abs ‘ ( exp ‘ ( 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 ) ∈ ℝ → ( abs ‘ ( exp ‘ ( i · ( ( 2 · π ) / 3 ) ) ) ) = 1 )
43 41 42 syl ⊢ ( ⊤ → ( abs ‘ ( exp ‘ ( i · ( ( 2 · π ) / 3 ) ) ) ) = 1 )
44 33 43 eqtrd ⊢ ( ⊤ → ( abs ‘ ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ) = 1 )
45 1 a1i ⊢ ( ⊤ → 𝑂 = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) )
46 45 fveq2d ⊢ ( ⊤ → ( abs ‘ 𝑂 ) = ( abs ‘ ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ) )
47 1red ⊢ ( ⊤ → 1 ∈ ℝ )
48 0le1 ⊢ 0 ≤ 1
49 48 a1i ⊢ ( ⊤ → 0 ≤ 1 )
50 47 49 absidd ⊢ ( ⊤ → ( abs ‘ 1 ) = 1 )
51 44 46 50 3eqtr4d ⊢ ( ⊤ → ( abs ‘ 𝑂 ) = ( abs ‘ 1 ) )
52 20 subid1d ⊢ ( ⊤ → ( 𝑂 − 0 ) = 𝑂 )
53 52 fveq2d ⊢ ( ⊤ → ( abs ‘ ( 𝑂 − 0 ) ) = ( abs ‘ 𝑂 ) )
54 23 subid1d ⊢ ( ⊤ → ( 1 − 0 ) = 1 )
55 54 fveq2d ⊢ ( ⊤ → ( abs ‘ ( 1 − 0 ) ) = ( abs ‘ 1 ) )
56 51 53 55 3eqtr4d ⊢ ( ⊤ → ( abs ‘ ( 𝑂 − 0 ) ) = ( abs ‘ ( 1 − 0 ) ) )
57 20 23 subnegd ⊢ ( ⊤ → ( 𝑂 − - 1 ) = ( 𝑂 + 1 ) )
58 20 23 addcld ⊢ ( ⊤ → ( 𝑂 + 1 ) ∈ ℂ )
59 20 sqcld ⊢ ( ⊤ → ( 𝑂 ↑ 2 ) ∈ ℂ )
60 58 59 addcomd ⊢ ( ⊤ → ( ( 𝑂 + 1 ) + ( 𝑂 ↑ 2 ) ) = ( ( 𝑂 ↑ 2 ) + ( 𝑂 + 1 ) ) )
61 1 cos9thpiminplylem3 ⊢ ( ( 𝑂 ↑ 2 ) + ( 𝑂 + 1 ) ) = 0
62 61 a1i ⊢ ( ⊤ → ( ( 𝑂 ↑ 2 ) + ( 𝑂 + 1 ) ) = 0 )
63 60 62 eqtrd ⊢ ( ⊤ → ( ( 𝑂 + 1 ) + ( 𝑂 ↑ 2 ) ) = 0 )
64 addeq0 ⊢ ( ( ( 𝑂 + 1 ) ∈ ℂ ∧ ( 𝑂 ↑ 2 ) ∈ ℂ ) → ( ( ( 𝑂 + 1 ) + ( 𝑂 ↑ 2 ) ) = 0 ↔ ( 𝑂 + 1 ) = - ( 𝑂 ↑ 2 ) ) )
65 64 biimpa ⊢ ( ( ( ( 𝑂 + 1 ) ∈ ℂ ∧ ( 𝑂 ↑ 2 ) ∈ ℂ ) ∧ ( ( 𝑂 + 1 ) + ( 𝑂 ↑ 2 ) ) = 0 ) → ( 𝑂 + 1 ) = - ( 𝑂 ↑ 2 ) )
66 58 59 63 65 syl21anc ⊢ ( ⊤ → ( 𝑂 + 1 ) = - ( 𝑂 ↑ 2 ) )
67 57 66 eqtrd ⊢ ( ⊤ → ( 𝑂 − - 1 ) = - ( 𝑂 ↑ 2 ) )
68 67 fveq2d ⊢ ( ⊤ → ( abs ‘ ( 𝑂 − - 1 ) ) = ( abs ‘ - ( 𝑂 ↑ 2 ) ) )
69 59 absnegd ⊢ ( ⊤ → ( abs ‘ - ( 𝑂 ↑ 2 ) ) = ( abs ‘ ( 𝑂 ↑ 2 ) ) )
70 2nn0 ⊢ 2 ∈ ℕ0
71 70 a1i ⊢ ( ⊤ → 2 ∈ ℕ0 )
72 20 71 absexpd ⊢ ( ⊤ → ( abs ‘ ( 𝑂 ↑ 2 ) ) = ( ( abs ‘ 𝑂 ) ↑ 2 ) )
73 46 44 eqtrd ⊢ ( ⊤ → ( abs ‘ 𝑂 ) = 1 )
74 73 oveq1d ⊢ ( ⊤ → ( ( abs ‘ 𝑂 ) ↑ 2 ) = ( 1 ↑ 2 ) )
75 sq1 ⊢ ( 1 ↑ 2 ) = 1
76 55 50 eqtrd ⊢ ( ⊤ → ( abs ‘ ( 1 − 0 ) ) = 1 )
77 75 76 eqtr4id ⊢ ( ⊤ → ( 1 ↑ 2 ) = ( abs ‘ ( 1 − 0 ) ) )
78 72 74 77 3eqtrd ⊢ ( ⊤ → ( abs ‘ ( 𝑂 ↑ 2 ) ) = ( abs ‘ ( 1 − 0 ) ) )
79 68 69 78 3eqtrd ⊢ ( ⊤ → ( abs ‘ ( 𝑂 − - 1 ) ) = ( abs ‘ ( 1 − 0 ) ) )
80 3 5 3 6 5 3 20 30 56 79 constrcccl ⊢ ( ⊤ → 𝑂 ∈ Constr )
81 80 mptru ⊢ 𝑂 ∈ Constr