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	|- ( ph -> B e. CC )
	dquart.c	|- ( ph -> C e. CC )
	dquart.x	|- ( ph -> X e. CC )
	dquart.s	|- ( ph -> S e. CC )
	dquart.m	|- ( ph -> M = ( ( 2 x. S ) ^ 2 ) )
	dquart.m0	|- ( ph -> M =/= 0 )
	dquart.i	|- ( ph -> I e. CC )
	dquart.i2	|- ( ph -> ( I ^ 2 ) = ( ( -u ( S ^ 2 ) - ( B / 2 ) ) + ( ( C / 4 ) / S ) ) )
	dquart.d	|- ( ph -> D e. CC )
	dquart.3	|- ( ph -> ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) + -u ( C ^ 2 ) ) ) = 0 )
	dquart.j	|- ( ph -> J e. CC )
	dquart.j2	|- ( ph -> ( J ^ 2 ) = ( ( -u ( S ^ 2 ) - ( B / 2 ) ) - ( ( C / 4 ) / S ) ) )
Assertion	dquart	|- ( ph -> ( ( ( ( X ^ 4 ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) = 0 <-> ( ( X = ( -u S + I ) \/ X = ( -u S - I ) ) \/ ( X = ( S + J ) \/ X = ( S - J ) ) ) ) )

Proof

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