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