quartfull

Description: The quartic equation, written out in full. This actually makes a fairly good Metamath stress test. Note that the length of this formula could be shortened significantly if the intermediate expressions were expanded and simplified, but it's not like this theorem will be used anyway. (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	quartfull.a	$⊢ φ \to A \in ℂ$
	quartfull.b	$⊢ φ \to B \in ℂ$
	quartfull.c	$⊢ φ \to C \in ℂ$
	quartfull.d	$⊢ φ \to D \in ℂ$
	quartfull.x	$⊢ φ \to X \in ℂ$
	quartfull.t0	$⊢ φ \to {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} \neq 0$
	quartfull.m0	$⊢ φ \to - \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3} \neq 0$
Assertion	quartfull	$⊢ φ \to (X^{4} + A X^{3} + B X^{2} + (C X + D) = 0 \leftrightarrow ((X = (- \frac{A}{4}) - (\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}) + \sqrt{(- {(\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2})}^{2}) - (\frac{B - (\frac{3}{8}) A^{2}}{2}) + (\frac{\frac{C - (\frac{A B}{2}) + (\frac{A^{3}}{8})}{4}}{\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}})} \lor X = (- \frac{A}{4}) - (\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}) - \sqrt{(- {(\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2})}^{2}) - (\frac{B - (\frac{3}{8}) A^{2}}{2}) + (\frac{\frac{C - (\frac{A B}{2}) + (\frac{A^{3}}{8})}{4}}{\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}})}) \lor (X = (- \frac{A}{4}) + (\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}) + \sqrt{(- {(\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2})}^{2}) - (\frac{B - (\frac{3}{8}) A^{2}}{2}) - (\frac{\frac{C - (\frac{A B}{2}) + (\frac{A^{3}}{8})}{4}}{\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}})} \lor X = (- \frac{A}{4}) + (\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}) - \sqrt{(- {(\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2})}^{2}) - (\frac{B - (\frac{3}{8}) A^{2}}{2}) - (\frac{\frac{C - (\frac{A B}{2}) + (\frac{A^{3}}{8})}{4}}{\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}})})))$

Proof

Step	Hyp	Ref	Expression
1		quartfull.a	$⊢ φ \to A \in ℂ$
2		quartfull.b	$⊢ φ \to B \in ℂ$
3		quartfull.c	$⊢ φ \to C \in ℂ$
4		quartfull.d	$⊢ φ \to D \in ℂ$
5		quartfull.x	$⊢ φ \to X \in ℂ$
6		quartfull.t0	$⊢ φ \to {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} \neq 0$
7		quartfull.m0	$⊢ φ \to - \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3} \neq 0$
8		eqidd	$⊢ φ \to - \frac{A}{4} = - \frac{A}{4}$
9		eqidd	$⊢ φ \to B - (\frac{3}{8}) A^{2} = B - (\frac{3}{8}) A^{2}$
10		eqidd	$⊢ φ \to C - (\frac{A B}{2}) + (\frac{A^{3}}{8}) = C - (\frac{A B}{2}) + (\frac{A^{3}}{8})$
11		eqidd	$⊢ φ \to (D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4} = (D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}$
12		eqidd	$⊢ φ \to {(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) = {(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})$
13		eqidd	$⊢ φ \to (- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) = (- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})$
14		eqidd	$⊢ φ \to \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}} = \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}$
15		eqidd	$⊢ φ \to \frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2} = \frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}$
16		eqidd	$⊢ φ \to - \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3} = - \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}$
17		eqidd	$⊢ φ \to {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} = {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}$
18		eqidd	$⊢ φ \to \sqrt{(- {(\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2})}^{2}) - (\frac{B - (\frac{3}{8}) A^{2}}{2}) + (\frac{\frac{C - (\frac{A B}{2}) + (\frac{A^{3}}{8})}{4}}{\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}})} = \sqrt{(- {(\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2})}^{2}) - (\frac{B - (\frac{3}{8}) A^{2}}{2}) + (\frac{\frac{C - (\frac{A B}{2}) + (\frac{A^{3}}{8})}{4}}{\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}})}$
19		eqidd	$⊢ φ \to \sqrt{(- {(\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2})}^{2}) - (\frac{B - (\frac{3}{8}) A^{2}}{2}) - (\frac{\frac{C - (\frac{A B}{2}) + (\frac{A^{3}}{8})}{4}}{\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}})} = \sqrt{(- {(\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2})}^{2}) - (\frac{B - (\frac{3}{8}) A^{2}}{2}) - (\frac{\frac{C - (\frac{A B}{2}) + (\frac{A^{3}}{8})}{4}}{\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}})}$
20	1 2 3 4 5 8 9 10 11 12 13 14 15 16 17 6 7 18 19	quart	$⊢ φ \to (X^{4} + A X^{3} + B X^{2} + (C X + D) = 0 \leftrightarrow ((X = (- \frac{A}{4}) - (\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}) + \sqrt{(- {(\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2})}^{2}) - (\frac{B - (\frac{3}{8}) A^{2}}{2}) + (\frac{\frac{C - (\frac{A B}{2}) + (\frac{A^{3}}{8})}{4}}{\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}})} \lor X = (- \frac{A}{4}) - (\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}) - \sqrt{(- {(\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2})}^{2}) - (\frac{B - (\frac{3}{8}) A^{2}}{2}) + (\frac{\frac{C - (\frac{A B}{2}) + (\frac{A^{3}}{8})}{4}}{\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}})}) \lor (X = (- \frac{A}{4}) + (\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}) + \sqrt{(- {(\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2})}^{2}) - (\frac{B - (\frac{3}{8}) A^{2}}{2}) - (\frac{\frac{C - (\frac{A B}{2}) + (\frac{A^{3}}{8})}{4}}{\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}})} \lor X = (- \frac{A}{4}) + (\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}) - \sqrt{(- {(\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2})}^{2}) - (\frac{B - (\frac{3}{8}) A^{2}}{2}) - (\frac{\frac{C - (\frac{A B}{2}) + (\frac{A^{3}}{8})}{4}}{\frac{\sqrt{- \frac{2 (B - (\frac{3}{8}) A^{2}) + {(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}} + (\frac{{(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4})}{{(\frac{(- 2 {(B - (\frac{3}{8}) A^{2})}^{3} - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2}) + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}) + \sqrt{{((- 2 {(B - (\frac{3}{8}) A^{2})}^{3}) - 27 {(C - (\frac{A B}{2}) + (\frac{A^{3}}{8}))}^{2} + 72 (B - (\frac{3}{8}) A^{2}) ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{2} - 4 {({(B - (\frac{3}{8}) A^{2})}^{2} + 12 ((D - (\frac{C A}{4})) + (\frac{A^{2} B}{16}) - (\frac{3}{256}) A^{4}))}^{3}}}{2})}^{\frac{1}{3}}})}{3}}}{2}})})))$

Metamath Proof Explorer

Theorem quartfull

Proof