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 
|- O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) )
cos9thpiminplylem4.2 
|- Z = ( O ^c ( 1 / 3 ) )
cos9thpiminplylem5.3 
|- A = ( Z + ( 1 / Z ) )
Assertion cos9thpiminplylem5 
|- ( ( A ^ 3 ) + ( ( -u 3 x. A ) + 1 ) ) = 0

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