Metamath Proof Explorer

Theorem cos9thpiminplylem3

Description: Lemma for cos9thpiminply . (Contributed by Thierry Arnoux, 14-Nov-2025)

Ref Expression
Hypothesis cos9thpiminplylem3.1 ⊢ O = e i ⁢ 2 ⁢ π 3
Assertion cos9thpiminplylem3 ⊢ O 2 + O + 1 = 0

Proof

Step Hyp Ref Expression
1 cos9thpiminplylem3.1 ⊢ O = e i ⁢ 2 ⁢ π 3
2 ax-icn ⊢ i ∈ ℂ
3 2 a1i ⊢ ⊤ → i ∈ ℂ
4 2cnd ⊢ ⊤ → 2 ∈ ℂ
5 picn ⊢ π ∈ ℂ
6 5 a1i ⊢ ⊤ → π ∈ ℂ
7 4 6 mulcld ⊢ ⊤ → 2 ⁢ π ∈ ℂ
8 3 7 mulcld ⊢ ⊤ → i ⁢ 2 ⁢ π ∈ ℂ
9 3cn ⊢ 3 ∈ ℂ
10 9 a1i ⊢ ⊤ → 3 ∈ ℂ
11 3ne0 ⊢ 3 ≠ 0
12 11 a1i ⊢ ⊤ → 3 ≠ 0
13 8 10 12 divcld ⊢ ⊤ → i ⁢ 2 ⁢ π 3 ∈ ℂ
14 13 efcld ⊢ ⊤ → e i ⁢ 2 ⁢ π 3 ∈ ℂ
15 1 14 eqeltrid ⊢ ⊤ → O ∈ ℂ
16 15 sqcld ⊢ ⊤ → O 2 ∈ ℂ
17 1cnd ⊢ ⊤ → 1 ∈ ℂ
18 15 17 addcld ⊢ ⊤ → O + 1 ∈ ℂ
19 16 18 addcomd ⊢ ⊤ → O 2 + O + 1 = O + 1 + O 2
20 15 17 addcomd ⊢ ⊤ → O + 1 = 1 + O
21 20 oveq1d ⊢ ⊤ → O + 1 + O 2 = 1 + O + O 2
22 oveq2 ⊢ n = 0 → O n = O 0
23 15 mptru ⊢ O ∈ ℂ
24 23 a1i ⊢ n = 0 → O ∈ ℂ
25 24 exp0d ⊢ n = 0 → O 0 = 1
26 22 25 eqtrd ⊢ n = 0 → O n = 1
27 oveq2 ⊢ n = 1 → O n = O 1
28 23 a1i ⊢ n = 1 → O ∈ ℂ
29 28 exp1d ⊢ n = 1 → O 1 = O
30 27 29 eqtrd ⊢ n = 1 → O n = O
31 oveq2 ⊢ n = 2 → O n = O 2
32 17 15 16 3jca ⊢ ⊤ → 1 ∈ ℂ ∧ O ∈ ℂ ∧ O 2 ∈ ℂ
33 0cnd ⊢ ⊤ → 0 ∈ ℂ
34 33 17 4 3jca ⊢ ⊤ → 0 ∈ ℂ ∧ 1 ∈ ℂ ∧ 2 ∈ ℂ
35 ax-1ne0 ⊢ 1 ≠ 0
36 35 a1i ⊢ ⊤ → 1 ≠ 0
37 36 necomd ⊢ ⊤ → 0 ≠ 1
38 2ne0 ⊢ 2 ≠ 0
39 38 a1i ⊢ ⊤ → 2 ≠ 0
40 39 necomd ⊢ ⊤ → 0 ≠ 2
41 1ne2 ⊢ 1 ≠ 2
42 41 a1i ⊢ ⊤ → 1 ≠ 2
43 26 30 31 32 34 37 40 42 sumtp ⊢ ⊤ → ∑ n ∈ 0 1 2 O n = 1 + O + O 2
44 3m1e2 ⊢ 3 − 1 = 2
45 44 oveq2i ⊢ 0 … 3 − 1 = 0 … 2
46 fz0tp ⊢ 0 … 2 = 0 1 2
47 45 46 eqtri ⊢ 0 … 3 − 1 = 0 1 2
48 47 sumeq1i ⊢ ∑ n = 0 3 − 1 O n = ∑ n ∈ 0 1 2 O n
49 1 a1i ⊢ ⊤ → O = e i ⁢ 2 ⁢ π 3
50 ine0 ⊢ i ≠ 0
51 50 a1i ⊢ ⊤ → i ≠ 0
52 pine0 ⊢ π ≠ 0
53 52 a1i ⊢ ⊤ → π ≠ 0
54 4 6 39 53 mulne0d ⊢ ⊤ → 2 ⁢ π ≠ 0
55 3 7 51 54 mulne0d ⊢ ⊤ → i ⁢ 2 ⁢ π ≠ 0
56 8 10 8 12 55 divdiv32d ⊢ ⊤ → i ⁢ 2 ⁢ π 3 i ⁢ 2 ⁢ π = i ⁢ 2 ⁢ π i ⁢ 2 ⁢ π 3
57 8 55 dividd ⊢ ⊤ → i ⁢ 2 ⁢ π i ⁢ 2 ⁢ π = 1
58 57 oveq1d ⊢ ⊤ → i ⁢ 2 ⁢ π i ⁢ 2 ⁢ π 3 = 1 3
59 56 58 eqtrd ⊢ ⊤ → i ⁢ 2 ⁢ π 3 i ⁢ 2 ⁢ π = 1 3
60 3re ⊢ 3 ∈ ℝ
61 60 a1i ⊢ ⊤ → 3 ∈ ℝ
62 1lt3 ⊢ 1 < 3
63 62 a1i ⊢ ⊤ → 1 < 3
64 recnz ⊢ 3 ∈ ℝ ∧ 1 < 3 → ¬ 1 3 ∈ ℤ
65 61 63 64 syl2anc ⊢ ⊤ → ¬ 1 3 ∈ ℤ
66 59 65 eqneltrd ⊢ ⊤ → ¬ i ⁢ 2 ⁢ π 3 i ⁢ 2 ⁢ π ∈ ℤ
67 efeq1 ⊢ i ⁢ 2 ⁢ π 3 ∈ ℂ → e i ⁢ 2 ⁢ π 3 = 1 ↔ i ⁢ 2 ⁢ π 3 i ⁢ 2 ⁢ π ∈ ℤ
68 67 necon3abid ⊢ i ⁢ 2 ⁢ π 3 ∈ ℂ → e i ⁢ 2 ⁢ π 3 ≠ 1 ↔ ¬ i ⁢ 2 ⁢ π 3 i ⁢ 2 ⁢ π ∈ ℤ
69 68 biimpar ⊢ i ⁢ 2 ⁢ π 3 ∈ ℂ ∧ ¬ i ⁢ 2 ⁢ π 3 i ⁢ 2 ⁢ π ∈ ℤ → e i ⁢ 2 ⁢ π 3 ≠ 1
70 13 66 69 syl2anc ⊢ ⊤ → e i ⁢ 2 ⁢ π 3 ≠ 1
71 49 70 eqnetrd ⊢ ⊤ → O ≠ 1
72 3nn0 ⊢ 3 ∈ ℕ 0
73 72 a1i ⊢ ⊤ → 3 ∈ ℕ 0
74 15 71 73 geoser ⊢ ⊤ → ∑ n = 0 3 − 1 O n = 1 − O 3 1 − O
75 49 oveq1d ⊢ ⊤ → O 3 = e i ⁢ 2 ⁢ π 3 3
76 73 nn0zd ⊢ ⊤ → 3 ∈ ℤ
77 efexp ⊢ i ⁢ 2 ⁢ π 3 ∈ ℂ ∧ 3 ∈ ℤ → e 3 ⁢ i ⁢ 2 ⁢ π 3 = e i ⁢ 2 ⁢ π 3 3
78 13 76 77 syl2anc ⊢ ⊤ → e 3 ⁢ i ⁢ 2 ⁢ π 3 = e i ⁢ 2 ⁢ π 3 3
79 8 10 12 divcan2d ⊢ ⊤ → 3 ⁢ i ⁢ 2 ⁢ π 3 = i ⁢ 2 ⁢ π
80 79 fveq2d ⊢ ⊤ → e 3 ⁢ i ⁢ 2 ⁢ π 3 = e i ⁢ 2 ⁢ π
81 ef2pi ⊢ e i ⁢ 2 ⁢ π = 1
82 80 81 eqtrdi ⊢ ⊤ → e 3 ⁢ i ⁢ 2 ⁢ π 3 = 1
83 75 78 82 3eqtr2d ⊢ ⊤ → O 3 = 1
84 83 oveq2d ⊢ ⊤ → 1 − O 3 = 1 − 1
85 1m1e0 ⊢ 1 − 1 = 0
86 84 85 eqtrdi ⊢ ⊤ → 1 − O 3 = 0
87 86 oveq1d ⊢ ⊤ → 1 − O 3 1 − O = 0 1 − O
88 17 15 subcld ⊢ ⊤ → 1 − O ∈ ℂ
89 71 necomd ⊢ ⊤ → 1 ≠ O
90 17 15 89 subne0d ⊢ ⊤ → 1 − O ≠ 0
91 88 90 div0d ⊢ ⊤ → 0 1 − O = 0
92 74 87 91 3eqtrd ⊢ ⊤ → ∑ n = 0 3 − 1 O n = 0
93 48 92 eqtr3id ⊢ ⊤ → ∑ n ∈ 0 1 2 O n = 0
94 21 43 93 3eqtr2d ⊢ ⊤ → O + 1 + O 2 = 0
95 19 94 eqtrd ⊢ ⊤ → O 2 + O + 1 = 0
96 95 mptru ⊢ O 2 + O + 1 = 0