Metamath Proof Explorer


Theorem cubic2

Description: The solution to the general cubic equation, for arbitrary choices G and T of the square and cube roots. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses cubic2.a φ A
cubic2.z φ A 0
cubic2.b φ B
cubic2.c φ C
cubic2.d φ D
cubic2.x φ X
cubic2.t φ T
cubic2.3 φ T 3 = N + G 2
cubic2.g φ G
cubic2.2 φ G 2 = N 2 4 M 3
cubic2.m φ M = B 2 3 A C
cubic2.n φ N = 2 B 3 - 9 A B C + 27 A 2 D
cubic2.0 φ T 0
Assertion cubic2 φ A X 3 + B X 2 + C X + D = 0 r r 3 = 1 X = B + r T + M r T 3 A

Proof

Step Hyp Ref Expression
1 cubic2.a φ A
2 cubic2.z φ A 0
3 cubic2.b φ B
4 cubic2.c φ C
5 cubic2.d φ D
6 cubic2.x φ X
7 cubic2.t φ T
8 cubic2.3 φ T 3 = N + G 2
9 cubic2.g φ G
10 cubic2.2 φ G 2 = N 2 4 M 3
11 cubic2.m φ M = B 2 3 A C
12 cubic2.n φ N = 2 B 3 - 9 A B C + 27 A 2 D
13 cubic2.0 φ T 0
14 3nn0 3 0
15 expcl X 3 0 X 3
16 6 14 15 sylancl φ X 3
17 1 16 mulcld φ A X 3
18 6 sqcld φ X 2
19 3 18 mulcld φ B X 2
20 17 19 addcld φ A X 3 + B X 2
21 4 6 mulcld φ C X
22 21 5 addcld φ C X + D
23 20 22 addcld φ A X 3 + B X 2 + C X + D
24 23 1 2 diveq0ad φ A X 3 + B X 2 + C X + D A = 0 A X 3 + B X 2 + C X + D = 0
25 20 22 1 2 divdird φ A X 3 + B X 2 + C X + D A = A X 3 + B X 2 A + C X + D A
26 17 19 1 2 divdird φ A X 3 + B X 2 A = A X 3 A + B X 2 A
27 16 1 2 divcan3d φ A X 3 A = X 3
28 3 18 1 2 div23d φ B X 2 A = B A X 2
29 27 28 oveq12d φ A X 3 A + B X 2 A = X 3 + B A X 2
30 26 29 eqtrd φ A X 3 + B X 2 A = X 3 + B A X 2
31 21 5 1 2 divdird φ C X + D A = C X A + D A
32 4 6 1 2 div23d φ C X A = C A X
33 32 oveq1d φ C X A + D A = C A X + D A
34 31 33 eqtrd φ C X + D A = C A X + D A
35 30 34 oveq12d φ A X 3 + B X 2 A + C X + D A = X 3 + B A X 2 + C A X + D A
36 25 35 eqtrd φ A X 3 + B X 2 + C X + D A = X 3 + B A X 2 + C A X + D A
37 36 eqeq1d φ A X 3 + B X 2 + C X + D A = 0 X 3 + B A X 2 + C A X + D A = 0
38 24 37 bitr3d φ A X 3 + B X 2 + C X + D = 0 X 3 + B A X 2 + C A X + D A = 0
39 3 1 2 divcld φ B A
40 4 1 2 divcld φ C A
41 5 1 2 divcld φ D A
42 7 1 2 divcld φ T A
43 14 a1i φ 3 0
44 7 1 2 43 expdivd φ T A 3 = T 3 A 3
45 8 oveq1d φ T 3 A 3 = N + G 2 A 3
46 2cn 2
47 expcl B 3 0 B 3
48 3 14 47 sylancl φ B 3
49 mulcl 2 B 3 2 B 3
50 46 48 49 sylancr φ 2 B 3
51 9cn 9
52 mulcl 9 A 9 A
53 51 1 52 sylancr φ 9 A
54 3 4 mulcld φ B C
55 53 54 mulcld φ 9 A B C
56 50 55 subcld φ 2 B 3 9 A B C
57 2nn0 2 0
58 7nn 7
59 57 58 decnncl 27
60 59 nncni 27
61 1 sqcld φ A 2
62 61 5 mulcld φ A 2 D
63 mulcl 27 A 2 D 27 A 2 D
64 60 62 63 sylancr φ 27 A 2 D
65 56 64 addcld φ 2 B 3 - 9 A B C + 27 A 2 D
66 12 65 eqeltrd φ N
67 66 9 addcld φ N + G
68 2cnd φ 2
69 expcl A 3 0 A 3
70 1 14 69 sylancl φ A 3
71 2ne0 2 0
72 71 a1i φ 2 0
73 3z 3
74 73 a1i φ 3
75 1 2 74 expne0d φ A 3 0
76 67 68 70 72 75 divdiv32d φ N + G 2 A 3 = N + G A 3 2
77 66 9 70 75 divdird φ N + G A 3 = N A 3 + G A 3
78 77 oveq1d φ N + G A 3 2 = N A 3 + G A 3 2
79 76 78 eqtrd φ N + G 2 A 3 = N A 3 + G A 3 2
80 44 45 79 3eqtrd φ T A 3 = N A 3 + G A 3 2
81 9 70 75 divcld φ G A 3
82 9 70 75 sqdivd φ G A 3 2 = G 2 A 3 2
83 10 oveq1d φ G 2 A 3 2 = N 2 4 M 3 A 3 2
84 66 sqcld φ N 2
85 4cn 4
86 3 sqcld φ B 2
87 3cn 3
88 1 4 mulcld φ A C
89 mulcl 3 A C 3 A C
90 87 88 89 sylancr φ 3 A C
91 86 90 subcld φ B 2 3 A C
92 11 91 eqeltrd φ M
93 expcl M 3 0 M 3
94 92 14 93 sylancl φ M 3
95 mulcl 4 M 3 4 M 3
96 85 94 95 sylancr φ 4 M 3
97 70 sqcld φ A 3 2
98 sqne0 A 3 A 3 2 0 A 3 0
99 70 98 syl φ A 3 2 0 A 3 0
100 75 99 mpbird φ A 3 2 0
101 84 96 97 100 divsubdird φ N 2 4 M 3 A 3 2 = N 2 A 3 2 4 M 3 A 3 2
102 66 70 75 sqdivd φ N A 3 2 = N 2 A 3 2
103 2z 2
104 103 a1i φ 2
105 1 2 104 expne0d φ A 2 0
106 92 61 105 43 expdivd φ M A 2 3 = M 3 A 2 3
107 46 87 mulcomi 2 3 = 3 2
108 107 oveq2i A 2 3 = A 3 2
109 57 a1i φ 2 0
110 1 43 109 expmuld φ A 2 3 = A 2 3
111 1 109 43 expmuld φ A 3 2 = A 3 2
112 108 110 111 3eqtr3a φ A 2 3 = A 3 2
113 112 oveq2d φ M 3 A 2 3 = M 3 A 3 2
114 106 113 eqtrd φ M A 2 3 = M 3 A 3 2
115 114 oveq2d φ 4 M A 2 3 = 4 M 3 A 3 2
116 85 a1i φ 4
117 116 94 97 100 divassd φ 4 M 3 A 3 2 = 4 M 3 A 3 2
118 115 117 eqtr4d φ 4 M A 2 3 = 4 M 3 A 3 2
119 102 118 oveq12d φ N A 3 2 4 M A 2 3 = N 2 A 3 2 4 M 3 A 3 2
120 101 119 eqtr4d φ N 2 4 M 3 A 3 2 = N A 3 2 4 M A 2 3
121 82 83 120 3eqtrd φ G A 3 2 = N A 3 2 4 M A 2 3
122 86 90 61 105 divsubdird φ B 2 3 A C A 2 = B 2 A 2 3 A C A 2
123 11 oveq1d φ M A 2 = B 2 3 A C A 2
124 3 1 2 sqdivd φ B A 2 = B 2 A 2
125 1 sqvald φ A 2 = A A
126 125 oveq2d φ A C A 2 = A C A A
127 4 1 1 2 2 divcan5d φ A C A A = C A
128 126 127 eqtr2d φ C A = A C A 2
129 128 oveq2d φ 3 C A = 3 A C A 2
130 87 a1i φ 3
131 130 88 61 105 divassd φ 3 A C A 2 = 3 A C A 2
132 129 131 eqtr4d φ 3 C A = 3 A C A 2
133 124 132 oveq12d φ B A 2 3 C A = B 2 A 2 3 A C A 2
134 122 123 133 3eqtr4d φ M A 2 = B A 2 3 C A
135 56 64 70 75 divdird φ 2 B 3 - 9 A B C + 27 A 2 D A 3 = 2 B 3 9 A B C A 3 + 27 A 2 D A 3
136 12 oveq1d φ N A 3 = 2 B 3 - 9 A B C + 27 A 2 D A 3
137 3 1 2 43 expdivd φ B A 3 = B 3 A 3
138 137 oveq2d φ 2 B A 3 = 2 B 3 A 3
139 68 48 70 75 divassd φ 2 B 3 A 3 = 2 B 3 A 3
140 138 139 eqtr4d φ 2 B A 3 = 2 B 3 A 3
141 51 a1i φ 9
142 1 54 mulcld φ A B C
143 141 142 70 75 divassd φ 9 A B C A 3 = 9 A B C A 3
144 141 1 54 mulassd φ 9 A B C = 9 A B C
145 144 oveq1d φ 9 A B C A 3 = 9 A B C A 3
146 54 61 1 105 2 divcan5d φ A B C A A 2 = B C A 2
147 df-3 3 = 2 + 1
148 147 oveq2i A 3 = A 2 + 1
149 expp1 A 2 0 A 2 + 1 = A 2 A
150 1 57 149 sylancl φ A 2 + 1 = A 2 A
151 148 150 syl5eq φ A 3 = A 2 A
152 61 1 mulcomd φ A 2 A = A A 2
153 151 152 eqtrd φ A 3 = A A 2
154 153 oveq2d φ A B C A 3 = A B C A A 2
155 3 1 4 1 2 2 divmuldivd φ B A C A = B C A A
156 125 oveq2d φ B C A 2 = B C A A
157 155 156 eqtr4d φ B A C A = B C A 2
158 146 154 157 3eqtr4rd φ B A C A = A B C A 3
159 158 oveq2d φ 9 B A C A = 9 A B C A 3
160 143 145 159 3eqtr4rd φ 9 B A C A = 9 A B C A 3
161 140 160 oveq12d φ 2 B A 3 9 B A C A = 2 B 3 A 3 9 A B C A 3
162 50 55 70 75 divsubdird φ 2 B 3 9 A B C A 3 = 2 B 3 A 3 9 A B C A 3
163 161 162 eqtr4d φ 2 B A 3 9 B A C A = 2 B 3 9 A B C A 3
164 151 oveq2d φ A 2 D A 3 = A 2 D A 2 A
165 5 1 61 2 105 divcan5d φ A 2 D A 2 A = D A
166 164 165 eqtr2d φ D A = A 2 D A 3
167 166 oveq2d φ 27 D A = 27 A 2 D A 3
168 60 a1i φ 27
169 168 62 70 75 divassd φ 27 A 2 D A 3 = 27 A 2 D A 3
170 167 169 eqtr4d φ 27 D A = 27 A 2 D A 3
171 163 170 oveq12d φ 2 B A 3 - 9 B A C A + 27 D A = 2 B 3 9 A B C A 3 + 27 A 2 D A 3
172 135 136 171 3eqtr4d φ N A 3 = 2 B A 3 - 9 B A C A + 27 D A
173 7 1 13 2 divne0d φ T A 0
174 39 40 41 6 42 80 81 121 134 172 173 mcubic φ X 3 + B A X 2 + C A X + D A = 0 r r 3 = 1 X = B A + r T A + M A 2 r T A 3
175 oveq1 r = 0 r 3 = 0 3
176 3nn 3
177 0exp 3 0 3 = 0
178 176 177 ax-mp 0 3 = 0
179 175 178 eqtrdi r = 0 r 3 = 0
180 0ne1 0 1
181 180 a1i r = 0 0 1
182 179 181 eqnetrd r = 0 r 3 1
183 182 necon2i r 3 = 1 r 0
184 simprl φ r r 0 r
185 7 adantr φ r r 0 T
186 1 adantr φ r r 0 A
187 2 adantr φ r r 0 A 0
188 184 185 186 187 divassd φ r r 0 r T A = r T A
189 188 eqcomd φ r r 0 r T A = r T A
190 189 oveq2d φ r r 0 B A + r T A = B A + r T A
191 3 adantr φ r r 0 B
192 184 185 mulcld φ r r 0 r T
193 191 192 186 187 divdird φ r r 0 B + r T A = B A + r T A
194 190 193 eqtr4d φ r r 0 B A + r T A = B + r T A
195 92 adantr φ r r 0 M
196 195 186 187 divcld φ r r 0 M A
197 simprr φ r r 0 r 0
198 13 adantr φ r r 0 T 0
199 184 185 197 198 mulne0d φ r r 0 r T 0
200 196 192 186 199 187 divcan7d φ r r 0 M A A r T A = M A r T
201 195 186 186 187 187 divdiv1d φ r r 0 M A A = M A A
202 186 sqvald φ r r 0 A 2 = A A
203 202 oveq2d φ r r 0 M A 2 = M A A
204 201 203 eqtr4d φ r r 0 M A A = M A 2
205 204 188 oveq12d φ r r 0 M A A r T A = M A 2 r T A
206 195 186 192 187 199 divdiv32d φ r r 0 M A r T = M r T A
207 200 205 206 3eqtr3d φ r r 0 M A 2 r T A = M r T A
208 194 207 oveq12d φ r r 0 B A + r T A + M A 2 r T A = B + r T A + M r T A
209 191 192 addcld φ r r 0 B + r T
210 195 192 199 divcld φ r r 0 M r T
211 209 210 186 187 divdird φ r r 0 B + r T + M r T A = B + r T A + M r T A
212 208 211 eqtr4d φ r r 0 B A + r T A + M A 2 r T A = B + r T + M r T A
213 212 oveq1d φ r r 0 B A + r T A + M A 2 r T A 3 = B + r T + M r T A 3
214 209 210 addcld φ r r 0 B + r T + M r T
215 87 a1i φ r r 0 3
216 3ne0 3 0
217 216 a1i φ r r 0 3 0
218 214 186 215 187 217 divdiv1d φ r r 0 B + r T + M r T A 3 = B + r T + M r T A 3
219 mulcom A 3 A 3 = 3 A
220 186 87 219 sylancl φ r r 0 A 3 = 3 A
221 220 oveq2d φ r r 0 B + r T + M r T A 3 = B + r T + M r T 3 A
222 213 218 221 3eqtrd φ r r 0 B A + r T A + M A 2 r T A 3 = B + r T + M r T 3 A
223 222 negeqd φ r r 0 B A + r T A + M A 2 r T A 3 = B + r T + M r T 3 A
224 223 eqeq2d φ r r 0 X = B A + r T A + M A 2 r T A 3 X = B + r T + M r T 3 A
225 224 anassrs φ r r 0 X = B A + r T A + M A 2 r T A 3 X = B + r T + M r T 3 A
226 183 225 sylan2 φ r r 3 = 1 X = B A + r T A + M A 2 r T A 3 X = B + r T + M r T 3 A
227 226 pm5.32da φ r r 3 = 1 X = B A + r T A + M A 2 r T A 3 r 3 = 1 X = B + r T + M r T 3 A
228 227 rexbidva φ r r 3 = 1 X = B A + r T A + M A 2 r T A 3 r r 3 = 1 X = B + r T + M r T 3 A
229 38 174 228 3bitrd φ A X 3 + B X 2 + C X + D = 0 r r 3 = 1 X = B + r T + M r T 3 A