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	$⊢ φ \to A \in ℂ$
	quart.b	$⊢ φ \to B \in ℂ$
	quart.c	$⊢ φ \to C \in ℂ$
	quart.d	$⊢ φ \to D \in ℂ$
	quart.x	$⊢ φ \to X \in ℂ$
	quart.e	$⊢ φ \to E = - \frac{A}{4}$
	quart.p	$⊢ φ \to P = B - (\frac{3}{8}) A^{2}$
	quart.q	$⊢ φ \to Q = C - (\frac{A B}{2}) + (\frac{A^{3}}{8})$
	quart.r	$⊢ φ \to R = (D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}$
	quart.u	$⊢ φ \to U = P^{2} + 12 R$
	quart.v	$⊢ φ \to V = (- 2 P^{3}) - 27 Q^{2} + 72 P R$
	quart.w	$⊢ φ \to W = \sqrt{V^{2} - 4 U^{3}}$
	quart.s	$⊢ φ \to S = \frac{\sqrt{M}}{2}$
	quart.m	$⊢ φ \to M = - \frac{2 P + T + (\frac{U}{T})}{3}$
	quart.t	$⊢ φ \to T = {(\frac{V + W}{2})}^{\frac{1}{3}}$
	quart.t0	$⊢ φ \to T \neq 0$
	quart.m0	$⊢ φ \to M \neq 0$
	quart.i	$⊢ φ \to I = \sqrt{(- S^{2}) - (\frac{P}{2}) + (\frac{\frac{Q}{4}}{S})}$
	quart.j	$⊢ φ \to J = \sqrt{(- S^{2}) - (\frac{P}{2}) - (\frac{\frac{Q}{4}}{S})}$
Assertion	quart	$⊢ φ \to (X^{4} + A X^{3} + B X^{2} + (C X + D) = 0 \leftrightarrow ((X = E - S + I \lor X = E - S - I) \lor (X = E + S + J \lor X = E + S - J)))$

Proof

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

Metamath Proof Explorer

Theorem quart

Proof