Metamath Proof Explorer

Theorem cos9thpiminplylem3

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

Ref Expression
Hypothesis cos9thpiminplylem3.1 
|- O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) )
Assertion cos9thpiminplylem3 
|- ( ( O ^ 2 ) + ( O + 1 ) ) = 0

Proof

Step Hyp Ref Expression
1 cos9thpiminplylem3.1 
 |-  O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) )
2 ax-icn 
 |-  _i e. CC
3 2 a1i 
 |-  ( T. -> _i e. CC )
4 2cnd 
 |-  ( T. -> 2 e. CC )
5 picn 
 |-  _pi e. CC
6 5 a1i 
 |-  ( T. -> _pi e. CC )
7 4 6 mulcld 
 |-  ( T. -> ( 2 x. _pi ) e. CC )
8 3 7 mulcld 
 |-  ( T. -> ( _i x. ( 2 x. _pi ) ) e. CC )
9 3cn 
 |-  3 e. CC
10 9 a1i 
 |-  ( T. -> 3 e. CC )
11 3ne0 
 |-  3 =/= 0
12 11 a1i 
 |-  ( T. -> 3 =/= 0 )
13 8 10 12 divcld 
 |-  ( T. -> ( ( _i x. ( 2 x. _pi ) ) / 3 ) e. CC )
14 13 efcld 
 |-  ( T. -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) e. CC )
15 1 14 eqeltrid 
 |-  ( T. -> O e. CC )
16 15 sqcld 
 |-  ( T. -> ( O ^ 2 ) e. CC )
17 1cnd 
 |-  ( T. -> 1 e. CC )
18 15 17 addcld 
 |-  ( T. -> ( O + 1 ) e. CC )
19 16 18 addcomd 
 |-  ( T. -> ( ( O ^ 2 ) + ( O + 1 ) ) = ( ( O + 1 ) + ( O ^ 2 ) ) )
20 15 17 addcomd 
 |-  ( T. -> ( O + 1 ) = ( 1 + O ) )
21 20 oveq1d 
 |-  ( T. -> ( ( O + 1 ) + ( O ^ 2 ) ) = ( ( 1 + O ) + ( O ^ 2 ) ) )
22 oveq2 
 |-  ( n = 0 -> ( O ^ n ) = ( O ^ 0 ) )
23 15 mptru 
 |-  O e. CC
24 23 a1i 
 |-  ( n = 0 -> O e. CC )
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 e. CC )
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 
 |-  ( T. -> ( 1 e. CC /\ O e. CC /\ ( O ^ 2 ) e. CC ) )
33 0cnd 
 |-  ( T. -> 0 e. CC )
34 33 17 4 3jca 
 |-  ( T. -> ( 0 e. CC /\ 1 e. CC /\ 2 e. CC ) )
35 ax-1ne0 
 |-  1 =/= 0
36 35 a1i 
 |-  ( T. -> 1 =/= 0 )
37 36 necomd 
 |-  ( T. -> 0 =/= 1 )
38 2ne0 
 |-  2 =/= 0
39 38 a1i 
 |-  ( T. -> 2 =/= 0 )
40 39 necomd 
 |-  ( T. -> 0 =/= 2 )
41 1ne2 
 |-  1 =/= 2
42 41 a1i 
 |-  ( T. -> 1 =/= 2 )
