# Metamath Proof Explorer

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

### Proof

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