Metamath Proof Explorer

Theorem quart

Description: The quartic equation, writing out all roots using square and cube root functions so that only direct substitutions remain, and we can actually claim to have a "quartic equation". Naturally, this theorem is ridiculously long (see quartfull ) if all the substitutions are performed. This is Metamath 100 proof #46. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses quart.a 
|- ( ph -> A e. CC )
quart.b 
|- ( ph -> B e. CC )
quart.c 
|- ( ph -> C e. CC )
quart.d 
|- ( ph -> D e. CC )
quart.x 
|- ( ph -> X e. CC )
quart.e 
|- ( ph -> E = -u ( A / 4 ) )
quart.p 
|- ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )
quart.q 
|- ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )
quart.r 
|- ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )
quart.u 
|- ( ph -> U = ( ( P ^ 2 ) + ( ; 1 2 x. R ) ) )
quart.v 
|- ( ph -> V = ( ( -u ( 2 x. ( P ^ 3 ) ) - ( ; 2 7 x. ( Q ^ 2 ) ) ) + ( ; 7 2 x. ( P x. R ) ) ) )
quart.w 
|- ( ph -> W = ( sqrt ` ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) ) )
quart.s 
|- ( ph -> S = ( ( sqrt ` M ) / 2 ) )
quart.m 
|- ( ph -> M = -u ( ( ( ( 2 x. P ) + T ) + ( U / T ) ) / 3 ) )
quart.t 
|- ( ph -> T = ( ( ( V + W ) / 2 ) ^c ( 1 / 3 ) ) )
quart.t0 
|- ( ph -> T =/= 0 )
quart.m0 
|- ( ph -> M =/= 0 )
quart.i 
|- ( ph -> I = ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) + ( ( Q / 4 ) / S ) ) ) )
quart.j 
|- ( ph -> J = ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) - ( ( Q / 4 ) / S ) ) ) )
Assertion quart 
|- ( ph -> ( ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( B x. ( X ^ 2 ) ) + ( ( C x. X ) + D ) ) ) = 0 <-> ( ( X = ( ( E - S ) + I ) \/ X = ( ( E - S ) - I ) ) \/ ( X = ( ( E + S ) + J ) \/ X = ( ( E + S ) - J ) ) ) ) )

Proof

Step Hyp Ref Expression
1 quart.a 
 |-  ( ph -> A e. CC )
2 quart.b 
 |-  ( ph -> B e. CC )
3 quart.c 
 |-  ( ph -> C e. CC )
4 quart.d 
 |-  ( ph -> D e. CC )
5 quart.x 
 |-  ( ph -> X e. CC )
6 quart.e 
 |-  ( ph -> E = -u ( A / 4 ) )
7 quart.p 
 |-  ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )
8 quart.q 
 |-  ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )
9 quart.r 
 |-  ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )
10 quart.u 
 |-  ( ph -> U = ( ( P ^ 2 ) + ( ; 1 2 x. R ) ) )
11 quart.v 
 |-  ( ph -> V = ( ( -u ( 2 x. ( P ^ 3 ) ) - ( ; 2 7 x. ( Q ^ 2 ) ) ) + ( ; 7 2 x. ( P x. R ) ) ) )
12 quart.w 
 |-  ( ph -> W = ( sqrt ` ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) ) )
13 quart.s 
 |-  ( ph -> S = ( ( sqrt ` M ) / 2 ) )
14 quart.m 
 |-  ( ph -> M = -u ( ( ( ( 2 x. P ) + T ) + ( U / T ) ) / 3 ) )
15 quart.t 
 |-  ( ph -> T = ( ( ( V + W ) / 2 ) ^c ( 1 / 3 ) ) )
16 quart.t0 
 |-  ( ph -> T =/= 0 )
17 quart.m0 
 |-  ( ph -> M =/= 0 )
18 quart.i 
 |-  ( ph -> I = ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) + ( ( Q / 4 ) / S ) ) ) )
