Metamath Proof Explorer

Theorem cos9thpiminplylem5

Description: The constructed complex number A is a root of the polynomial ( ( X ^ 3 ) + ( ( -u 3 x. X ) + 1 ) ) . (Contributed by Thierry Arnoux, 14-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 cos9thpiminplylem3.1 ⊢ 𝑂 = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) )
2 cos9thpiminplylem4.2 ⊢ 𝑍 = ( 𝑂 ↑𝑐 ( 1 / 3 ) )
3 cos9thpiminplylem5.3 ⊢ 𝐴 = ( 𝑍 + ( 1 / 𝑍 ) )
4 ax-icn ⊢ i ∈ ℂ
5 2cn ⊢ 2 ∈ ℂ
6 picn ⊢ π ∈ ℂ
7 5 6 mulcli ⊢ ( 2 · π ) ∈ ℂ
8 4 7 mulcli ⊢ ( i · ( 2 · π ) ) ∈ ℂ
9 3cn ⊢ 3 ∈ ℂ
10 3ne0 ⊢ 3 ≠ 0
11 8 9 10 divcli ⊢ ( ( i · ( 2 · π ) ) / 3 ) ∈ ℂ
12 efcl ⊢ ( ( ( i · ( 2 · π ) ) / 3 ) ∈ ℂ → ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ ℂ )
13 11 12 ax-mp ⊢ ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ ℂ
14 1 13 eqeltri ⊢ 𝑂 ∈ ℂ
15 ax-1cn ⊢ 1 ∈ ℂ
16 15 9 10 divcli ⊢ ( 1 / 3 ) ∈ ℂ
17 cxpcl ⊢ ( ( 𝑂 ∈ ℂ ∧ ( 1 / 3 ) ∈ ℂ ) → ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ∈ ℂ )
18 14 16 17 mp2an ⊢ ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ∈ ℂ
19 2 18 eqeltri ⊢ 𝑍 ∈ ℂ
20 efne0 ⊢ ( ( ( i · ( 2 · π ) ) / 3 ) ∈ ℂ → ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ≠ 0 )
21 11 20 ax-mp ⊢ ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ≠ 0
22 1 21 eqnetri ⊢ 𝑂 ≠ 0
23 cxpne0 ⊢ ( ( 𝑂 ∈ ℂ ∧ 𝑂 ≠ 0 ∧ ( 1 / 3 ) ∈ ℂ ) → ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ≠ 0 )
24 14 22 16 23 mp3an ⊢ ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ≠ 0
25 2 24 eqnetri ⊢ 𝑍 ≠ 0
26 15 19 25 divcli ⊢ ( 1 / 𝑍 ) ∈ ℂ
27 19 26 addcli ⊢ ( 𝑍 + ( 1 / 𝑍 ) ) ∈ ℂ
28 3 27 eqeltri ⊢ 𝐴 ∈ ℂ
29 3nn0 ⊢ 3 ∈ ℕ0
30 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐴 ↑ 3 ) ∈ ℂ )
31 28 29 30 mp2an ⊢ ( 𝐴 ↑ 3 ) ∈ ℂ
32 9 negcli ⊢ - 3 ∈ ℂ
33 32 28 mulcli ⊢ ( - 3 · 𝐴 ) ∈ ℂ
34 33 15 addcli ⊢ ( ( - 3 · 𝐴 ) + 1 ) ∈ ℂ
35 31 34 pm3.2i ⊢ ( ( 𝐴 ↑ 3 ) ∈ ℂ ∧ ( ( - 3 · 𝐴 ) + 1 ) ∈ ℂ )
36 binom3 ⊢ ( ( 𝑍 ∈ ℂ ∧ ( 1 / 𝑍 ) ∈ ℂ ) → ( ( 𝑍 + ( 1 / 𝑍 ) ) ↑ 3 ) = ( ( ( 𝑍 ↑ 3 ) + ( 3 · ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) ) ) + ( ( 3 · ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) ) + ( ( 1 / 𝑍 ) ↑ 3 ) ) ) )
37 19 26 36 mp2an ⊢ ( ( 𝑍 + ( 1 / 𝑍 ) ) ↑ 3 ) = ( ( ( 𝑍 ↑ 3 ) + ( 3 · ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) ) ) + ( ( 3 · ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) ) + ( ( 1 / 𝑍 ) ↑ 3 ) ) )
38 3 oveq1i ⊢ ( 𝐴 ↑ 3 ) = ( ( 𝑍 + ( 1 / 𝑍 ) ) ↑ 3 )
39 33 15 negdii ⊢ - ( ( - 3 · 𝐴 ) + 1 ) = ( - ( - 3 · 𝐴 ) + - 1 )
40 32 28 mulneg1i ⊢ ( - - 3 · 𝐴 ) = - ( - 3 · 𝐴 )
41 40 oveq1i ⊢ ( ( - - 3 · 𝐴 ) + - 1 ) = ( - ( - 3 · 𝐴 ) + - 1 )
42 9 negnegi ⊢ - - 3 = 3
43 42 oveq1i ⊢ ( - - 3 · 𝐴 ) = ( 3 · 𝐴 )
44 43 oveq1i ⊢ ( ( - - 3 · 𝐴 ) + - 1 ) = ( ( 3 · 𝐴 ) + - 1 )
45 41 44 eqtr3i ⊢ ( - ( - 3 · 𝐴 ) + - 1 ) = ( ( 3 · 𝐴 ) + - 1 )
46 6nn0 ⊢ 6 ∈ ℕ0
47 expcl ⊢ ( ( 𝑍 ∈ ℂ ∧ 6 ∈ ℕ0 ) → ( 𝑍 ↑ 6 ) ∈ ℂ )
48 19 46 47 mp2an ⊢ ( 𝑍 ↑ 6 ) ∈ ℂ
49 expcl ⊢ ( ( 𝑍 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑍 ↑ 3 ) ∈ ℂ )
50 19 29 49 mp2an ⊢ ( 𝑍 ↑ 3 ) ∈ ℂ
51 48 50 addcomi ⊢ ( ( 𝑍 ↑ 6 ) + ( 𝑍 ↑ 3 ) ) = ( ( 𝑍 ↑ 3 ) + ( 𝑍 ↑ 6 ) )
52 1 2 cos9thpiminplylem4 ⊢ ( ( 𝑍 ↑ 6 ) + ( 𝑍 ↑ 3 ) ) = - 1
53 13 sqcli ⊢ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 ) ∈ ℂ
54 13 21 pm3.2i ⊢ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ ℂ ∧ ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ≠ 0 )
55 15 53 54 3pm3.2i ⊢ ( 1 ∈ ℂ ∧ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 ) ∈ ℂ ∧ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ ℂ ∧ ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ≠ 0 ) )
56 5 15 11 adddiri ⊢ ( ( 2 + 1 ) · ( ( i · ( 2 · π ) ) / 3 ) ) = ( ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) + ( 1 · ( ( i · ( 2 · π ) ) / 3 ) ) )
57 2p1e3 ⊢ ( 2 + 1 ) = 3
58 57 oveq1i ⊢ ( ( 2 + 1 ) · ( ( i · ( 2 · π ) ) / 3 ) ) = ( 3 · ( ( i · ( 2 · π ) ) / 3 ) )
59 8 9 10 divcan2i ⊢ ( 3 · ( ( i · ( 2 · π ) ) / 3 ) ) = ( i · ( 2 · π ) )
60 58 59 eqtri ⊢ ( ( 2 + 1 ) · ( ( i · ( 2 · π ) ) / 3 ) ) = ( i · ( 2 · π ) )
61 11 mullidi ⊢ ( 1 · ( ( i · ( 2 · π ) ) / 3 ) ) = ( ( i · ( 2 · π ) ) / 3 )
62 61 oveq2i ⊢ ( ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) + ( 1 · ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) + ( ( i · ( 2 · π ) ) / 3 ) )
63 56 60 62 3eqtr3ri ⊢ ( ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) + ( ( i · ( 2 · π ) ) / 3 ) ) = ( i · ( 2 · π ) )
64 63 fveq2i ⊢ ( exp ‘ ( ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) + ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( exp ‘ ( i · ( 2 · π ) ) )
65 5 11 mulcli ⊢ ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) ∈ ℂ
66 efadd ⊢ ( ( ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) ∈ ℂ ∧ ( ( i · ( 2 · π ) ) / 3 ) ∈ ℂ ) → ( exp ‘ ( ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) + ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( ( exp ‘ ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ) )
67 65 11 66 mp2an ⊢ ( exp ‘ ( ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) + ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( ( exp ‘ ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) )
68 64 67 eqtr3i ⊢ ( exp ‘ ( i · ( 2 · π ) ) ) = ( ( exp ‘ ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) )
69 ef2pi ⊢ ( exp ‘ ( i · ( 2 · π ) ) ) = 1
70 2z ⊢ 2 ∈ ℤ
71 efexp ⊢ ( ( ( ( i · ( 2 · π ) ) / 3 ) ∈ ℂ ∧ 2 ∈ ℤ ) → ( exp ‘ ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 ) )
72 11 70 71 mp2an ⊢ ( exp ‘ ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 )
73 72 oveq1i ⊢ ( ( exp ‘ ( 2 · ( ( i · ( 2 · π ) ) / 3 ) ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 ) · ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) )
74 68 69 73 3eqtr3i ⊢ 1 = ( ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 ) · ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) )
75 divmul3 ⊢ ( ( 1 ∈ ℂ ∧ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 ) ∈ ℂ ∧ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ ℂ ∧ ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ≠ 0 ) ) → ( ( 1 / ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 ) ↔ 1 = ( ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 ) · ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ) ) )
76 75 biimpar ⊢ ( ( ( 1 ∈ ℂ ∧ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 ) ∈ ℂ ∧ ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ∈ ℂ ∧ ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ≠ 0 ) ) ∧ 1 = ( ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 ) · ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ) ) → ( 1 / ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 ) )
77 55 74 76 mp2an ⊢ ( 1 / ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 )
78 1 oveq2i ⊢ ( 1 / 𝑂 ) = ( 1 / ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) )
79 1 oveq1i ⊢ ( 𝑂 ↑ 2 ) = ( ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) ) ↑ 2 )
80 77 78 79 3eqtr4ri ⊢ ( 𝑂 ↑ 2 ) = ( 1 / 𝑂 )
81 2 oveq1i ⊢ ( 𝑍 ↑ 3 ) = ( ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ↑ 3 )
82 3nn ⊢ 3 ∈ ℕ
83 cxproot ⊢ ( ( 𝑂 ∈ ℂ ∧ 3 ∈ ℕ ) → ( ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ↑ 3 ) = 𝑂 )
84 14 82 83 mp2an ⊢ ( ( 𝑂 ↑𝑐 ( 1 / 3 ) ) ↑ 3 ) = 𝑂
85 81 84 eqtr2i ⊢ 𝑂 = ( 𝑍 ↑ 3 )
86 85 oveq1i ⊢ ( 𝑂 ↑ 2 ) = ( ( 𝑍 ↑ 3 ) ↑ 2 )
87 85 oveq2i ⊢ ( 1 / 𝑂 ) = ( 1 / ( 𝑍 ↑ 3 ) )
88 80 86 87 3eqtr3i ⊢ ( ( 𝑍 ↑ 3 ) ↑ 2 ) = ( 1 / ( 𝑍 ↑ 3 ) )
89 3t2e6 ⊢ ( 3 · 2 ) = 6
90 89 oveq2i ⊢ ( 𝑍 ↑ ( 3 · 2 ) ) = ( 𝑍 ↑ 6 )
91 2nn0 ⊢ 2 ∈ ℕ0
92 expmul ⊢ ( ( 𝑍 ∈ ℂ ∧ 3 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 𝑍 ↑ ( 3 · 2 ) ) = ( ( 𝑍 ↑ 3 ) ↑ 2 ) )
93 19 29 91 92 mp3an ⊢ ( 𝑍 ↑ ( 3 · 2 ) ) = ( ( 𝑍 ↑ 3 ) ↑ 2 )
94 90 93 eqtr3i ⊢ ( 𝑍 ↑ 6 ) = ( ( 𝑍 ↑ 3 ) ↑ 2 )
95 3z ⊢ 3 ∈ ℤ
96 exprec ⊢ ( ( 𝑍 ∈ ℂ ∧ 𝑍 ≠ 0 ∧ 3 ∈ ℤ ) → ( ( 1 / 𝑍 ) ↑ 3 ) = ( 1 / ( 𝑍 ↑ 3 ) ) )
97 19 25 95 96 mp3an ⊢ ( ( 1 / 𝑍 ) ↑ 3 ) = ( 1 / ( 𝑍 ↑ 3 ) )
98 88 94 97 3eqtr4i ⊢ ( 𝑍 ↑ 6 ) = ( ( 1 / 𝑍 ) ↑ 3 )
99 98 oveq2i ⊢ ( ( 𝑍 ↑ 3 ) + ( 𝑍 ↑ 6 ) ) = ( ( 𝑍 ↑ 3 ) + ( ( 1 / 𝑍 ) ↑ 3 ) )
100 51 52 99 3eqtr3i ⊢ - 1 = ( ( 𝑍 ↑ 3 ) + ( ( 1 / 𝑍 ) ↑ 3 ) )
101 sqdivid ⊢ ( ( 𝑍 ∈ ℂ ∧ 𝑍 ≠ 0 ) → ( ( 𝑍 ↑ 2 ) / 𝑍 ) = 𝑍 )
102 19 25 101 mp2an ⊢ ( ( 𝑍 ↑ 2 ) / 𝑍 ) = 𝑍
103 19 sqcli ⊢ ( 𝑍 ↑ 2 ) ∈ ℂ
104 103 19 25 divreci ⊢ ( ( 𝑍 ↑ 2 ) / 𝑍 ) = ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) )
105 102 104 eqtr3i ⊢ 𝑍 = ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) )
106 15 5 negsubi ⊢ ( 1 + - 2 ) = ( 1 − 2 )
107 5 15 negsubdi2i ⊢ - ( 2 − 1 ) = ( 1 − 2 )
108 2m1e1 ⊢ ( 2 − 1 ) = 1
109 108 negeqi ⊢ - ( 2 − 1 ) = - 1
110 106 107 109 3eqtr2i ⊢ ( 1 + - 2 ) = - 1
111 110 oveq2i ⊢ ( 𝑍 ↑ ( 1 + - 2 ) ) = ( 𝑍 ↑ - 1 )
112 1z ⊢ 1 ∈ ℤ
113 91 nn0negzi ⊢ - 2 ∈ ℤ
114 expaddz ⊢ ( ( ( 𝑍 ∈ ℂ ∧ 𝑍 ≠ 0 ) ∧ ( 1 ∈ ℤ ∧ - 2 ∈ ℤ ) ) → ( 𝑍 ↑ ( 1 + - 2 ) ) = ( ( 𝑍 ↑ 1 ) · ( 𝑍 ↑ - 2 ) ) )
115 19 25 112 113 114 mp4an ⊢ ( 𝑍 ↑ ( 1 + - 2 ) ) = ( ( 𝑍 ↑ 1 ) · ( 𝑍 ↑ - 2 ) )
116 expn1 ⊢ ( 𝑍 ∈ ℂ → ( 𝑍 ↑ - 1 ) = ( 1 / 𝑍 ) )
117 19 116 ax-mp ⊢ ( 𝑍 ↑ - 1 ) = ( 1 / 𝑍 )
118 111 115 117 3eqtr3i ⊢ ( ( 𝑍 ↑ 1 ) · ( 𝑍 ↑ - 2 ) ) = ( 1 / 𝑍 )
119 exp1 ⊢ ( 𝑍 ∈ ℂ → ( 𝑍 ↑ 1 ) = 𝑍 )
120 19 119 ax-mp ⊢ ( 𝑍 ↑ 1 ) = 𝑍
121 expnegz ⊢ ( ( 𝑍 ∈ ℂ ∧ 𝑍 ≠ 0 ∧ 2 ∈ ℤ ) → ( 𝑍 ↑ - 2 ) = ( 1 / ( 𝑍 ↑ 2 ) ) )
122 19 25 70 121 mp3an ⊢ ( 𝑍 ↑ - 2 ) = ( 1 / ( 𝑍 ↑ 2 ) )
123 19 25 sqrecii ⊢ ( ( 1 / 𝑍 ) ↑ 2 ) = ( 1 / ( 𝑍 ↑ 2 ) )
124 122 123 eqtr4i ⊢ ( 𝑍 ↑ - 2 ) = ( ( 1 / 𝑍 ) ↑ 2 )
125 120 124 oveq12i ⊢ ( ( 𝑍 ↑ 1 ) · ( 𝑍 ↑ - 2 ) ) = ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) )
126 118 125 eqtr3i ⊢ ( 1 / 𝑍 ) = ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) )
127 105 126 oveq12i ⊢ ( 𝑍 + ( 1 / 𝑍 ) ) = ( ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) + ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) )
128 3 127 eqtri ⊢ 𝐴 = ( ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) + ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) )
129 128 oveq2i ⊢ ( 3 · 𝐴 ) = ( 3 · ( ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) + ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) ) )
130 103 26 mulcli ⊢ ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) ∈ ℂ
131 26 sqcli ⊢ ( ( 1 / 𝑍 ) ↑ 2 ) ∈ ℂ
132 19 131 mulcli ⊢ ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) ∈ ℂ
133 9 130 132 adddii ⊢ ( 3 · ( ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) + ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) ) ) = ( ( 3 · ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) ) + ( 3 · ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) ) )
134 129 133 eqtri ⊢ ( 3 · 𝐴 ) = ( ( 3 · ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) ) + ( 3 · ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) ) )
135 100 134 oveq12i ⊢ ( - 1 + ( 3 · 𝐴 ) ) = ( ( ( 𝑍 ↑ 3 ) + ( ( 1 / 𝑍 ) ↑ 3 ) ) + ( ( 3 · ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) ) + ( 3 · ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) ) ) )
136 15 negcli ⊢ - 1 ∈ ℂ
137 9 28 mulcli ⊢ ( 3 · 𝐴 ) ∈ ℂ
138 136 137 addcomi ⊢ ( - 1 + ( 3 · 𝐴 ) ) = ( ( 3 · 𝐴 ) + - 1 )
139 expcl ⊢ ( ( ( 1 / 𝑍 ) ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( ( 1 / 𝑍 ) ↑ 3 ) ∈ ℂ )
140 26 29 139 mp2an ⊢ ( ( 1 / 𝑍 ) ↑ 3 ) ∈ ℂ
141 9 130 mulcli ⊢ ( 3 · ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) ) ∈ ℂ
142 9 132 mulcli ⊢ ( 3 · ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) ) ∈ ℂ
143 50 140 141 142 add42i ⊢ ( ( ( 𝑍 ↑ 3 ) + ( ( 1 / 𝑍 ) ↑ 3 ) ) + ( ( 3 · ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) ) + ( 3 · ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) ) ) ) = ( ( ( 𝑍 ↑ 3 ) + ( 3 · ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) ) ) + ( ( 3 · ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) ) + ( ( 1 / 𝑍 ) ↑ 3 ) ) )
144 135 138 143 3eqtr3i ⊢ ( ( 3 · 𝐴 ) + - 1 ) = ( ( ( 𝑍 ↑ 3 ) + ( 3 · ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) ) ) + ( ( 3 · ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) ) + ( ( 1 / 𝑍 ) ↑ 3 ) ) )
145 39 45 144 3eqtri ⊢ - ( ( - 3 · 𝐴 ) + 1 ) = ( ( ( 𝑍 ↑ 3 ) + ( 3 · ( ( 𝑍 ↑ 2 ) · ( 1 / 𝑍 ) ) ) ) + ( ( 3 · ( 𝑍 · ( ( 1 / 𝑍 ) ↑ 2 ) ) ) + ( ( 1 / 𝑍 ) ↑ 3 ) ) )
146 37 38 145 3eqtr4i ⊢ ( 𝐴 ↑ 3 ) = - ( ( - 3 · 𝐴 ) + 1 )
147 addeq0 ⊢ ( ( ( 𝐴 ↑ 3 ) ∈ ℂ ∧ ( ( - 3 · 𝐴 ) + 1 ) ∈ ℂ ) → ( ( ( 𝐴 ↑ 3 ) + ( ( - 3 · 𝐴 ) + 1 ) ) = 0 ↔ ( 𝐴 ↑ 3 ) = - ( ( - 3 · 𝐴 ) + 1 ) ) )
148 147 biimpar ⊢ ( ( ( ( 𝐴 ↑ 3 ) ∈ ℂ ∧ ( ( - 3 · 𝐴 ) + 1 ) ∈ ℂ ) ∧ ( 𝐴 ↑ 3 ) = - ( ( - 3 · 𝐴 ) + 1 ) ) → ( ( 𝐴 ↑ 3 ) + ( ( - 3 · 𝐴 ) + 1 ) ) = 0 )
149 35 146 148 mp2an ⊢ ( ( 𝐴 ↑ 3 ) + ( ( - 3 · 𝐴 ) + 1 ) ) = 0