Metamath Proof Explorer


Theorem dquart

Description: Solve a depressed quartic equation. To eliminate S , which is the square root of a solution M to the resolvent cubic equation, apply cubic or one of its variants. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses dquart.b φ B
dquart.c φ C
dquart.x φ X
dquart.s φ S
dquart.m φ M = 2 S 2
dquart.m0 φ M 0
dquart.i φ I
dquart.i2 φ I 2 = S 2 - B 2 + C 4 S
dquart.d φ D
dquart.3 φ M 3 + 2 B M 2 + B 2 4 D M + C 2 = 0
dquart.j φ J
dquart.j2 φ J 2 = S 2 - B 2 - C 4 S
Assertion dquart φ X 4 + B X 2 + C X + D = 0 X = - S + I X = - S - I X = S + J X = S J

Proof

Step Hyp Ref Expression
1 dquart.b φ B
2 dquart.c φ C
3 dquart.x φ X
4 dquart.s φ S
5 dquart.m φ M = 2 S 2
6 dquart.m0 φ M 0
7 dquart.i φ I
8 dquart.i2 φ I 2 = S 2 - B 2 + C 4 S
9 dquart.d φ D
10 dquart.3 φ M 3 + 2 B M 2 + B 2 4 D M + C 2 = 0
11 dquart.j φ J
12 dquart.j2 φ J 2 = S 2 - B 2 - C 4 S
13 3 sqcld φ X 2
14 2cn 2
15 mulcl 2 S 2 S
16 14 4 15 sylancr φ 2 S
17 16 sqcld φ 2 S 2
18 5 17 eqeltrd φ M
19 18 1 addcld φ M + B
20 19 halfcld φ M + B 2
21 binom2 X 2 M + B 2 X 2 + M + B 2 2 = X 2 2 + 2 X 2 M + B 2 + M + B 2 2
22 13 20 21 syl2anc φ X 2 + M + B 2 2 = X 2 2 + 2 X 2 M + B 2 + M + B 2 2
23 2nn0 2 0
24 23 a1i φ 2 0
25 3 24 24 expmuld φ X 2 2 = X 2 2
26 2t2e4 2 2 = 4
27 26 oveq2i X 2 2 = X 4
28 25 27 eqtr3di φ X 2 2 = X 4
29 14 a1i φ 2
30 29 13 20 mul12d φ 2 X 2 M + B 2 = X 2 2 M + B 2
31 2ne0 2 0
32 31 a1i φ 2 0
33 19 29 32 divcan2d φ 2 M + B 2 = M + B
34 33 oveq2d φ X 2 2 M + B 2 = X 2 M + B
35 13 19 mulcomd φ X 2 M + B = M + B X 2
36 34 35 eqtrd φ X 2 2 M + B 2 = M + B X 2
37 18 1 13 adddird φ M + B X 2 = M X 2 + B X 2
38 30 36 37 3eqtrd φ 2 X 2 M + B 2 = M X 2 + B X 2
39 28 38 oveq12d φ X 2 2 + 2 X 2 M + B 2 = X 4 + M X 2 + B X 2
40 4nn0 4 0
41 expcl X 4 0 X 4
42 3 40 41 sylancl φ X 4
43 18 13 mulcld φ M X 2
44 1 13 mulcld φ B X 2
45 42 43 44 add12d φ X 4 + M X 2 + B X 2 = M X 2 + X 4 + B X 2
46 39 45 eqtrd φ X 2 2 + 2 X 2 M + B 2 = M X 2 + X 4 + B X 2
47 46 oveq1d φ X 2 2 + 2 X 2 M + B 2 + M + B 2 2 = M X 2 + X 4 + B X 2 + M + B 2 2
48 42 44 addcld φ X 4 + B X 2
49 20 sqcld φ M + B 2 2
50 43 48 49 addassd φ M X 2 + X 4 + B X 2 + M + B 2 2 = M X 2 + X 4 + B X 2 + M + B 2 2
51 22 47 50 3eqtrd φ X 2 + M + B 2 2 = M X 2 + X 4 + B X 2 + M + B 2 2
52 18 halfcld φ M 2
53 52 3 mulcld φ M 2 X
54 4cn 4
55 54 a1i φ 4
56 4ne0 4 0
57 56 a1i φ 4 0
58 2 55 57 divcld φ C 4
59 53 58 subcld φ M 2 X C 4
60 5 6 eqnetrrd φ 2 S 2 0
61 sqne0 2 S 2 S 2 0 2 S 0
62 16 61 syl φ 2 S 2 0 2 S 0
63 60 62 mpbid φ 2 S 0
64 mulne0b 2 S 2 0 S 0 2 S 0
65 14 4 64 sylancr φ 2 0 S 0 2 S 0
66 63 65 mpbird φ 2 0 S 0
67 66 simprd φ S 0
68 59 4 29 67 32 divcan5d φ 2 M 2 X C 4 2 S = M 2 X C 4 S
69 29 53 58 subdid φ 2 M 2 X C 4 = 2 M 2 X 2 C 4
70 29 52 3 mulassd φ 2 M 2 X = 2 M 2 X
71 18 29 32 divcan2d φ 2 M 2 = M
72 71 oveq1d φ 2 M 2 X = M X
73 70 72 eqtr3d φ 2 M 2 X = M X
74 29 2 55 57 divassd φ 2 C 4 = 2 C 4
75 26 oveq2i 2 C 2 2 = 2 C 4
76 2 29 29 32 32 divcan5d φ 2 C 2 2 = C 2
77 75 76 eqtr3id φ 2 C 4 = C 2
78 74 77 eqtr3d φ 2 C 4 = C 2
79 73 78 oveq12d φ 2 M 2 X 2 C 4 = M X C 2
80 69 79 eqtrd φ 2 M 2 X C 4 = M X C 2
81 80 oveq1d φ 2 M 2 X C 4 2 S = M X C 2 2 S
82 68 81 eqtr3d φ M 2 X C 4 S = M X C 2 2 S
83 82 oveq1d φ M 2 X C 4 S 2 = M X C 2 2 S 2
84 18 3 mulcld φ M X
85 2 halfcld φ C 2
86 84 85 subcld φ M X C 2
87 86 16 63 sqdivd φ M X C 2 2 S 2 = M X C 2 2 2 S 2
88 18 sqcld φ M 2
89 88 13 mulcld φ M 2 X 2
90 84 2 mulcld φ M X C
91 89 90 subcld φ M 2 X 2 M X C
92 2 sqcld φ C 2
93 92 55 57 divcld φ C 2 4
94 91 93 18 6 divdird φ M 2 X 2 - M X C + C 2 4 M = M 2 X 2 M X C M + C 2 4 M
95 binom2sub M X C 2 M X C 2 2 = M X 2 - 2 M X C 2 + C 2 2
96 84 85 95 syl2anc φ M X C 2 2 = M X 2 - 2 M X C 2 + C 2 2
97 18 3 sqmuld φ M X 2 = M 2 X 2
98 29 84 85 mul12d φ 2 M X C 2 = M X 2 C 2
99 2 29 32 divcan2d φ 2 C 2 = C
100 99 oveq2d φ M X 2 C 2 = M X C
101 98 100 eqtrd φ 2 M X C 2 = M X C
102 97 101 oveq12d φ M X 2 2 M X C 2 = M 2 X 2 M X C
103 2 29 32 sqdivd φ C 2 2 = C 2 2 2
104 sq2 2 2 = 4
105 104 oveq2i C 2 2 2 = C 2 4
106 103 105 eqtrdi φ C 2 2 = C 2 4
107 102 106 oveq12d φ M X 2 - 2 M X C 2 + C 2 2 = M 2 X 2 - M X C + C 2 4
108 96 107 eqtr2d φ M 2 X 2 - M X C + C 2 4 = M X C 2 2
109 108 5 oveq12d φ M 2 X 2 - M X C + C 2 4 M = M X C 2 2 2 S 2
110 89 90 18 6 divsubdird φ M 2 X 2 M X C M = M 2 X 2 M M X C M
111 88 13 18 6 div23d φ M 2 X 2 M = M 2 M X 2
112 18 sqvald φ M 2 = M M
113 112 oveq1d φ M 2 M = M M M
114 18 18 6 divcan3d φ M M M = M
115 113 114 eqtrd φ M 2 M = M
116 115 oveq1d φ M 2 M X 2 = M X 2
117 111 116 eqtrd φ M 2 X 2 M = M X 2
118 18 3 2 mul32d φ M X C = M C X
119 18 2 3 mulassd φ M C X = M C X
120 118 119 eqtrd φ M X C = M C X
121 120 oveq1d φ M X C M = M C X M
122 2 3 mulcld φ C X
123 122 18 6 divcan3d φ M C X M = C X
124 121 123 eqtrd φ M X C M = C X
125 117 124 oveq12d φ M 2 X 2 M M X C M = M X 2 C X
126 110 125 eqtrd φ M 2 X 2 M X C M = M X 2 C X
127 126 oveq1d φ M 2 X 2 M X C M + C 2 4 M = M X 2 - C X + C 2 4 M
128 93 18 6 divcld φ C 2 4 M
129 43 122 128 subsubd φ M X 2 C X C 2 4 M = M X 2 - C X + C 2 4 M
130 127 129 eqtr4d φ M 2 X 2 M X C M + C 2 4 M = M X 2 C X C 2 4 M
131 94 109 130 3eqtr3d φ M X C 2 2 2 S 2 = M X 2 C X C 2 4 M
132 83 87 131 3eqtrd φ M 2 X C 4 S 2 = M X 2 C X C 2 4 M
133 51 132 oveq12d φ X 2 + M + B 2 2 M 2 X C 4 S 2 = M X 2 + X 4 + B X 2 + M + B 2 2 - M X 2 C X C 2 4 M
134 48 49 addcld φ X 4 + B X 2 + M + B 2 2
135 122 128 subcld φ C X C 2 4 M
136 43 134 135 pnncand φ M X 2 + X 4 + B X 2 + M + B 2 2 - M X 2 C X C 2 4 M = X 4 + B X 2 + M + B 2 2 + C X C 2 4 M
137 128 negcld φ C 2 4 M
138 48 49 122 137 add4d φ X 4 + B X 2 + M + B 2 2 + C X + C 2 4 M = X 4 + B X 2 + C X + M + B 2 2 + C 2 4 M
139 122 128 negsubd φ C X + C 2 4 M = C X C 2 4 M
140 139 oveq2d φ X 4 + B X 2 + M + B 2 2 + C X + C 2 4 M = X 4 + B X 2 + M + B 2 2 + C X C 2 4 M
141 49 128 negsubd φ M + B 2 2 + C 2 4 M = M + B 2 2 C 2 4 M
142 1 2 3 4 5 6 7 8 9 10 dquartlem2 φ M + B 2 2 C 2 4 M = D
143 141 142 eqtrd φ M + B 2 2 + C 2 4 M = D
144 143 oveq2d φ X 4 + B X 2 + C X + M + B 2 2 + C 2 4 M = X 4 + B X 2 + C X + D
145 48 122 9 addassd φ X 4 + B X 2 + C X + D = X 4 + B X 2 + C X + D
146 144 145 eqtrd φ X 4 + B X 2 + C X + M + B 2 2 + C 2 4 M = X 4 + B X 2 + C X + D
147 138 140 146 3eqtr3d φ X 4 + B X 2 + M + B 2 2 + C X C 2 4 M = X 4 + B X 2 + C X + D
148 133 136 147 3eqtrd φ X 2 + M + B 2 2 M 2 X C 4 S 2 = X 4 + B X 2 + C X + D
149 13 20 addcld φ X 2 + M + B 2
150 59 4 67 divcld φ M 2 X C 4 S
151 subsq X 2 + M + B 2 M 2 X C 4 S X 2 + M + B 2 2 M 2 X C 4 S 2 = X 2 + M + B 2 + M 2 X C 4 S X 2 + M + B 2 - M 2 X C 4 S
152 149 150 151 syl2anc φ X 2 + M + B 2 2 M 2 X C 4 S 2 = X 2 + M + B 2 + M 2 X C 4 S X 2 + M + B 2 - M 2 X C 4 S
153 148 152 eqtr3d φ X 4 + B X 2 + C X + D = X 2 + M + B 2 + M 2 X C 4 S X 2 + M + B 2 - M 2 X C 4 S
154 153 eqeq1d φ X 4 + B X 2 + C X + D = 0 X 2 + M + B 2 + M 2 X C 4 S X 2 + M + B 2 - M 2 X C 4 S = 0
155 149 150 addcld φ X 2 + M + B 2 + M 2 X C 4 S
156 149 150 subcld φ X 2 + M + B 2 - M 2 X C 4 S
157 155 156 mul0ord φ X 2 + M + B 2 + M 2 X C 4 S X 2 + M + B 2 - M 2 X C 4 S = 0 X 2 + M + B 2 + M 2 X C 4 S = 0 X 2 + M + B 2 - M 2 X C 4 S = 0
158 1 2 3 4 5 6 7 8 dquartlem1 φ X 2 + M + B 2 + M 2 X C 4 S = 0 X = - S + I X = - S - I
159 4 negcld φ S
160 sqneg 2 S 2 S 2 = 2 S 2
161 16 160 syl φ 2 S 2 = 2 S 2
162 5 161 eqtr4d φ M = 2 S 2
163 mulneg2 2 S 2 S = 2 S
164 14 4 163 sylancr φ 2 S = 2 S
165 164 oveq1d φ 2 S 2 = 2 S 2
166 162 165 eqtr4d φ M = 2 S 2
167 4 sqcld φ S 2
168 167 negcld φ S 2
169 1 halfcld φ B 2
170 168 169 subcld φ - S 2 - B 2
171 58 4 67 divcld φ C 4 S
172 170 171 negsubd φ S 2 - B 2 + C 4 S = S 2 - B 2 - C 4 S
173 sqneg S S 2 = S 2
174 4 173 syl φ S 2 = S 2
175 174 eqcomd φ S 2 = S 2
176 175 negeqd φ S 2 = S 2
177 176 oveq1d φ - S 2 - B 2 = - S 2 - B 2
178 58 4 67 divneg2d φ C 4 S = C 4 S
179 177 178 oveq12d φ S 2 - B 2 + C 4 S = S 2 - B 2 + C 4 S
180 12 172 179 3eqtr2d φ J 2 = S 2 - B 2 + C 4 S
181 1 2 3 159 166 6 11 180 dquartlem1 φ X 2 + M + B 2 + M 2 X C 4 S = 0 X = - S + J X = - S - J
182 59 4 67 divneg2d φ M 2 X C 4 S = M 2 X C 4 S
183 182 oveq2d φ X 2 + M + B 2 + M 2 X C 4 S = X 2 + M + B 2 + M 2 X C 4 S
184 149 150 negsubd φ X 2 + M + B 2 + M 2 X C 4 S = X 2 + M + B 2 - M 2 X C 4 S
185 183 184 eqtr3d φ X 2 + M + B 2 + M 2 X C 4 S = X 2 + M + B 2 - M 2 X C 4 S
186 185 eqeq1d φ X 2 + M + B 2 + M 2 X C 4 S = 0 X 2 + M + B 2 - M 2 X C 4 S = 0
187 4 negnegd φ S = S
188 187 oveq1d φ - S + J = S + J
189 188 eqeq2d φ X = - S + J X = S + J
190 187 oveq1d φ - S - J = S J
191 190 eqeq2d φ X = - S - J X = S J
192 189 191 orbi12d φ X = - S + J X = - S - J X = S + J X = S J
193 181 186 192 3bitr3d φ X 2 + M + B 2 - M 2 X C 4 S = 0 X = S + J X = S J
194 158 193 orbi12d φ X 2 + M + B 2 + M 2 X C 4 S = 0 X 2 + M + B 2 - M 2 X C 4 S = 0 X = - S + I X = - S - I X = S + J X = S J
195 154 157 194 3bitrd φ X 4 + B X 2 + C X + D = 0 X = - S + I X = - S - I X = S + J X = S J