19 quart.j 
 |-  ( ph -> J = ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) - ( ( Q / 4 ) / S ) ) ) )
20 6 oveq2d 
 |-  ( ph -> ( X - E ) = ( X - -u ( A / 4 ) ) )
21 4cn 
 |-  4 e. CC
22 21 a1i 
 |-  ( ph -> 4 e. CC )
23 4ne0 
 |-  4 =/= 0
24 23 a1i 
 |-  ( ph -> 4 =/= 0 )
25 1 22 24 divcld 
 |-  ( ph -> ( A / 4 ) e. CC )
26 5 25 subnegd 
 |-  ( ph -> ( X - -u ( A / 4 ) ) = ( X + ( A / 4 ) ) )
27 20 26 eqtrd 
 |-  ( ph -> ( X - E ) = ( X + ( A / 4 ) ) )
28 1 2 3 4 7 8 9 5 27 quart1 
 |-  ( ph -> ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( B x. ( X ^ 2 ) ) + ( ( C x. X ) + D ) ) ) = ( ( ( ( X - E ) ^ 4 ) + ( P x. ( ( X - E ) ^ 2 ) ) ) + ( ( Q x. ( X - E ) ) + R ) ) )
29 28 eqeq1d 
 |-  ( ph -> ( ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( B x. ( X ^ 2 ) ) + ( ( C x. X ) + D ) ) ) = 0 <-> ( ( ( ( X - E ) ^ 4 ) + ( P x. ( ( X - E ) ^ 2 ) ) ) + ( ( Q x. ( X - E ) ) + R ) ) = 0 ) )
30 1 2 3 4 7 8 9 quart1cl 
 |-  ( ph -> ( P e. CC /\ Q e. CC /\ R e. CC ) )
31 30 simp1d 
 |-  ( ph -> P e. CC )
32 30 simp2d 
 |-  ( ph -> Q e. CC )
33 25 negcld 
 |-  ( ph -> -u ( A / 4 ) e. CC )
34 6 33 eqeltrd 
 |-  ( ph -> E e. CC )
35 5 34 subcld 
 |-  ( ph -> ( X - E ) e. CC )
36 1 2 3 4 1 6 7 8 9 10 11 12 13 14 15 16 quartlem3 
 |-  ( ph -> ( S e. CC /\ M e. CC /\ T e. CC ) )
37 36 simp1d 
 |-  ( ph -> S e. CC )
