Metamath Proof Explorer

Theorem cos9thpinconstrlem2

Description: The complex number A is not constructible. (Contributed by Thierry Arnoux, 15-Nov-2025)

Ref Expression
Hypotheses cos9thpinconstr.1 ⊢ 𝑂 = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) )
cos9thpiminply.2 ⊢ 𝑍 = ( 𝑂 ↑𝑐 ( 1 / 3 ) )
cos9thpiminply.3 ⊢ 𝐴 = ( 𝑍 + ( 1 / 𝑍 ) )
Assertion cos9thpinconstrlem2 ¬ 𝐴 ∈ Constr

Proof

Step Hyp Ref Expression
1 cos9thpinconstr.1 ⊢ 𝑂 = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) )
2 cos9thpiminply.2 ⊢ 𝑍 = ( 𝑂 ↑𝑐 ( 1 / 3 ) )
3 cos9thpiminply.3 ⊢ 𝐴 = ( 𝑍 + ( 1 / 𝑍 ) )
4 eqid ⊢ ( deg1 ‘ ( ℂfld ↾s ℚ ) ) = ( deg1 ‘ ( ℂfld ↾s ℚ ) )
5 eqid ⊢ ( ℂfld minPoly ℚ ) = ( ℂfld minPoly ℚ )
6 ax-icn ⊢ i ∈ ℂ
7 6 a1i ⊢ ( ⊤ → i ∈ ℂ )
8 2cnd ⊢ ( ⊤ → 2 ∈ ℂ )
9 picn ⊢ π ∈ ℂ
10 9 a1i ⊢ ( ⊤ → π ∈ ℂ )
11 8 10 mulcld ⊢ ( ⊤ → ( 2 · π ) ∈ ℂ )
12 7 11 mulcld ⊢ ( ⊤ → ( i · ( 2 · π ) ) ∈ ℂ )
13 3cn ⊢ 3 ∈ ℂ
14 13 a1i ⊢ ( ⊤ → 3 ∈ ℂ )
15 3ne0 ⊢ 3 ≠ 0
16 15 a1i ⊢ ( ⊤ → 3 ≠ 0 )
17 12 14 16 divcld ⊢ ( ⊤ → ( ( i · ( 2 · π ) ) / 3 ) ∈ ℂ )
18 17 efcld ⊢ ( ⊤ → ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ ℂ )
19 1 18 eqeltrid ⊢ ( ⊤ → 𝑂 ∈ ℂ )
20 13 15 reccli ⊢ ( 1 / 3 ) ∈ ℂ
21 20 a1i ⊢ ( ⊤ → ( 1 / 3 ) ∈ ℂ )
22 19 21 cxpcld ⊢ ( ⊤ → ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ∈ ℂ )
23 2 22 eqeltrid ⊢ ( ⊤ → 𝑍 ∈ ℂ )
24 2 a1i ⊢ ( ⊤ → 𝑍 = ( 𝑂 ↑𝑐 ( 1 / 3 ) ) )
25 1 a1i ⊢ ( ⊤ → 𝑂 = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) )
26 17 efne0d ⊢ ( ⊤ → ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ≠ 0 )
27 25 26 eqnetrd ⊢ ( ⊤ → 𝑂 ≠ 0 )
28 19 27 21 cxpne0d ⊢ ( ⊤ → ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ≠ 0 )
29 24 28 eqnetrd ⊢ ( ⊤ → 𝑍 ≠ 0 )
30 23 29 reccld ⊢ ( ⊤ → ( 1 / 𝑍 ) ∈ ℂ )
31 23 30 addcld ⊢ ( ⊤ → ( 𝑍 + ( 1 / 𝑍 ) ) ∈ ℂ )
32 3 31 eqeltrid ⊢ ( ⊤ → 𝐴 ∈ ℂ )
33 eqidd ⊢ ( ⊤ → ( ( ℂfld minPoly ℚ ) ‘ 𝐴 ) = ( ( ℂfld minPoly ℚ ) ‘ 𝐴 ) )
34 eqid ⊢ ( ℂfld ↾s ℚ ) = ( ℂfld ↾s ℚ )
35 eqid ⊢ ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) = ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) )
36 eqid ⊢ ( .r ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) = ( .r ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) )
37 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) )
38 eqid ⊢ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) = ( Poly1 ‘ ( ℂfld ↾s ℚ ) )
39 eqid ⊢ ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) = ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) )
40 eqid ⊢ ( var1 ‘ ( ℂfld ↾s ℚ ) ) = ( var1 ‘ ( ℂfld ↾s ℚ ) )
41 eqid ⊢ ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ - 3 ) ( .r ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 1 ) ) ) = ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ - 3 ) ( .r ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 1 ) ) )
42 1 2 3 34 35 36 37 38 39 40 4 41 5 cos9thpiminply ⊢ ( ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ - 3 ) ( .r ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 1 ) ) ) = ( ( ℂfld minPoly ℚ ) ‘ 𝐴 ) ∧ ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ - 3 ) ( .r ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 1 ) ) ) ) = 3 )
43 42 simpli ⊢ ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ - 3 ) ( .r ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 1 ) ) ) = ( ( ℂfld minPoly ℚ ) ‘ 𝐴 )
44 43 fveq2i ⊢ ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ - 3 ) ( .r ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 1 ) ) ) ) = ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ 𝐴 ) )
45 42 simpri ⊢ ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( 3 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ - 3 ) ( .r ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( var1 ‘ ( ℂfld ↾s ℚ ) ) ) ( +g ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℂfld ↾s ℚ ) ) ) ‘ 1 ) ) ) ) = 3
46 44 45 eqtr3i ⊢ ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ 𝐴 ) ) = 3
47 3nn0 ⊢ 3 ∈ ℕ0
48 46 47 eqeltri ⊢ ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ 𝐴 ) ) ∈ ℕ0
49 48 a1i ⊢ ( ⊤ → ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ 𝐴 ) ) ∈ ℕ0 )
50 46 a1i ⊢ ( 𝑛 ∈ ℕ0 → ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ 𝐴 ) ) = 3 )
51 3z ⊢ 3 ∈ ℤ
52 iddvds ⊢ ( 3 ∈ ℤ → 3 ∥ 3 )
53 51 52 ax-mp ⊢ 3 ∥ 3
54 simpr ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 = ( 2 ↑ 𝑛 ) ) → 3 = ( 2 ↑ 𝑛 ) )
55 53 54 breqtrid ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 = ( 2 ↑ 𝑛 ) ) → 3 ∥ ( 2 ↑ 𝑛 ) )
56 3prm ⊢ 3 ∈ ℙ
57 2prm ⊢ 2 ∈ ℙ
58 prmdvdsexpr ⊢ ( ( 3 ∈ ℙ ∧ 2 ∈ ℙ ∧ 𝑛 ∈ ℕ0 ) → ( 3 ∥ ( 2 ↑ 𝑛 ) → 3 = 2 ) )
59 56 57 58 mp3an12 ⊢ ( 𝑛 ∈ ℕ0 → ( 3 ∥ ( 2 ↑ 𝑛 ) → 3 = 2 ) )
60 59 imp ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 ∥ ( 2 ↑ 𝑛 ) ) → 3 = 2 )
61 55 60 syldan ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 = ( 2 ↑ 𝑛 ) ) → 3 = 2 )
62 2re ⊢ 2 ∈ ℝ
63 2lt3 ⊢ 2 < 3
64 62 63 gtneii ⊢ 3 ≠ 2
65 64 neii ⊢ ¬ 3 = 2
66 65 a1i ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 3 = ( 2 ↑ 𝑛 ) ) → ¬ 3 = 2 )
67 61 66 pm2.65da ⊢ ( 𝑛 ∈ ℕ0 → ¬ 3 = ( 2 ↑ 𝑛 ) )
68 67 neqned ⊢ ( 𝑛 ∈ ℕ0 → 3 ≠ ( 2 ↑ 𝑛 ) )
69 50 68 eqnetrd ⊢ ( 𝑛 ∈ ℕ0 → ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ 𝐴 ) ) ≠ ( 2 ↑ 𝑛 ) )
70 69 adantl ⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ0 ) → ( ( deg1 ‘ ( ℂfld ↾s ℚ ) ) ‘ ( ( ℂfld minPoly ℚ ) ‘ 𝐴 ) ) ≠ ( 2 ↑ 𝑛 ) )
71 4 5 32 33 49 70 constrcon ⊢ ( ⊤ → ¬ 𝐴 ∈ Constr )
72 71 mptru ⊢ ¬ 𝐴 ∈ Constr