Metamath Proof Explorer

Theorem cos9thpiminplylem3

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

Ref Expression
Hypothesis cos9thpiminplylem3.1 ⊢ 𝑂 = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) )
Assertion cos9thpiminplylem3 ( ( 𝑂 ↑ 2 ) + ( 𝑂 + 1 ) ) = 0

Proof

Step Hyp Ref Expression
1 cos9thpiminplylem3.1 ⊢ 𝑂 = ( exp ‘ ( ( 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 ⊢ ( ⊤ → ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ ℂ )
15 1 14 eqeltrid ⊢ ( ⊤ → 𝑂 ∈ ℂ )
16 15 sqcld ⊢ ( ⊤ → ( 𝑂 ↑ 2 ) ∈ ℂ )
17 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
18 15 17 addcld ⊢ ( ⊤ → ( 𝑂 + 1 ) ∈ ℂ )
19 16 18 addcomd ⊢ ( ⊤ → ( ( 𝑂 ↑ 2 ) + ( 𝑂 + 1 ) ) = ( ( 𝑂 + 1 ) + ( 𝑂 ↑ 2 ) ) )
20 15 17 addcomd ⊢ ( ⊤ → ( 𝑂 + 1 ) = ( 1 + 𝑂 ) )
21 20 oveq1d ⊢ ( ⊤ → ( ( 𝑂 + 1 ) + ( 𝑂 ↑ 2 ) ) = ( ( 1 + 𝑂 ) + ( 𝑂 ↑ 2 ) ) )
22 oveq2 ⊢ ( 𝑛 = 0 → ( 𝑂 ↑ 𝑛 ) = ( 𝑂 ↑ 0 ) )
23 15 mptru ⊢ 𝑂 ∈ ℂ
24 23 a1i ⊢ ( 𝑛 = 0 → 𝑂 ∈ ℂ )
25 24 exp0d ⊢ ( 𝑛 = 0 → ( 𝑂 ↑ 0 ) = 1 )
26 22 25 eqtrd ⊢ ( 𝑛 = 0 → ( 𝑂 ↑ 𝑛 ) = 1 )
27 oveq2 ⊢ ( 𝑛 = 1 → ( 𝑂 ↑ 𝑛 ) = ( 𝑂 ↑ 1 ) )
28 23 a1i ⊢ ( 𝑛 = 1 → 𝑂 ∈ ℂ )
29 28 exp1d ⊢ ( 𝑛 = 1 → ( 𝑂 ↑ 1 ) = 𝑂 )
30 27 29 eqtrd ⊢ ( 𝑛 = 1 → ( 𝑂 ↑ 𝑛 ) = 𝑂 )
31 oveq2 ⊢ ( 𝑛 = 2 → ( 𝑂 ↑ 𝑛 ) = ( 𝑂 ↑ 2 ) )
32 17 15 16 3jca ⊢ ( ⊤ → ( 1 ∈ ℂ ∧ 𝑂 ∈ ℂ ∧ ( 𝑂 ↑ 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 ⊢ ( ⊤ → Σ 𝑛 ∈ { 0 , 1 , 2 } ( 𝑂 ↑ 𝑛 ) = ( ( 1 + 𝑂 ) + ( 𝑂 ↑ 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 ⊢ Σ 𝑛 ∈ ( 0 ... ( 3 − 1 ) ) ( 𝑂 ↑ 𝑛 ) = Σ 𝑛 ∈ { 0 , 1 , 2 } ( 𝑂 ↑ 𝑛 )
49 1 a1i ⊢ ( ⊤ → 𝑂 = ( exp ‘ ( ( 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 ) ∈ ℂ → ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) = 1 ↔ ( ( ( i · ( 2 · π ) ) / 3 ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
68 67 necon3abid ⊢ ( ( ( i · ( 2 · π ) ) / 3 ) ∈ ℂ → ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ≠ 1 ↔ ¬ ( ( ( i · ( 2 · π ) ) / 3 ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
69 68 biimpar ⊢ ( ( ( ( i · ( 2 · π ) ) / 3 ) ∈ ℂ ∧ ¬ ( ( ( i · ( 2 · π ) ) / 3 ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) → ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ≠ 1 )
70 13 66 69 syl2anc ⊢ ( ⊤ → ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ≠ 1 )
71 49 70 eqnetrd ⊢ ( ⊤ → 𝑂 ≠ 1 )
72 3nn0 ⊢ 3 ∈ ℕ0
73 72 a1i ⊢ ( ⊤ → 3 ∈ ℕ0 )
74 15 71 73 geoser ⊢ ( ⊤ → Σ 𝑛 ∈ ( 0 ... ( 3 − 1 ) ) ( 𝑂 ↑ 𝑛 ) = ( ( 1 − ( 𝑂 ↑ 3 ) ) / ( 1 − 𝑂 ) ) )
75 49 oveq1d ⊢ ( ⊤ → ( 𝑂 ↑ 3 ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 3 ) )
76 73 nn0zd ⊢ ( ⊤ → 3 ∈ ℤ )
77 efexp ⊢ ( ( ( ( i · ( 2 · π ) ) / 3 ) ∈ ℂ ∧ 3 ∈ ℤ ) → ( exp ‘ ( 3 · ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 3 ) )
78 13 76 77 syl2anc ⊢ ( ⊤ → ( exp ‘ ( 3 · ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 3 ) )
79 8 10 12 divcan2d ⊢ ( ⊤ → ( 3 · ( ( i · ( 2 · π ) ) / 3 ) ) = ( i · ( 2 · π ) ) )
80 79 fveq2d ⊢ ( ⊤ → ( exp ‘ ( 3 · ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( exp ‘ ( i · ( 2 · π ) ) ) )
81 ef2pi ⊢ ( exp ‘ ( i · ( 2 · π ) ) ) = 1
82 80 81 eqtrdi ⊢ ( ⊤ → ( exp ‘ ( 3 · ( ( i · ( 2 · π ) ) / 3 ) ) ) = 1 )
83 75 78 82 3eqtr2d ⊢ ( ⊤ → ( 𝑂 ↑ 3 ) = 1 )
84 83 oveq2d ⊢ ( ⊤ → ( 1 − ( 𝑂 ↑ 3 ) ) = ( 1 − 1 ) )
85 1m1e0 ⊢ ( 1 − 1 ) = 0
86 84 85 eqtrdi ⊢ ( ⊤ → ( 1 − ( 𝑂 ↑ 3 ) ) = 0 )
87 86 oveq1d ⊢ ( ⊤ → ( ( 1 − ( 𝑂 ↑ 3 ) ) / ( 1 − 𝑂 ) ) = ( 0 / ( 1 − 𝑂 ) ) )
88 17 15 subcld ⊢ ( ⊤ → ( 1 − 𝑂 ) ∈ ℂ )
89 71 necomd ⊢ ( ⊤ → 1 ≠ 𝑂 )
90 17 15 89 subne0d ⊢ ( ⊤ → ( 1 − 𝑂 ) ≠ 0 )
91 88 90 div0d ⊢ ( ⊤ → ( 0 / ( 1 − 𝑂 ) ) = 0 )
92 74 87 91 3eqtrd ⊢ ( ⊤ → Σ 𝑛 ∈ ( 0 ... ( 3 − 1 ) ) ( 𝑂 ↑ 𝑛 ) = 0 )
93 48 92 eqtr3id ⊢ ( ⊤ → Σ 𝑛 ∈ { 0 , 1 , 2 } ( 𝑂 ↑ 𝑛 ) = 0 )
94 21 43 93 3eqtr2d ⊢ ( ⊤ → ( ( 𝑂 + 1 ) + ( 𝑂 ↑ 2 ) ) = 0 )
95 19 94 eqtrd ⊢ ( ⊤ → ( ( 𝑂 ↑ 2 ) + ( 𝑂 + 1 ) ) = 0 )
96 95 mptru ⊢ ( ( 𝑂 ↑ 2 ) + ( 𝑂 + 1 ) ) = 0