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	$⊢ φ \to B \in ℂ$
	dquart.c	$⊢ φ \to C \in ℂ$
	dquart.x	$⊢ φ \to X \in ℂ$
	dquart.s	$⊢ φ \to S \in ℂ$
	dquart.m	$⊢ φ \to M = {2 S}^{2}$
	dquart.m0	$⊢ φ \to M \neq 0$
	dquart.i	$⊢ φ \to I \in ℂ$
	dquart.i2	$⊢ φ \to I^{2} = (- S^{2}) - (\frac{B}{2}) + (\frac{\frac{C}{4}}{S})$
	dquart.d	$⊢ φ \to D \in ℂ$
	dquart.3	$⊢ φ \to M^{3} + 2 B M^{2} + (B^{2} - 4 D) \cdot M + (- C^{2}) = 0$
	dquart.j	$⊢ φ \to J \in ℂ$
	dquart.j2	$⊢ φ \to J^{2} = (- S^{2}) - (\frac{B}{2}) - (\frac{\frac{C}{4}}{S})$
Assertion	dquart	$⊢ φ \to (X^{4} + B X^{2} + C X + D = 0 \leftrightarrow ((X = - S + I \lor X = - S - I) \lor (X = S + J \lor X = S - J)))$

Proof

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

Metamath Proof Explorer

Theorem dquart

Proof