Metamath Proof Explorer

Theorem cos9thpiminplylem4

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

Ref Expression
Hypotheses cos9thpiminplylem3.1 
|- O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) )
cos9thpiminplylem4.2 
|- Z = ( O ^c ( 1 / 3 ) )
Assertion cos9thpiminplylem4 
|- ( ( Z ^ 6 ) + ( Z ^ 3 ) ) = -u 1

Proof

Step Hyp Ref Expression
1 cos9thpiminplylem3.1 
 |-  O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) )
2 cos9thpiminplylem4.2 
 |-  Z = ( O ^c ( 1 / 3 ) )
3 ax-icn 
 |-  _i e. CC
4 2cn 
 |-  2 e. CC
5 picn 
 |-  _pi e. CC
6 4 5 mulcli 
 |-  ( 2 x. _pi ) e. CC
7 3 6 mulcli 
 |-  ( _i x. ( 2 x. _pi ) ) e. CC
8 3cn 
 |-  3 e. CC
9 3ne0 
 |-  3 =/= 0
10 7 8 9 divcli 
 |-  ( ( _i x. ( 2 x. _pi ) ) / 3 ) e. CC
11 efcl 
 |-  ( ( ( _i x. ( 2 x. _pi ) ) / 3 ) e. CC -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) e. CC )
12 10 11 ax-mp 
 |-  ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) e. CC
13 1 12 eqeltri 
 |-  O e. CC
14 8 9 reccli 
 |-  ( 1 / 3 ) e. CC
15 cxpcl 
 |-  ( ( O e. CC /\ ( 1 / 3 ) e. CC ) -> ( O ^c ( 1 / 3 ) ) e. CC )
16 13 14 15 mp2an 
 |-  ( O ^c ( 1 / 3 ) ) e. CC
17 2 16 eqeltri 
 |-  Z e. CC
18 3nn0 
 |-  3 e. NN0
19 2nn0 
 |-  2 e. NN0
20 expmul 
 |-  ( ( Z e. CC /\ 3 e. NN0 /\ 2 e. NN0 ) -> ( Z ^ ( 3 x. 2 ) ) = ( ( Z ^ 3 ) ^ 2 ) )
21 17 18 19 20 mp3an 
 |-  ( Z ^ ( 3 x. 2 ) ) = ( ( Z ^ 3 ) ^ 2 )
22 3t2e6 
 |-  ( 3 x. 2 ) = 6
23 22 oveq2i 
 |-  ( Z ^ ( 3 x. 2 ) ) = ( Z ^ 6 )
24 2 oveq1i 
 |-  ( Z ^ 3 ) = ( ( O ^c ( 1 / 3 ) ) ^ 3 )
25 cxpmul2 
 |-  ( ( O e. CC /\ ( 1 / 3 ) e. CC /\ 3 e. NN0 ) -> ( O ^c ( ( 1 / 3 ) x. 3 ) ) = ( ( O ^c ( 1 / 3 ) ) ^ 3 ) )
26 13 14 18 25 mp3an 
 |-  ( O ^c ( ( 1 / 3 ) x. 3 ) ) = ( ( O ^c ( 1 / 3 ) ) ^ 3 )
27 24 26 eqtr4i 
 |-  ( Z ^ 3 ) = ( O ^c ( ( 1 / 3 ) x. 3 ) )
28 ax-1cn 
 |-  1 e. CC
29 28 8 9 divcan1i 
 |-  ( ( 1 / 3 ) x. 3 ) = 1
30 29 oveq2i 
 |-  ( O ^c ( ( 1 / 3 ) x. 3 ) ) = ( O ^c 1 )
31 cxp1 
 |-  ( O e. CC -> ( O ^c 1 ) = O )
32 13 31 ax-mp 
 |-  ( O ^c 1 ) = O
33 27 30 32 3eqtri 
 |-  ( Z ^ 3 ) = O
34 33 oveq1i 
 |-  ( ( Z ^ 3 ) ^ 2 ) = ( O ^ 2 )
35 21 23 34 3eqtr3i 
 |-  ( Z ^ 6 ) = ( O ^ 2 )
36 35 33 oveq12i 
 |-  ( ( Z ^ 6 ) + ( Z ^ 3 ) ) = ( ( O ^ 2 ) + O )
37 13 sqcli 
 |-  ( O ^ 2 ) e. CC
38 37 13 addcli 
 |-  ( ( O ^ 2 ) + O ) e. CC
39 38 28 pm3.2i 
 |-  ( ( ( O ^ 2 ) + O ) e. CC /\ 1 e. CC )
40 37 13 28 addassi 
 |-  ( ( ( O ^ 2 ) + O ) + 1 ) = ( ( O ^ 2 ) + ( O + 1 ) )
41 1 cos9thpiminplylem3 
 |-  ( ( O ^ 2 ) + ( O + 1 ) ) = 0
42 40 41 eqtri 
 |-  ( ( ( O ^ 2 ) + O ) + 1 ) = 0
43 addeq0 
 |-  ( ( ( ( O ^ 2 ) + O ) e. CC /\ 1 e. CC ) -> ( ( ( ( O ^ 2 ) + O ) + 1 ) = 0 <-> ( ( O ^ 2 ) + O ) = -u 1 ) )
44 43 biimpa 
 |-  ( ( ( ( ( O ^ 2 ) + O ) e. CC /\ 1 e. CC ) /\ ( ( ( O ^ 2 ) + O ) + 1 ) = 0 ) -> ( ( O ^ 2 ) + O ) = -u 1 )
45 39 42 44 mp2an 
 |-  ( ( O ^ 2 ) + O ) = -u 1
46 36 45 eqtri 
 |-  ( ( Z ^ 6 ) + ( Z ^ 3 ) ) = -u 1