Theorem cos9thpiminplylem4

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

	Ref	Expression
Hypotheses	cos9thpiminplylem3.1	⊢ 𝑂 = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) )
	cos9thpiminplylem4.2	⊢ 𝑍 = ( 𝑂 ↑𝑐 ( 1 / 3 ) )
Assertion	cos9thpiminplylem4	⊢ ( ( 𝑍 ↑ 6 ) + ( 𝑍 ↑ 3 ) ) = - 1

Proof

Step	Hyp	Ref	Expression
1		cos9thpiminplylem3.1	⊢ 𝑂 = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) )
2		cos9thpiminplylem4.2	⊢ 𝑍 = ( 𝑂 ↑𝑐 ( 1 / 3 ) )
3		ax-icn	⊢ i ∈ ℂ
4		2cn	⊢ 2 ∈ ℂ
5		picn	⊢ π ∈ ℂ
6	4 5	mulcli	⊢ ( 2 · π ) ∈ ℂ
7	3 6	mulcli	⊢ ( i · ( 2 · π ) ) ∈ ℂ
8		3cn	⊢ 3 ∈ ℂ
9		3ne0	⊢ 3 ≠ 0
10	7 8 9	divcli	⊢ ( ( i · ( 2 · π ) ) / 3 ) ∈ ℂ
11		efcl	⊢ ( ( ( i · ( 2 · π ) ) / 3 ) ∈ ℂ → ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ ℂ )
12	10 11	ax-mp	⊢ ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ ℂ
13	1 12	eqeltri	⊢ 𝑂 ∈ ℂ
14	8 9	reccli	⊢ ( 1 / 3 ) ∈ ℂ
15		cxpcl	⊢ ( ( 𝑂 ∈ ℂ ∧ ( 1 / 3 ) ∈ ℂ ) → ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ∈ ℂ )
16	13 14 15	mp2an	⊢ ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ∈ ℂ
17	2 16	eqeltri	⊢ 𝑍 ∈ ℂ
18		3nn0	⊢ 3 ∈ ℕ0
19		2nn0	⊢ 2 ∈ ℕ0
20		expmul	⊢ ( ( 𝑍 ∈ ℂ ∧ 3 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 𝑍 ↑ ( 3 · 2 ) ) = ( ( 𝑍 ↑ 3 ) ↑ 2 ) )
21	17 18 19 20	mp3an	⊢ ( 𝑍 ↑ ( 3 · 2 ) ) = ( ( 𝑍 ↑ 3 ) ↑ 2 )
22		3t2e6	⊢ ( 3 · 2 ) = 6
23	22	oveq2i	⊢ ( 𝑍 ↑ ( 3 · 2 ) ) = ( 𝑍 ↑ 6 )
24	2	oveq1i	⊢ ( 𝑍 ↑ 3 ) = ( ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ↑ 3 )
25		cxpmul2	⊢ ( ( 𝑂 ∈ ℂ ∧ ( 1 / 3 ) ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑂 ↑𝑐 ( ( 1 / 3 ) · 3 ) ) = ( ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ↑ 3 ) )
26	13 14 18 25	mp3an	⊢ ( 𝑂 ↑𝑐 ( ( 1 / 3 ) · 3 ) ) = ( ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ↑ 3 )
27	24 26	eqtr4i	⊢ ( 𝑍 ↑ 3 ) = ( 𝑂 ↑𝑐 ( ( 1 / 3 ) · 3 ) )
28		ax-1cn	⊢ 1 ∈ ℂ
29	28 8 9	divcan1i	⊢ ( ( 1 / 3 ) · 3 ) = 1
30	29	oveq2i	⊢ ( 𝑂 ↑𝑐 ( ( 1 / 3 ) · 3 ) ) = ( 𝑂 ↑𝑐 1 )
31		cxp1	⊢ ( 𝑂 ∈ ℂ → ( 𝑂 ↑𝑐 1 ) = 𝑂 )
32	13 31	ax-mp	⊢ ( 𝑂 ↑𝑐 1 ) = 𝑂
33	27 30 32	3eqtri	⊢ ( 𝑍 ↑ 3 ) = 𝑂
34	33	oveq1i	⊢ ( ( 𝑍 ↑ 3 ) ↑ 2 ) = ( 𝑂 ↑ 2 )
35	21 23 34	3eqtr3i	⊢ ( 𝑍 ↑ 6 ) = ( 𝑂 ↑ 2 )
36	35 33	oveq12i	⊢ ( ( 𝑍 ↑ 6 ) + ( 𝑍 ↑ 3 ) ) = ( ( 𝑂 ↑ 2 ) + 𝑂 )
37	13	sqcli	⊢ ( 𝑂 ↑ 2 ) ∈ ℂ
38	37 13	addcli	⊢ ( ( 𝑂 ↑ 2 ) + 𝑂 ) ∈ ℂ
39	38 28	pm3.2i	⊢ ( ( ( 𝑂 ↑ 2 ) + 𝑂 ) ∈ ℂ ∧ 1 ∈ ℂ )
40	37 13 28	addassi	⊢ ( ( ( 𝑂 ↑ 2 ) + 𝑂 ) + 1 ) = ( ( 𝑂 ↑ 2 ) + ( 𝑂 + 1 ) )
41	1	cos9thpiminplylem3	⊢ ( ( 𝑂 ↑ 2 ) + ( 𝑂 + 1 ) ) = 0
42	40 41	eqtri	⊢ ( ( ( 𝑂 ↑ 2 ) + 𝑂 ) + 1 ) = 0
43		addeq0	⊢ ( ( ( ( 𝑂 ↑ 2 ) + 𝑂 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ( 𝑂 ↑ 2 ) + 𝑂 ) + 1 ) = 0 ↔ ( ( 𝑂 ↑ 2 ) + 𝑂 ) = - 1 ) )
44	43	biimpa	⊢ ( ( ( ( ( 𝑂 ↑ 2 ) + 𝑂 ) ∈ ℂ ∧ 1 ∈ ℂ ) ∧ ( ( ( 𝑂 ↑ 2 ) + 𝑂 ) + 1 ) = 0 ) → ( ( 𝑂 ↑ 2 ) + 𝑂 ) = - 1 )
45	39 42 44	mp2an	⊢ ( ( 𝑂 ↑ 2 ) + 𝑂 ) = - 1
46	36 45	eqtri	⊢ ( ( 𝑍 ↑ 6 ) + ( 𝑍 ↑ 3 ) ) = - 1