38 13 oveq2d 
 |-  ( ph -> ( 2 x. S ) = ( 2 x. ( ( sqrt ` M ) / 2 ) ) )
39 36 simp2d 
 |-  ( ph -> M e. CC )
40 39 sqrtcld 
 |-  ( ph -> ( sqrt ` M ) e. CC )
41 2cnd 
 |-  ( ph -> 2 e. CC )
42 2ne0 
 |-  2 =/= 0
43 42 a1i 
 |-  ( ph -> 2 =/= 0 )
44 40 41 43 divcan2d 
 |-  ( ph -> ( 2 x. ( ( sqrt ` M ) / 2 ) ) = ( sqrt ` M ) )
45 38 44 eqtrd 
 |-  ( ph -> ( 2 x. S ) = ( sqrt ` M ) )
46 45 oveq1d 
 |-  ( ph -> ( ( 2 x. S ) ^ 2 ) = ( ( sqrt ` M ) ^ 2 ) )
47 39 sqsqrtd 
 |-  ( ph -> ( ( sqrt ` M ) ^ 2 ) = M )
48 46 47 eqtr2d 
 |-  ( ph -> M = ( ( 2 x. S ) ^ 2 ) )
49 1 2 3 4 1 6 7 8 9 10 11 12 13 14 15 16 17 18 19 quartlem4 
 |-  ( ph -> ( S =/= 0 /\ I e. CC /\ J e. CC ) )
50 49 simp2d 
 |-  ( ph -> I e. CC )
51 18 oveq1d 
 |-  ( ph -> ( I ^ 2 ) = ( ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) + ( ( Q / 4 ) / S ) ) ) ^ 2 ) )
52 37 sqcld 
 |-  ( ph -> ( S ^ 2 ) e. CC )
53 52 negcld 
 |-  ( ph -> -u ( S ^ 2 ) e. CC )
54 31 halfcld 
 |-  ( ph -> ( P / 2 ) e. CC )
55 53 54 subcld 
 |-  ( ph -> ( -u ( S ^ 2 ) - ( P / 2 ) ) e. CC )
56 32 22 24 divcld 
 |-  ( ph -> ( Q / 4 ) e. CC )
57 49 simp1d 
 |-  ( ph -> S =/= 0 )
58 56 37 57 divcld 
 |-  ( ph -> ( ( Q / 4 ) / S ) e. CC )
59 55 58 addcld 
 |-  ( ph -> ( ( -u ( S ^ 2 ) - ( P / 2 ) ) + ( ( Q / 4 ) / S ) ) e. CC )
60 59 sqsqrtd 
 |-  ( ph -> ( ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) + ( ( Q / 4 ) / S ) ) ) ^ 2 ) = ( ( -u ( S ^ 2 ) - ( P / 2 ) ) + ( ( Q / 4 ) / S ) ) )
61 51 60 eqtrd 
 |-  ( ph -> ( I ^ 2 ) = ( ( -u ( S ^ 2 ) - ( P / 2 ) ) + ( ( Q / 4 ) / S ) ) )
62 30 simp3d 
 |-  ( ph -> R e. CC )
63 1cnd 
 |-  ( ph -> 1 e. CC )
64 3z 
 |-  3 e. ZZ
65 1exp 
 |-  ( 3 e. ZZ -> ( 1 ^ 3 ) = 1 )
66 64 65 mp1i 
 |-  ( ph -> ( 1 ^ 3 ) = 1 )
67 36 simp3d 
 |-  ( ph -> T e. CC )
68 67 mulid2d 
 |-  ( ph -> ( 1 x. T ) = T )
69 68 oveq2d 
 |-  ( ph -> ( ( 2 x. P ) + ( 1 x. T ) ) = ( ( 2 x. P ) + T ) )
70 68 oveq2d 
 |-  ( ph -> ( U / ( 1 x. T ) ) = ( U / T ) )
71 69 70 oveq12d 
 |-  ( ph -> ( ( ( 2 x. P ) + ( 1 x. T ) ) + ( U / ( 1 x. T ) ) ) = ( ( ( 2 x. P ) + T ) + ( U / T ) ) )
72 71 oveq1d 
 |-  ( ph -> ( ( ( ( 2 x. P ) + ( 1 x. T ) ) + ( U / ( 1 x. T ) ) ) / 3 ) = ( ( ( ( 2 x. P ) + T ) + ( U / T ) ) / 3 ) )
73 72 negeqd 
 |-  ( ph -> -u ( ( ( ( 2 x. P ) + ( 1 x. T ) ) + ( U / ( 1 x. T ) ) ) / 3 ) = -u ( ( ( ( 2 x. P ) + T ) + ( U / T ) ) / 3 ) )
74 14 73 eqtr4d 
 |-  ( ph -> M = -u ( ( ( ( 2 x. P ) + ( 1 x. T ) ) + ( U / ( 1 x. T ) ) ) / 3 ) )
75 oveq1 
 |-  ( x = 1 -> ( x ^ 3 ) = ( 1 ^ 3 ) )
76 75 eqeq1d 
 |-  ( x = 1 -> ( ( x ^ 3 ) = 1 <-> ( 1 ^ 3 ) = 1 ) )
77 oveq1 
 |-  ( x = 1 -> ( x x. T ) = ( 1 x. T ) )
78 77 oveq2d 
 |-  ( x = 1 -> ( ( 2 x. P ) + ( x x. T ) ) = ( ( 2 x. P ) + ( 1 x. T ) ) )
79 77 oveq2d 
 |-  ( x = 1 -> ( U / ( x x. T ) ) = ( U / ( 1 x. T ) ) )
80 78 79 oveq12d 
 |-  ( x = 1 -> ( ( ( 2 x. P ) + ( x x. T ) ) + ( U / ( x x. T ) ) ) = ( ( ( 2 x. P ) + ( 1 x. T ) ) + ( U / ( 1 x. T ) ) ) )
81 80 oveq1d 
 |-  ( x = 1 -> ( ( ( ( 2 x. P ) + ( x x. T ) ) + ( U / ( x x. T ) ) ) / 3 ) = ( ( ( ( 2 x. P ) + ( 1 x. T ) ) + ( U / ( 1 x. T ) ) ) / 3 ) )
82 81 negeqd 
 |-  ( x = 1 -> -u ( ( ( ( 2 x. P ) + ( x x. T ) ) + ( U / ( x x. T ) ) ) / 3 ) = -u ( ( ( ( 2 x. P ) + ( 1 x. T ) ) + ( U / ( 1 x. T ) ) ) / 3 ) )
83 82 eqeq2d 
 |-  ( x = 1 -> ( M = -u ( ( ( ( 2 x. P ) + ( x x. T ) ) + ( U / ( x x. T ) ) ) / 3 ) <-> M = -u ( ( ( ( 2 x. P ) + ( 1 x. T ) ) + ( U / ( 1 x. T ) ) ) / 3 ) ) )
84 76 83 anbi12d 
 |-  ( x = 1 -> ( ( ( x ^ 3 ) = 1 /\ M = -u ( ( ( ( 2 x. P ) + ( x x. T ) ) + ( U / ( x x. T ) ) ) / 3 ) ) <-> ( ( 1 ^ 3 ) = 1 /\ M = -u ( ( ( ( 2 x. P ) + ( 1 x. T ) ) + ( U / ( 1 x. T ) ) ) / 3 ) ) ) )
85 84 rspcev 
 |-  ( ( 1 e. CC /\ ( ( 1 ^ 3 ) = 1 /\ M = -u ( ( ( ( 2 x. P ) + ( 1 x. T ) ) + ( U / ( 1 x. T ) ) ) / 3 ) ) ) -> E. x e. CC ( ( x ^ 3 ) = 1 /\ M = -u ( ( ( ( 2 x. P ) + ( x x. T ) ) + ( U / ( x x. T ) ) ) / 3 ) ) )
86 63 66 74 85 syl12anc 
 |-  ( ph -> E. x e. CC ( ( x ^ 3 ) = 1 /\ M = -u ( ( ( ( 2 x. P ) + ( x x. T ) ) + ( U / ( x x. T ) ) ) / 3 ) ) )
87 2cn 
 |-  2 e. CC
88 mulcl 
 |-  ( ( 2 e. CC /\ P e. CC ) -> ( 2 x. P ) e. CC )
89 87 31 88 sylancr 
 |-  ( ph -> ( 2 x. P ) e. CC )
90 31 sqcld 
 |-  ( ph -> ( P ^ 2 ) e. CC )
91 mulcl 
 |-  ( ( 4 e. CC /\ R e. CC ) -> ( 4 x. R ) e. CC )
92 21 62 91 sylancr 
 |-  ( ph -> ( 4 x. R ) e. CC )
93 90 92 subcld 
 |-  ( ph -> ( ( P ^ 2 ) - ( 4 x. R ) ) e. CC )
94 32 sqcld 
 |-  ( ph -> ( Q ^ 2 ) e. CC )
95 94 negcld 
 |-  ( ph -> -u ( Q ^ 2 ) e. CC )
96 15 oveq1d 
 |-  ( ph -> ( T ^ 3 ) = ( ( ( ( V + W ) / 2 ) ^c ( 1 / 3 ) ) ^ 3 ) )
97 1 2 3 4 1 6 7 8 9 10 11 12 quartlem2 
 |-  ( ph -> ( U e. CC /\ V e. CC /\ W e. CC ) )
98 97 simp2d 
 |-  ( ph -> V e. CC )
99 97 simp3d 
 |-  ( ph -> W e. CC )
100 98 99 addcld 
 |-  ( ph -> ( V + W ) e. CC )
101 100 halfcld 
 |-  ( ph -> ( ( V + W ) / 2 ) e. CC )
102 3nn 
 |-  3 e. NN
103 cxproot 
 |-  ( ( ( ( V + W ) / 2 ) e. CC /\ 3 e. NN ) -> ( ( ( ( V + W ) / 2 ) ^c ( 1 / 3 ) ) ^ 3 ) = ( ( V + W ) / 2 ) )
104 101 102 103 sylancl 
 |-  ( ph -> ( ( ( ( V + W ) / 2 ) ^c ( 1 / 3 ) ) ^ 3 ) = ( ( V + W ) / 2 ) )
105 96 104 eqtrd 
 |-  ( ph -> ( T ^ 3 ) = ( ( V + W ) / 2 ) )
106 12 oveq1d 
 |-  ( ph -> ( W ^ 2 ) = ( ( sqrt ` ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) ) ^ 2 ) )
107 98 sqcld 
 |-  ( ph -> ( V ^ 2 ) e. CC )
108 97 simp1d 
 |-  ( ph -> U e. CC )
109 3nn0 
 |-  3 e. NN0
110 expcl 
 |-  ( ( U e. CC /\ 3 e. NN0 ) -> ( U ^ 3 ) e. CC )
111 108 109 110 sylancl 
 |-  ( ph -> ( U ^ 3 ) e. CC )
112 mulcl 
 |-  ( ( 4 e. CC /\ ( U ^ 3 ) e. CC ) -> ( 4 x. ( U ^ 3 ) ) e. CC )
113 21 111 112 sylancr 
 |-  ( ph -> ( 4 x. ( U ^ 3 ) ) e. CC )
114 107 113 subcld 
 |-  ( ph -> ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) e. CC )
115 114 sqsqrtd 
 |-  ( ph -> ( ( sqrt ` ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) ) ^ 2 ) = ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) )
116 106 115 eqtrd 
 |-  ( ph -> ( W ^ 2 ) = ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) )
117 31 32 62 10 11 quartlem1 
 |-  ( ph -> ( U = ( ( ( 2 x. P ) ^ 2 ) - ( 3 x. ( ( P ^ 2 ) - ( 4 x. R ) ) ) ) /\ V = ( ( ( 2 x. ( ( 2 x. P ) ^ 3 ) ) - ( 9 x. ( ( 2 x. P ) x. ( ( P ^ 2 ) - ( 4 x. R ) ) ) ) ) + ( ; 2 7 x. -u ( Q ^ 2 ) ) ) ) )
118 117 simpld 
 |-  ( ph -> U = ( ( ( 2 x. P ) ^ 2 ) - ( 3 x. ( ( P ^ 2 ) - ( 4 x. R ) ) ) ) )
119 117 simprd 
 |-  ( ph -> V = ( ( ( 2 x. ( ( 2 x. P ) ^ 3 ) ) - ( 9 x. ( ( 2 x. P ) x. ( ( P ^ 2 ) - ( 4 x. R ) ) ) ) ) + ( ; 2 7 x. -u ( Q ^ 2 ) ) ) )
120 89 93 95 39 67 105 99 116 118 119 16 mcubic 
 |-  ( ph -> ( ( ( ( M ^ 3 ) + ( ( 2 x. P ) x. ( M ^ 2 ) ) ) + ( ( ( ( P ^ 2 ) - ( 4 x. R ) ) x. M ) + -u ( Q ^ 2 ) ) ) = 0 <-> E. x e. CC ( ( x ^ 3 ) = 1 /\ M = -u ( ( ( ( 2 x. P ) + ( x x. T ) ) + ( U / ( x x. T ) ) ) / 3 ) ) ) )
121 86 120 mpbird 
 |-  ( ph -> ( ( ( M ^ 3 ) + ( ( 2 x. P ) x. ( M ^ 2 ) ) ) + ( ( ( ( P ^ 2 ) - ( 4 x. R ) ) x. M ) + -u ( Q ^ 2 ) ) ) = 0 )
122 49 simp3d 
 |-  ( ph -> J e. CC )
123 19 oveq1d 
 |-  ( ph -> ( J ^ 2 ) = ( ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) - ( ( Q / 4 ) / S ) ) ) ^ 2 ) )
124 55 58 subcld 
 |-  ( ph -> ( ( -u ( S ^ 2 ) - ( P / 2 ) ) - ( ( Q / 4 ) / S ) ) e. CC )
125 124 sqsqrtd 
 |-  ( ph -> ( ( sqrt ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) - ( ( Q / 4 ) / S ) ) ) ^ 2 ) = ( ( -u ( S ^ 2 ) - ( P / 2 ) ) - ( ( Q / 4 ) / S ) ) )
126 123 125 eqtrd 
 |-  ( ph -> ( J ^ 2 ) = ( ( -u ( S ^ 2 ) - ( P / 2 ) ) - ( ( Q / 4 ) / S ) ) )
127 31 32 35 37 48 17 50 61 62 121 122 126 dquart 
 |-  ( ph -> ( ( ( ( ( X - E ) ^ 4 ) + ( P x. ( ( X - E ) ^ 2 ) ) ) + ( ( Q x. ( X - E ) ) + R ) ) = 0 <-> ( ( ( X - E ) = ( -u S + I ) \/ ( X - E ) = ( -u S - I ) ) \/ ( ( X - E ) = ( S + J ) \/ ( X - E ) = ( S - J ) ) ) ) )
128 37 negcld 
 |-  ( ph -> -u S e. CC )
129 128 50 addcld 
 |-  ( ph -> ( -u S + I ) e. CC )
130 5 34 129 subaddd 
 |-  ( ph -> ( ( X - E ) = ( -u S + I ) <-> ( E + ( -u S + I ) ) = X ) )
131 34 37 negsubd 
 |-  ( ph -> ( E + -u S ) = ( E - S ) )
132 131 oveq1d 
 |-  ( ph -> ( ( E + -u S ) + I ) = ( ( E - S ) + I ) )
133 34 128 50 addassd 
 |-  ( ph -> ( ( E + -u S ) + I ) = ( E + ( -u S + I ) ) )
134 132 133 eqtr3d 
 |-  ( ph -> ( ( E - S ) + I ) = ( E + ( -u S + I ) ) )
135 134 eqeq1d 
 |-  ( ph -> ( ( ( E - S ) + I ) = X <-> ( E + ( -u S + I ) ) = X ) )
136 130 135 bitr4d 
 |-  ( ph -> ( ( X - E ) = ( -u S + I ) <-> ( ( E - S ) + I ) = X ) )
137 eqcom 
 |-  ( ( ( E - S ) + I ) = X <-> X = ( ( E - S ) + I ) )
138 136 137 bitrdi 
 |-  ( ph -> ( ( X - E ) = ( -u S + I ) <-> X = ( ( E - S ) + I ) ) )
139 128 50 subcld 
 |-  ( ph -> ( -u S - I ) e. CC )
140 5 34 139 subaddd 
 |-  ( ph -> ( ( X - E ) = ( -u S - I ) <-> ( E + ( -u S - I ) ) = X ) )
141 131 oveq1d 
 |-  ( ph -> ( ( E + -u S ) - I ) = ( ( E - S ) - I ) )
142 34 128 50 addsubassd 
 |-  ( ph -> ( ( E + -u S ) - I ) = ( E + ( -u S - I ) ) )
143 141 142 eqtr3d 
 |-  ( ph -> ( ( E - S ) - I ) = ( E + ( -u S - I ) ) )
144 143 eqeq1d 
 |-  ( ph -> ( ( ( E - S ) - I ) = X <-> ( E + ( -u S - I ) ) = X ) )
145 140 144 bitr4d 
 |-  ( ph -> ( ( X - E ) = ( -u S - I ) <-> ( ( E - S ) - I ) = X ) )
146 eqcom 
 |-  ( ( ( E - S ) - I ) = X <-> X = ( ( E - S ) - I ) )
147 145 146 bitrdi 
 |-  ( ph -> ( ( X - E ) = ( -u S - I ) <-> X = ( ( E - S ) - I ) ) )
148 138 147 orbi12d 
 |-  ( ph -> ( ( ( X - E ) = ( -u S + I ) \/ ( X - E ) = ( -u S - I ) ) <-> ( X = ( ( E - S ) + I ) \/ X = ( ( E - S ) - I ) ) ) )
149 37 122 addcld 
 |-  ( ph -> ( S + J ) e. CC )
150 5 34 149 subaddd 
 |-  ( ph -> ( ( X - E ) = ( S + J ) <-> ( E + ( S + J ) ) = X ) )
151 34 37 122 addassd 
 |-  ( ph -> ( ( E + S ) + J ) = ( E + ( S + J ) ) )
152 151 eqeq1d 
 |-  ( ph -> ( ( ( E + S ) + J ) = X <-> ( E + ( S + J ) ) = X ) )
153 150 152 bitr4d 
 |-  ( ph -> ( ( X - E ) = ( S + J ) <-> ( ( E + S ) + J ) = X ) )
154 eqcom 
 |-  ( ( ( E + S ) + J ) = X <-> X = ( ( E + S ) + J ) )
155 153 154 bitrdi 
 |-  ( ph -> ( ( X - E ) = ( S + J ) <-> X = ( ( E + S ) + J ) ) )
156 37 122 subcld 
 |-  ( ph -> ( S - J ) e. CC )
157 5 34 156 subaddd 
 |-  ( ph -> ( ( X - E ) = ( S - J ) <-> ( E + ( S - J ) ) = X ) )
158 34 37 122 addsubassd 
 |-  ( ph -> ( ( E + S ) - J ) = ( E + ( S - J ) ) )
159 158 eqeq1d 
 |-  ( ph -> ( ( ( E + S ) - J ) = X <-> ( E + ( S - J ) ) = X ) )
160 157 159 bitr4d 
 |-  ( ph -> ( ( X - E ) = ( S - J ) <-> ( ( E + S ) - J ) = X ) )
161 eqcom 
 |-  ( ( ( E + S ) - J ) = X <-> X = ( ( E + S ) - J ) )
162 160 161 bitrdi 
 |-  ( ph -> ( ( X - E ) = ( S - J ) <-> X = ( ( E + S ) - J ) ) )
163 155 162 orbi12d 
 |-  ( ph -> ( ( ( X - E ) = ( S + J ) \/ ( X - E ) = ( S - J ) ) <-> ( X = ( ( E + S ) + J ) \/ X = ( ( E + S ) - J ) ) ) )
164 148 163 orbi12d 
 |-  ( ph -> ( ( ( ( X - E ) = ( -u S + I ) \/ ( X - E ) = ( -u S - I ) ) \/ ( ( X - E ) = ( S + J ) \/ ( X - E ) = ( S - J ) ) ) <-> ( ( X = ( ( E - S ) + I ) \/ X = ( ( E - S ) - I ) ) \/ ( X = ( ( E + S ) + J ) \/ X = ( ( E + S ) - J ) ) ) ) )
165 29 127 164 3bitrd 
 |-  ( ph -> ( ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( B x. ( X ^ 2 ) ) + ( ( C x. X ) + D ) ) ) = 0 <-> ( ( X = ( ( E - S ) + I ) \/ X = ( ( E - S ) - I ) ) \/ ( X = ( ( E + S ) + J ) \/ X = ( ( E + S ) - J ) ) ) ) )