43 26 30 31 32 34 37 40 42 sumtp 
 |-  ( T. -> sum_ n e. { 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 
 |-  sum_ n e. ( 0 ... ( 3 - 1 ) ) ( O ^ n ) = sum_ n e. { 0 , 1 , 2 } ( O ^ n )
49 1 a1i 
 |-  ( T. -> O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) )
50 ine0 
 |-  _i =/= 0
51 50 a1i 
 |-  ( T. -> _i =/= 0 )
52 pine0 
 |-  _pi =/= 0
53 52 a1i 
 |-  ( T. -> _pi =/= 0 )
54 4 6 39 53 mulne0d 
 |-  ( T. -> ( 2 x. _pi ) =/= 0 )
55 3 7 51 54 mulne0d 
 |-  ( T. -> ( _i x. ( 2 x. _pi ) ) =/= 0 )
56 8 10 8 12 55 divdiv32d 
 |-  ( T. -> ( ( ( _i x. ( 2 x. _pi ) ) / 3 ) / ( _i x. ( 2 x. _pi ) ) ) = ( ( ( _i x. ( 2 x. _pi ) ) / ( _i x. ( 2 x. _pi ) ) ) / 3 ) )
57 8 55 dividd 
 |-  ( T. -> ( ( _i x. ( 2 x. _pi ) ) / ( _i x. ( 2 x. _pi ) ) ) = 1 )
58 57 oveq1d 
 |-  ( T. -> ( ( ( _i x. ( 2 x. _pi ) ) / ( _i x. ( 2 x. _pi ) ) ) / 3 ) = ( 1 / 3 ) )
59 56 58 eqtrd 
 |-  ( T. -> ( ( ( _i x. ( 2 x. _pi ) ) / 3 ) / ( _i x. ( 2 x. _pi ) ) ) = ( 1 / 3 ) )
60 3re 
 |-  3 e. RR
61 60 a1i 
 |-  ( T. -> 3 e. RR )
62 1lt3 
 |-  1 < 3
63 62 a1i 
 |-  ( T. -> 1 < 3 )
64 recnz 
 |-  ( ( 3 e. RR /\ 1 < 3 ) -> -. ( 1 / 3 ) e. ZZ )
65 61 63 64 syl2anc 
 |-  ( T. -> -. ( 1 / 3 ) e. ZZ )
66 59 65 eqneltrd 
 |-  ( T. -> -. ( ( ( _i x. ( 2 x. _pi ) ) / 3 ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ )
67 efeq1 
 |-  ( ( ( _i x. ( 2 x. _pi ) ) / 3 ) e. CC -> ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) = 1 <-> ( ( ( _i x. ( 2 x. _pi ) ) / 3 ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
68 67 necon3abid 
 |-  ( ( ( _i x. ( 2 x. _pi ) ) / 3 ) e. CC -> ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) =/= 1 <-> -. ( ( ( _i x. ( 2 x. _pi ) ) / 3 ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
69 68 biimpar 
 |-  ( ( ( ( _i x. ( 2 x. _pi ) ) / 3 ) e. CC /\ -. ( ( ( _i x. ( 2 x. _pi ) ) / 3 ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) =/= 1 )
70 13 66 69 syl2anc 
 |-  ( T. -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) =/= 1 )
71 49 70 eqnetrd 
 |-  ( T. -> O =/= 1 )
72 3nn0 
 |-  3 e. NN0
73 72 a1i 
 |-  ( T. -> 3 e. NN0 )
74 15 71 73 geoser 
 |-  ( T. -> sum_ n e. ( 0 ... ( 3 - 1 ) ) ( O ^ n ) = ( ( 1 - ( O ^ 3 ) ) / ( 1 - O ) ) )
75 49 oveq1d 
 |-  ( T. -> ( O ^ 3 ) = ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ^ 3 ) )
76 73 nn0zd 
 |-  ( T. -> 3 e. ZZ )
77 efexp 
 |-  ( ( ( ( _i x. ( 2 x. _pi ) ) / 3 ) e. CC /\ 3 e. ZZ ) -> ( exp ` ( 3 x. ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ) = ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ^ 3 ) )
78 13 76 77 syl2anc 
 |-  ( T. -> ( exp ` ( 3 x. ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ) = ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ^ 3 ) )
79 8 10 12 divcan2d 
 |-  ( T. -> ( 3 x. ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) = ( _i x. ( 2 x. _pi ) ) )
80 79 fveq2d 
 |-  ( T. -> ( exp ` ( 3 x. ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ) = ( exp ` ( _i x. ( 2 x. _pi ) ) ) )
81 ef2pi 
 |-  ( exp ` ( _i x. ( 2 x. _pi ) ) ) = 1
82 80 81 eqtrdi 
 |-  ( T. -> ( exp ` ( 3 x. ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) ) = 1 )
83 75 78 82 3eqtr2d 
 |-  ( T. -> ( O ^ 3 ) = 1 )
84 83 oveq2d 
 |-  ( T. -> ( 1 - ( O ^ 3 ) ) = ( 1 - 1 ) )
85 1m1e0 
 |-  ( 1 - 1 ) = 0
86 84 85 eqtrdi 
 |-  ( T. -> ( 1 - ( O ^ 3 ) ) = 0 )
87 86 oveq1d 
 |-  ( T. -> ( ( 1 - ( O ^ 3 ) ) / ( 1 - O ) ) = ( 0 / ( 1 - O ) ) )
88 17 15 subcld 
 |-  ( T. -> ( 1 - O ) e. CC )
89 71 necomd 
 |-  ( T. -> 1 =/= O )
90 17 15 89 subne0d 
 |-  ( T. -> ( 1 - O ) =/= 0 )
91 88 90 div0d 
 |-  ( T. -> ( 0 / ( 1 - O ) ) = 0 )
92 74 87 91 3eqtrd 
 |-  ( T. -> sum_ n e. ( 0 ... ( 3 - 1 ) ) ( O ^ n ) = 0 )
93 48 92 eqtr3id 
 |-  ( T. -> sum_ n e. { 0 , 1 , 2 } ( O ^ n ) = 0 )
94 21 43 93 3eqtr2d 
 |-  ( T. -> ( ( O + 1 ) + ( O ^ 2 ) ) = 0 )
95 19 94 eqtrd 
 |-  ( T. -> ( ( O ^ 2 ) + ( O + 1 ) ) = 0 )
96 95 mptru 
 |-  ( ( O ^ 2 ) + ( O + 1 ) ) = 0