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	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	dquart.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	dquart.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	dquart.s	⊢ ( 𝜑 → 𝑆 ∈ ℂ )
	dquart.m	⊢ ( 𝜑 → 𝑀 = ( ( 2 · 𝑆 ) ↑ 2 ) )
	dquart.m0	⊢ ( 𝜑 → 𝑀 ≠ 0 )
	dquart.i	⊢ ( 𝜑 → 𝐼 ∈ ℂ )
	dquart.i2	⊢ ( 𝜑 → ( 𝐼 ↑ 2 ) = ( ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) + ( ( 𝐶 / 4 ) / 𝑆 ) ) )
	dquart.d	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
	dquart.3	⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝐵 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( ( 𝐵 ↑ 2 ) − ( 4 · 𝐷 ) ) · 𝑀 ) + - ( 𝐶 ↑ 2 ) ) ) = 0 )
	dquart.j	⊢ ( 𝜑 → 𝐽 ∈ ℂ )
	dquart.j2	⊢ ( 𝜑 → ( 𝐽 ↑ 2 ) = ( ( - ( 𝑆 ↑ 2 ) − ( 𝐵 / 2 ) ) − ( ( 𝐶 / 4 ) / 𝑆 ) ) )
Assertion	dquart	⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 4 ) + ( 𝐵 · ( 𝑋 ↑ 2 ) ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) = 0 ↔ ( ( 𝑋 = ( - 𝑆 + 𝐼 ) ∨ 𝑋 = ( - 𝑆 − 𝐼 ) ) ∨ ( 𝑋 = ( 𝑆 + 𝐽 ) ∨ 𝑋 = ( 𝑆 − 𝐽 ) ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem dquart

Proof