:: Solution of Cubic and Quartic Equations
:: by Marco Riccardi
::
:: Received March 3, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XCMPLX_0, RELAT_1, NEWTON, ARYTM_3, ARYTM_1, SQUARE_1,
POWER, COMPLEX1, SIN_COS, COMPTRIG, SUBSET_1, CARD_1, XXREAL_0, REAL_1,
FUNCT_3, PREPOWER, POLYEQ_5, NAT_1;
notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1,
COMPLEX1, SQUARE_1, NEWTON, QUIN_1, POWER, SIN_COS, PREPOWER, COMPTRIG;
constructors REAL_1, SQUARE_1, NAT_1, QUIN_1, PREPOWER, POWER, POLYEQ_1,
SIN_COS, COMPTRIG, NAT_D, XREAL_0, POLYEQ_3, NUMBERS, XCMPLX_0, XXREAL_0,
ABIAN, NEWTON, BINOP_2;
registrations ORDINAL1, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, NEWTON,
SIN_COS, QUIN_1, CARD_1;
requirements ARITHM, SUBSET, REAL, NUMERALS;
equalities SQUARE_1, QUIN_1;
theorems XCMPLX_1, NEWTON, COMPTRIG, COMPLEX1, POLYEQ_3, ORDINAL1, SIN_COS,
COMPLEX2, POWER, NAT_1, PREPOWER;
begin :: Preliminaries
reserve a,b for Complex;
theorem Th1:
a*a = a|^2
proof
thus a*a = a|^1*a
.= a|^(1+1) by NEWTON:6
.= a|^2;
end;
theorem Th2:
a*a*a = a|^3
proof
thus a*a*a = a|^2*a by Th1
.= a|^(2+1) by NEWTON:6
.= a|^3;
end;
theorem Th3:
a*a*a*a = a|^4
proof
thus a*a*a*a = a|^3*a by Th2
.= a|^(3+1) by NEWTON:6
.= a|^4;
end;
theorem Th4:
(a - b)|^2 = a|^2 -2*a*b +b|^2
proof
thus (a - b)|^2 = (a - b)*(a - b) by Th1
.= a^2 - 2*a*b + b^2
.= a|^2 -2*a*b +b*b by Th1
.= a|^2 -2*a*b +b|^2 by Th1;
end;
:: like SERIES_4:5
theorem Th5:
(a - b)|^3 = a|^3 -3*a|^2*b +3*b|^2*a -b|^3
proof
(a-b)|^(2+1)=((a-b)|^2)*(a-b) by NEWTON:6
.=(a|^2-2*a*b+b|^2)*(a-b) by Th4
.=a|^2*a-a|^2*b-(2*a*b*a-2*a*b*b)+(b|^2*a-b|^2*b)
.=a|^2*a-a|^2*b-(2*a*b*a-2*a*b*b)+(b|^2*a-b|^(2+1)) by NEWTON:6
.=a|^3-a|^2*b-(2*(a*a)*b-2*a*b*b)+(b|^2*a-b|^3) by NEWTON:6
.=a|^3-a|^2*b-(2*(a|^1*a)*b-2*a*b*b)+(b|^2*a-b|^3)
.=a|^3-a|^2*b-(2*(a|^(1+1))*b-2*a*b*b)+(b|^2*a-b|^3) by NEWTON:6
.=a|^3-3*a|^2*b+2*(b*b)*a+b|^2*a-b|^3
.=a|^3-3*a|^2*b+2*(b|^1*b)*a+b|^2*a-b|^3
.=a|^3-3*a|^2*b+2*b|^(1+1)*a+b|^2*a-b|^3 by NEWTON:6
.=a|^3-3*a|^2*b+3*b|^2*a-b|^3;
hence thesis;
end;
theorem Th6:
(a - b)|^4 = a|^4 -4*a|^3*b +6*a|^2*b|^2 -4*b|^3*a +b|^4
proof
(a-b)|^(3+1)=((a-b)|^3)*(a-b) by NEWTON:6
.=(a|^3-3*a|^2*b+3*b|^2*a-b|^3)*(a-b) by Th5
.=a|^3*a-a|^3*b+(-3*a|^2*b*a+3*a|^2*b*b)+(3*b|^2*a*a-3*b|^2*a*b)+ (-b|^3
*a+b|^3*b)
.=a|^3*a-a|^3*b+(-3*a|^2*b*a+3*a|^2*b*b)+(3*b|^2*a*a-3*b|^2*a*b)+ (-b|^3
*a+b|^(3+1)) by NEWTON:6
.=a|^4-a|^3*b+(-3*(a|^2*a)*b+3*a|^2*b*b)+(3*b|^2*a*a-3*b|^2*a*b)+ (-b|^3
*a+b|^4) by NEWTON:6
.=a|^4-a|^3*b+(-3*(a|^(2+1))*b+3*a|^2*b*b)+(3*b|^2*a*a-3*b|^2*a*b)+ (-b
|^3*a+b|^4) by NEWTON:6
.=a|^4-a|^3*b+(-3*a|^3*b+3*a|^2*(b*b))+(3*b|^2*a*a-3*b|^2*a*b)+ (-b|^3*a
+b|^4)
.=a|^4-a|^3*b+(-3*a|^3*b+3*a|^2*(b|^1*b))+(3*b|^2*a*a-3*b|^2*a*b)+ (-b|^
3*a+b|^4)
.=a|^4-a|^3*b+(-3*a|^3*b+3*a|^2*(b|^(1+1)))+(3*b|^2*a*a-3*b|^2*a*b)+ (-b
|^3*a+b|^4) by NEWTON:6
.=a|^4-a|^3*b+(-3*a|^3*b+3*a|^2*b|^2)+(3*b|^2*(a*a)-3*b|^2*a*b)+ (-b|^3*
a+b|^4)
.=a|^4-a|^3*b+(-3*a|^3*b+3*a|^2*b|^2)+(3*b|^2*(a|^1*a)-3*b|^2*b*a)+ (-b
|^3*a+b|^4)
.=a|^4-a|^3*b+(-3*a|^3*b+3*a|^2*b|^2)+(3*b|^2*a|^(1+1)-3*(b|^2*b)*a)+ (-
b|^3*a+b|^4) by NEWTON:6
.=a|^4-a|^3*b+(-3*a|^3*b+3*a|^2*b|^2)+(3*b|^2*a|^2-3*(b|^(2+1))*a)+ (-b
|^3*a+b|^4) by NEWTON:6
.=a|^4-4*a|^3*b+6*a|^2*b|^2-4*b|^3*a+b|^4;
hence thesis;
end;
notation
let n be Nat;
let r be Real;
synonym n -real-root r for n -root r;
end;
:: principal root
definition
let n be non zero Nat;
let z be Complex;
func n -root z -> Complex equals
(n -real-root |.z.|)*(cos((Arg z)/n)
+ sin((Arg z)/n)*<i>);
correctness;
end;
reserve z for Complex;
reserve n0 for non zero Nat;
theorem Th7:
(n0-root z)|^n0 = z
proof
reconsider n=n0 as Element of NAT by ORDINAL1:def 12;
thus (n0-root z)|^n0 = ((n-real-root |.z.|)*cos((Arg z+2*PI*0)/n) + (n
-real-root |.z.|)*sin((Arg z+2*PI*0)/n)*<i>)|^n
.= z by POLYEQ_3:34;
end;
theorem Th8:
for r being Real st r >= 0 holds n0-root r = n0-real-root r
proof
let r be Real;
reconsider r9=r as Real;
assume
A1: r >= 0;
then Arg r9 = 0 by COMPTRIG:35;
hence thesis by A1,COMPLEX1:43,SIN_COS:31;
end;
theorem Th9:
for r being Real st r > 0 holds n0-root(z/r) = n0-root z/ n0-root r
proof
let r be Real;
reconsider r9=1/r as Real;
reconsider n=n0 as Element of NAT by ORDINAL1:def 12;
A1: n>=0+1 by NAT_1:13;
assume
A2: r > 0;
then
A3: |.r.|>0 by COMPLEX1:47;
z/r = z*(1/r) & Arg(z*r9) = Arg z by A2,COMPLEX2:27,XCMPLX_1:99;
hence
n0-root(z/r) = (n -real-root(|.z.|/|.r.|))*(cos((Arg z)/n) + sin((Arg z
)/n)*<i>) by COMPLEX1:67
.= n -real-root |.z.|/(n -real-root |.r.|)*(cos((Arg z)/n) + sin((Arg z)
/n)*<i>) by A3,A1,COMPLEX1:46,POWER:13
.= (cos((Arg z)/n) + sin((Arg z)/n)*<i>)/ ((n -real-root |.r.|)/(n
-real-root |.z.|)) by XCMPLX_1:79
.= n -real-root |.z.|*(cos((Arg z)/n) + sin((Arg z)/n)*<i>)/(n
-real-root |.r.|) by XCMPLX_1:77
.= n0-root z/(n -real-root r) by A2,COMPLEX1:43
.= n0-root z/n0-root r by A2,Th8;
end;
theorem Th10:
z|^2 = a iff z = 2-root a or z = -2-root a
proof
A1: a = (2-root a)|^2 by Th7
.= (2-root a)*(2-root a) by Th1;
hereby
assume z|^2 = a;
then
A2: z*z = a by Th1;
assume not z = 2-root a;
then
A3: (z - 2-root a) <> 0;
assume not z = -2-root a;
then (z + 2-root a) <> 0;
then (z - 2-root a)*(z + 2-root a) <> 0 by A3;
hence contradiction by A1,A2;
end;
assume z = 2-root a or z = -2-root a;
then z*z - (2-root a)*(2-root a) = 0;
hence z|^2 = a by A1,Th1;
end;
begin :: Solution of Quadratic Equations
reserve a0,a1,a2,s1,s2 for Complex;
theorem Th11:
a1 = -(s1+s2) & a0 = s1*s2 implies (z|^2 + a1*z + a0 = 0 iff z =
s1 or z = s2)
proof
assume a1 = -(s1+s2) & a0 = s1*s2;
then
A1: (z-s1)*(z-s2) = z*z +a1*z +a0 .= z|^2 + a1*z + a0 by Th1;
hereby
assume z|^2 + a1*z + a0 = 0;
then
A2: z-s1 = 0 or z-s2 = 0 by A1;
assume not z = s1;
hence z = s2 by A2;
end;
assume z = s1 or z = s2;
hence z|^2 + a1*z + a0 = 0 by A1;
end;
theorem Th12:
a2<>0 implies (a2*z|^2+a1*z+a0 = 0 iff z = -a1/(2*a2)+2-root(
delta(a0,a1,a2))/(2*a2) or z = -a1/(2*a2)-2-root(delta(a0,a1,a2))/(2*a2))
proof
set s1 = -a1/(2*a2)+2-root(delta(a0,a1,a2))/(2*a2);
set s2 = -a1/(2*a2)-2-root(delta(a0,a1,a2))/(2*a2);
A1: -(s1+s2) = a1/(2*a2)+a1/(2*a2) .= 1/2*(a1/a2)+a1/(2*a2) by XCMPLX_1:103
.= 1/2*(a1/a2)+1/2*(a1/a2) by XCMPLX_1:103
.= a1/a2;
assume
A2: a2<>0;
then a2*z|^2+a1*z+a0 = (a2*z|^2+a1*z+a0)/a2*a2 by XCMPLX_1:87
.= (a2*z|^2/a2+a1*z/a2+a0/a2)*a2 by XCMPLX_1:63
.= (z|^2+a1*z/a2+a0/a2)*a2 by A2,XCMPLX_1:89
.= (z|^2+a1*(z/a2)+a0/a2)*a2 by XCMPLX_1:74
.= (z|^2+z/(a2/a1)+a0/a2)*a2 by XCMPLX_1:81
.= (z|^2+(a1/a2)*z+a0/a2)*a2 by XCMPLX_1:79;
then
A3: a2*z|^2+a1*z+a0 = 0 iff z|^2+(a1/a2)*z+a0/a2 = 0 by A2;
s1*s2 = (a1/(2*a2))*(a1/(2*a2))- (2-root(delta(a0,a1,a2))/(2*a2))* (2
-root(delta(a0,a1,a2))/(2*a2))
.= (a1*a1)/((2*a2)*(2*a2)) - (2-root(delta(a0,a1,a2))/(2*a2))* (2-root(
delta(a0,a1,a2))/(2*a2)) by XCMPLX_1:76
.= (a1*a1)/(4*a2*a2) - ((2-root(delta(a0,a1,a2))* (2-root(delta(a0,a1,a2
)))))/((2*a2)*(2*a2)) by XCMPLX_1:76
.= (a1*a1)/(4*a2*a2) - (2-root(delta(a0,a1,a2))|^2)/ ((2*a2)*(2*a2)) by Th1
.= (a1*a1)/(4*a2*a2) - delta(a0,a1,a2)/((2*a2)*(2*a2)) by Th7
.= (a1*a1 - delta(a0,a1,a2))/(4*a2*a2) by XCMPLX_1:120
.= (a0*(4*a2))/(a2*(4*a2))
.= (a0/a2)*(4*a2/(4*a2)) by XCMPLX_1:76
.= (a0/a2)*1 by A2,XCMPLX_1:60
.= a0/a2;
hence thesis by A3,A1,Th11;
end;
begin :: Solution of Cubic Equations
reserve a3,x,q,r,s,s3 for Complex;
theorem Th13:
z = x - a2/3 & q = (3*a1 - a2|^2)/9 & r = (9*a2*a1 - 2*a2|^3 -
27*a0)/54 implies (z|^3+a2*z|^2+a1*z+a0 = 0 iff x|^3+3*q*x-2*r = 0)
proof
assume
A1: z = x - a2/3;
then
A2: 3*z = 3*x - a2;
A3: (3*x)|^2 = 3|^2*x|^2 by NEWTON:7
.= (3*3)*x|^2 by Th1
.= 9*x|^2;
A4: (3*x)|^3 = (3|^3)*(x|^3) by NEWTON:7
.= (3*3*3)*x|^3 by Th2
.= 27*x|^3;
A5: 27*z|^3 = 3*3*3*z|^3 .= 3|^3*z|^3 by Th2
.= ((3*x) - a2)|^3 by A2,NEWTON:7
.= 27*x|^3-3*(9*x|^2)*a2+3*a2|^2*(3*x)-a2|^3 by A4,A3,Th5
.= 27*x|^3-27*a2*x|^2+9*a2|^2*x-a2|^3;
assume
A6: q = (3*a1 - a2|^2)/9 & r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54;
A7: 27*a1*z = 27*a1*x -9*a2*a1 by A1;
(27*1)*a2*z|^2 = 3*a2*(3*3)*(1*1)*z|^2 .= 3*a2*3|^2*z|^2 by Th1
.= 3*a2*(3|^2*z|^2)
.= 3*a2*(3*z)|^2 by NEWTON:7
.= 3*a2*((3*x)|^2 -2*(3*x)*a2 +a2|^2) by A2,Th4
.= 3*a2*((3*x)*(3*x) -2*(3*x)*a2 +a2|^2) by Th1
.= 27*a2*x*x -2*(3*x)*a2*(3*a2) +a2|^2*(3*a2)
.= 27*a2*(x*x) -18*(a2*a2)*x +3*a2*(a2*a2) by Th1
.= 27*a2*x|^2 -18*(a2*a2)*x +3*a2*a2*a2 by Th1
.= 27*a2*x|^2 -18*a2|^2*x +3*(a2*a2*a2) by Th1
.= 27*a2*x|^2 -18*a2|^2*x +3*a2|^3 by Th2;
then
27*(z|^3+a2*z|^2+a1*z+a0) = (27*x|^3)+(-9*a2|^2+27*a1)*x +(2*a2|^3-9*a2*
a1+27*a0) by A5,A7
.= 27*(x|^3 +3*q*x -2*r) by A6;
hence thesis;
end;
theorem Th14:
a2 = -(s1+s2+s3) & a1 = s1*s2+s1*s3+s2*s3 & a0 = -s1*s2*s3
implies (z|^3 + a2*z|^2 + a1*z + a0 = 0 iff z = s1 or z = s2 or z = s3)
proof
assume a2 = -(s1+s2+s3) & a1 = s1*s2+s1*s3+s2*s3 & a0 = -s1*s2*s3;
then
A1: (z-s1)*(z-s2)*(z-s3) = z*z*z + a2*z*z +a1*z +a0
.= z|^3 + a2*(z*z) + a1*z + a0 by Th2
.= z|^3 + a2*z|^2 + a1*z + a0 by Th1;
hereby
assume z|^3 + a2*z|^2 + a1*z + a0 = 0;
then
A2: (z-s1)*(z-s2) = 0 or z-s3 = 0 by A1;
assume ( not z = s1)& not z = s2;
then z-s1<>0 & z-s2<>0;
hence z = s3 by A2;
end;
assume z = s1 or z = s2 or z = s3;
hence z|^3 + a2*z|^2 + a1*z + a0 = 0 by A1;
end;
:: Cardan's Solution
:: Mathematical Handbook for Scientists and Engineers (Korn) p.23
:: roots of cubic (I)
::$N Cubic equation
::$L https://en.wikipedia.org/wiki/Cubic_equation Cubic equation
theorem
q = (3*a1 - a2|^2)/9 & q <> 0 & r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s
= 2-root(q|^3+r|^2) & s1 = 3-root(r+s) & s2 = -q/s1 implies ( z|^3+a2*z|^2+a1*z
+a0 = 0 iff z = s1+s2-a2/3 or z = -(s1+s2)/2-a2/3+(s1-s2)*(2-root 3)*<i>/2 or z
= -(s1+s2)/2-a2/3-(s1-s2)*(2-root 3)*<i>/2)
proof
assume that
A1: q = (3*a1 - a2|^2)/9 and
A2: q <> 0;
assume
A3: r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54;
set t = (s1+s2)/2, d = (s1-s2)/2;
set x = z + a2/3;
set x1 = 2*t, x2 = -t+d*(2-root 3)*<i>, x3 = -t-d*(2-root 3)*<i>;
A4: -(x1+x2+x3) = 0;
assume
A5: s = 2-root(q|^3+r|^2);
assume
A6: s1 = 3-root(r+s);
A7: s1 <> 0
proof
assume s1 = 0;
then
A8: 0 = s1|^3 by NEWTON:11
.= r+s by A6,Th7;
q|^3+r|^2 = s|^2 by A5,Th7
.= s*s by Th1
.= (-s)*(-s)
.= r|^2 by A8,Th1;
then q*q*q = 0 by Th2;
hence contradiction by A2;
end;
assume
A9: s2 = -q/s1;
then
A10: s2*s2*s2 = -(q/s1)*(q/s1)*(q/s1) .= -((q*q)/(s1*s1))*(q/s1) by XCMPLX_1:76
.= -q*q*q/(s1*s1*s1) by XCMPLX_1:76
.= -(q*q*q)/3-root(r+s)|^3 by A6,Th2
.= -(q*q*q)/(r+s) by Th7
.= -q|^3/(r+s) by Th2;
A11: s1*s1*s1 = s1|^3 by Th2
.= r+s by A6,Th7;
A12: x1*x2+x1*x3+x2*x3 = -3*t*t-d*d*((2-root 3)*(2-root 3))*(-1)
.= -3*t*t-d*d*((2-root 3)|^2)*(-1) by Th1
.= -3*t*t-d*d*3*(-1) by Th7
.= 3*(s1*(q/s1)) by A9
.= 3*((s1*q)/s1) by XCMPLX_1:74
.= 3*q by A7,XCMPLX_1:89;
-x1*x2*x3 = (-2*t)*(t*t-d*d*((2-root 3)*(2-root 3))*(-1))
.= (-2*t)*(t*t-d*d*((2-root 3)|^2)*(-1)) by Th1
.= (-2*t)*(t*t-d*d*3*(-1)) by Th7
.= -((r+s)-q|^3/(r+s)) by A11,A10
.= -((r+s)*(r+s)/(r+s)-q|^3/(r+s)) by A11,A7,XCMPLX_1:89
.= -((r*r+2*s*r+s*s-q|^3)/(r+s)) by XCMPLX_1:120
.= -(((r*r+2*s*r)+(2-root(q|^3+r|^2))|^2-q|^3)/(r+s)) by A5,Th1
.= -(((r*r+2*s*r)+(q|^3+r|^2)-q|^3)/(r+s)) by Th7
.= -(((r*r+2*s*r)+r|^2)/(r+s))
.= -((r*r+2*s*r+r*r)/(r+s)) by Th1
.= -2*r*(r+s)/(r+s)
.= -2*r by A11,A7,XCMPLX_1:89;
then
A13: x|^3+0*x|^2+(3*q)*x+(-2*r) = 0 iff x = x1 or x = x2 or x = x3 by A4,A12
,Th14;
z = x - a2/3;
then z|^3+a2*z|^2+a1*z+a0 = 0 iff x|^3+3*q*x-2*r = 0 by A1,A3,Th13;
hence thesis by A13;
end;
:: roots of cubic (II)
::$L https://en.wikipedia.org/wiki/Cubic_equation Cubic equation
theorem
q = (3*a1 - a2|^2)/9 & q = 0 & r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1
= 3-root(2*r) implies ( z|^3+a2*z|^2+a1*z+a0 = 0 iff z = s1-a2/3 or z = -s1/2-
a2/3+s1*(2-root 3)*<i>/2 or z = -s1/2-a2/3-s1*(2-root 3)*<i>/2)
proof
assume that
A1: q = (3*a1 - a2|^2)/9 and
A2: q = 0;
set t = s1/2;
set x1 = 2*t, x2 = -t+t*(2-root 3)*<i>, x3 = -t-t*(2-root 3)*<i>;
A3: x1*x2+x1*x3+x2*x3 = -3*t*t-t*t*((2-root 3)*(2-root 3))*(-1)
.= -3*t*t-t*t*((2-root 3)|^2)*(-1) by Th1
.= -3*t*t-t*t*3*(-1) by Th7
.= 3*q by A2;
set x = z + a2/3;
assume
A4: r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54;
assume
A5: s1 = 3-root(2*r);
A6: -(x1+x2+x3) = 0;
A7: s1*s1*s1 = s1|^3 by Th2
.= 2*r by A5,Th7;
-x1*x2*x3 = (-2*t)*(t*t-t*t*((2-root 3)*(2-root 3))*(-1))
.= (-2*t)*(t*t-t*t*((2-root 3)|^2)*(-1)) by Th1
.= (-2*t)*(t*t-t*t*3*(-1)) by Th7
.= -2*r by A7;
then
A8: x|^3+0*x|^2+(3*q)*x+(-2*r) = 0 iff x = x1 or x = x2 or x = x3 by A6,A3,Th14
;
z = x - a2/3;
then z|^3+a2*z|^2+a1*z+a0 = 0 iff x|^3+3*q*x-2*r = 0 by A1,A4,Th13;
hence thesis by A8;
end;
definition
let a0,a1,a2 be Complex;
func 1_root_of_cubic(a0,a1,a2) -> Complex means
:Def2:
ex r,s1 st r =
(9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) & it = s1-a2/3 if 3*a1 - a2|^
2 = 0 otherwise ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/9 & r = (9*a2*a1 - 2*a2|^3
- 27*a0)/54 & s = 2-root(q|^3+r|^2) & s1 = 3-root(r+s) & s2 = -q/s1 & it = s1+
s2-a2/3;
existence
proof
set q = (3*a1 - a2|^2)/9, r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54, s = 2-root(q
|^3+r|^2), s1 = 3-root(r+s), s2 = -q/s1, IT = s1+s2-a2/3;
thus 3*a1 - a2|^2 = 0 implies ex IT,r,s1 being Complex st r = (9*a2
*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) & IT = s1-a2/3
proof
set r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54, s1 = 3-root(2*r), IT = s1-a2/3;
assume 3*a1 - a2|^2 = 0;
take IT,r,s1;
thus thesis;
end;
assume 3*a1 - a2|^2 <> 0;
take IT,q,r,s,s1,s2;
thus thesis;
end;
uniqueness;
correctness;
func 2_root_of_cubic(a0,a1,a2) -> Complex means
:Def3:
ex r,s1 st r =
(9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) & it = -s1/2-a2/3+s1*(2-root
3)*<i>/2 if 3*a1 - a2|^2 = 0 otherwise ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/9 &
r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s = 2-root(q|^3+r|^2) & s1 = 3-root(r+s) &
s2 = -q/s1 & it = -(s1+s2)/2-a2/3+(s1-s2)*(2-root 3)*<i>/2;
existence
proof
set q = (3*a1 - a2|^2)/9, r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54, s = 2-root(q
|^3+r|^2), s1 = 3-root(r+s), s2 = -q/s1, IT = -(s1+s2)/2-a2/3+(s1-s2)*(2-root 3
)*<i>/2;
thus 3*a1 - a2|^2 = 0 implies ex IT,r,s1 being Complex st r = (9*a2
*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) & IT = -s1/2-a2/3+s1*(2-root 3)*
<i>/2
proof
set r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54, s1 = 3-root(2*r), IT = -s1/2-a2/
3+s1*(2-root 3)*<i>/2;
assume 3*a1 - a2|^2 = 0;
take IT,r,s1;
thus thesis;
end;
assume 3*a1 - a2|^2 <> 0;
take IT,q,r,s,s1,s2;
thus thesis;
end;
uniqueness;
correctness;
func 3_root_of_cubic(a0,a1,a2) -> Complex means
:Def4:
ex r,s1 st r =
(9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) & it = -s1/2-a2/3-s1*(2-root
3)*<i>/2 if 3*a1 - a2|^2 = 0 otherwise ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/9 &
r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s = 2-root(q|^3+r|^2) & s1 = 3-root(r+s) &
s2 = -q/s1 & it = -(s1+s2)/2-a2/3-(s1-s2)*(2-root 3)*<i>/2;
existence
proof
set q = (3*a1 - a2|^2)/9, r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54, s = 2-root(q
|^3+r|^2), s1 = 3-root(r+s), s2 = -q/s1, IT = -(s1+s2)/2-a2/3-(s1-s2)*(2-root 3
)*<i>/2;
thus 3*a1 - a2|^2 = 0 implies ex IT,r,s1 being Complex st r = (9*a2
*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) & IT = -s1/2-a2/3-s1*(2-root 3)*
<i>/2
proof
set r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54, s1 = 3-root(2*r), IT = -s1/2-a2/
3-s1*(2-root 3)*<i>/2;
assume 3*a1 - a2|^2 = 0;
take IT,r,s1;
thus thesis;
end;
assume 3*a1 - a2|^2 <> 0;
take IT,q,r,s,s1,s2;
thus thesis;
end;
uniqueness;
correctness;
end;
theorem Th17:
1_root_of_cubic(a0,a1,a2)+2_root_of_cubic(a0,a1,a2)+
3_root_of_cubic(a0,a1,a2) = -a2
proof
per cases;
suppose
A1: 3*a1 - a2|^2 = 0;
then
A2: ex r,s1 st r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) &
3_root_of_cubic(a0,a1,a2) = -s1/2-a2/3-s1*(2-root 3)*<i>/2 by Def4;
( ex r,s1 st r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) &
1_root_of_cubic(a0,a1,a2) = s1-a2/3)& ex r,s1 st r = (9*a2*a1 - 2*a2|^3 - 27*
a0)/54 & s1 = 3-root(2*r) & 2_root_of_cubic(a0,a1,a2) = -s1/2-a2/3+s1*(2-root 3
)*<i>/2 by A1,Def2,Def3;
hence thesis by A2;
end;
suppose
A3: 3*a1 - a2|^2 <> 0;
then
A4: ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/9 & r = (9*a2*a1 - 2*a2|^3 - 27*
a0)/54 & s = 2-root(q|^3+r|^2) & s1 = 3-root(r+s) & s2 = -q/s1 &
3_root_of_cubic(a0,a1,a2) = -(s1+s2)/2-a2/3-(s1-s2)*(2-root 3)*<i>/2 by Def4;
( ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/9 & r = (9*a2*a1 - 2*a2|^3 - 27
*a0)/54 & s = 2-root(q|^3+r|^2) & s1 = 3-root(r+s) & s2 = -q/s1 &
1_root_of_cubic(a0,a1, a2) = s1+s2-a2/3)& ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/
9 & r = (9*a2*a1 - 2* a2|^3 - 27*a0)/54 & s = 2-root(q|^3+r|^2) & s1 = 3-root(r
+s) & s2 = -q/s1 & 2_root_of_cubic(a0,a1,a2) = -(s1+s2)/2-a2/3+(s1-s2)*(2-root
3)*<i>/2 by A3,Def2,Def3;
hence thesis by A4;
end;
end;
theorem Th18:
1_root_of_cubic(a0,a1,a2) * 2_root_of_cubic(a0,a1,a2) +
1_root_of_cubic(a0,a1,a2) * 3_root_of_cubic(a0,a1,a2) + 2_root_of_cubic(a0,a1,
a2) * 3_root_of_cubic(a0,a1,a2) = a1
proof
per cases;
suppose
A1: 3*a1 - a2|^2 = 0;
set r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54, s1 = 3-root(2*r);
A2: ( ex r,s1 st r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) &
2_root_of_cubic(a0,a1,a2) = -s1/2-a2/3+s1*(2-root 3)*<i>/2)& ex r,s1 st r = (9
*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) & 3_root_of_cubic(a0,a1,a2) = -
s1/2-a2/3-s1*(2-root 3)*<i>/2 by A1,Def3,Def4;
thus 1_root_of_cubic(a0,a1,a2) * 2_root_of_cubic(a0,a1,a2) +
1_root_of_cubic(a0,a1,a2) * 3_root_of_cubic(a0,a1,a2) + 2_root_of_cubic(a0,a1,
a2) * 3_root_of_cubic(a0,a1,a2) = 1_root_of_cubic(a0,a1,a2) * (2_root_of_cubic(
a0,a1,a2) + 3_root_of_cubic(a0,a1,a2)) + 2_root_of_cubic(a0,a1,a2) *
3_root_of_cubic(a0,a1,a2)
.= (s1-a2/3)*((-s1/2-a2/3+s1*(2-root 3)*<i>/2)+ (-s1/2-a2/3-s1*(2-root
3)*<i>/2))+ (-s1/2-a2/3+s1*(2-root 3)*<i>/2)* (-s1/2-a2/3-s1*(2-root 3)*<i>/2)
by A1,A2,Def2
.= (-3*s1*s1/4-a2*s1/3+3*a2*a2/9+a2*s1/3) -(s1*s1*((2-root 3)*(2-root
3))*(-1)/2/2)
.= (-3*s1*s1/4+a2*a2/3)-(s1*s1*((2-root 3)|^2)*(-1)/2/2) by Th1
.= (-3*s1*s1/4+a2*a2/3)-(s1*s1*3*(-1)/2/2) by Th7
.= (a2|^2)/3 by Th1
.= a1 by A1;
end;
suppose
A3: 3*a1 - a2|^2 <> 0;
set q = (3*a1 - a2|^2)/9, r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54, s = 2-root(q
|^3+r|^2), s1 = 3-root(r+s), s2 = -q/s1;
A4: s1 <> 0
proof
assume s1 = 0;
then
A5: 0 = s1|^3 by NEWTON:11
.= r+s by Th7;
q|^3+r|^2 = s|^2 by Th7
.= s*s by Th1
.= (-s)*(-s)
.= r|^2 by A5,Th1;
then q*q*q = 0 by Th2;
hence contradiction by A3;
end;
A6: ( ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/9 & r = (9*a2*a1 - 2*a2|^3 - 27
*a0)/54 & s = 2-root(q|^3+r|^2) & s1 = 3-root(r+s) & s2 = -q/s1 &
2_root_of_cubic(a0,a1, a2) = -(s1+s2)/2-a2/3+(s1-s2)*(2-root 3)*<i>/2)& ex q,r,
s,s1,s2 st q = (3*a1 - a2|^2)/9 & r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s = 2
-root(q|^3+r|^2) & s1 = 3 -root(r+s) & s2 = -q/s1 & 3_root_of_cubic(a0,a1,a2) =
-(s1+s2)/2-a2/3-(s1-s2)*( 2-root 3)*<i>/2 by A3,Def3,Def4;
set t = s1+s2, d = s1-s2;
thus 1_root_of_cubic(a0,a1,a2) * 2_root_of_cubic(a0,a1,a2) +
1_root_of_cubic(a0,a1,a2) * 3_root_of_cubic(a0,a1,a2) + 2_root_of_cubic(a0,a1,
a2) * 3_root_of_cubic(a0,a1,a2) = 1_root_of_cubic(a0,a1,a2) * (2_root_of_cubic(
a0,a1,a2) + 3_root_of_cubic(a0,a1,a2)) + 2_root_of_cubic(a0,a1,a2) *
3_root_of_cubic(a0,a1,a2)
.= (t-a2/3)*((-t/2-a2/3+d*(2-root 3)*<i>/2)+ (-t/2-a2/3-d*(2-root 3)*
<i>/2))+(-t/2-a2/3+d*(2-root 3)*<i>/2)* (-t/2-a2/3-d*(2-root 3)*<i>/2) by A3,A6
,Def2
.= (-3*t*t/4-a2*t/3+3*a2*a2/9+a2*t/3)-(d*d*((2-root 3)*(2-root 3))*(-1
)/4)
.= (-3*t*t/4+a2*a2/3)-(d*d*((2-root 3)|^2)*(-1)/4) by Th1
.= (-3*t*t/4+a2*a2/3)-(d*d*(3)*(-1)/4) by Th7
.= 3*s1*(q/s1)+a2*a2/3
.= 3*q+a2*a2/3 by A4,XCMPLX_1:90
.= 3*q+a2|^2/3 by Th1
.= a1;
end;
end;
theorem Th19:
1_root_of_cubic(a0,a1,a2) * 2_root_of_cubic(a0,a1,a2) *
3_root_of_cubic(a0,a1,a2) = -a0
proof
per cases;
suppose
A1: 3*a1 - a2|^2 = 0;
set r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54, s1 = 3-root(2*r);
( ex r,s1 st r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) &
2_root_of_cubic(a0,a1,a2) = -s1/2-a2/3+s1*(2-root 3)*<i>/2)& ex r,s1 st r = (9
*a2*a1 - 2*a2|^3 - 27*a0)/54 & s1 = 3-root(2*r) & 3_root_of_cubic(a0,a1,a2) = -
s1/2-a2/3-s1*(2-root 3)*<i>/2 by A1,Def3,Def4;
hence 1_root_of_cubic(a0,a1,a2) * 2_root_of_cubic(a0,a1,a2) *
3_root_of_cubic(a0,a1,a2) = (s1-a2/3)*(-s1/2-a2/3+s1*(2-root 3)*<i>/2)* (-s1/2-
a2/3-s1*(2-root 3)*<i>/2) by A1,Def2
.= (s1-a2/3)*((s1/2+a2/3)*(s1/2+a2/3)+(2-root 3)*(2-root 3)*s1*s1/2/2)
.= (s1-a2/3)*((s1/2+a2/3)*(s1/2+a2/3)+(2-root 3)|^2*s1*s1/2/2) by Th1
.= (s1-a2/3)*((s1/2+a2/3)*(s1/2+a2/3)+3*s1*s1/2/2) by Th7
.= s1*s1*s1-a2*a2*a2/3/3/3
.= s1|^3-a2*a2*a2/27 by Th2
.= 2*r-a2*a2*a2/27 by Th7
.= (9*a2*a1 - 2*a2|^3 - 27*a0)/27-a2|^3/27 by Th2
.= (3*a2*a1 - a2|^(2+1))/9 -a0
.= (3*a2*a1 - a2|^2*a2)/9 -a0 by NEWTON:6
.= -a0 by A1;
end;
suppose
A2: 3*a1 - a2|^2 <> 0;
set q = (3*a1 - a2|^2)/9, r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54, s = 2-root(q
|^3+r|^2), s1 = 3-root(r+s), s2 = -q/s1;
A3: s1 <> 0
proof
assume s1 = 0;
then
A4: 0 = s1|^3 by NEWTON:11
.= r+s by Th7;
q|^3+r|^2 = s|^2 by Th7
.= s*s by Th1
.= (-s)*(-s)
.= r|^2 by A4,Th1;
then q*q*q = 0 by Th2;
hence contradiction by A2;
end;
A5: s1*s1*s1 = s1|^3 by Th2
.= r+s by Th7;
then
A6: (r+s)-(q*q*q)/(r+s) = (r+s)*(r+s)/(r+s)-(q*q*q)/(r+s) by A3,XCMPLX_1:89
.= ((r+s)*(r+s)-(q*q*q))/(r+s) by XCMPLX_1:120
.= (r*r+2*r*s+s*s-q|^3)/(r+s) by Th2
.= (r*r+2*r*s+s|^2-q|^3)/(r+s) by Th1
.= (r*r+2*r*s+(q|^3+r|^2)-q|^3)/(r+s) by Th7
.= ((r*r+2*r*s)+r|^2)/(r+s)
.= ((r*r+2*r*s)+r*r)/(r+s) by Th1
.= 2*r*(r+s)/(r+s)
.= 2*r by A5,A3,XCMPLX_1:89;
set t = s1+s2, d = s1-s2;
A7: s1*s2 = -(q/s1*s1) .= -q by A3,XCMPLX_1:87;
( ex q,r,s,s1,s2 st q = (3*a1 - a2|^2)/9 & r = (9*a2*a1 - 2*a2|^3 - 27
*a0)/54 & s = 2-root(q|^3+r|^2) & s1 = 3-root(r+s) & s2 = -q/s1 &
2_root_of_cubic(a0,a1, a2) = -(s1+s2)/2-a2/3+(s1-s2)*(2-root 3)*<i>/2)& ex q,r,
s,s1,s2 st q = (3*a1 - a2|^2)/9 & r = (9*a2*a1 - 2*a2|^3 - 27*a0)/54 & s = 2
-root(q|^3+r|^2) & s1 = 3 -root(r+s) & s2 = -q/s1 & 3_root_of_cubic(a0,a1,a2) =
-(s1+s2)/2-a2/3-(s1-s2)*( 2-root 3)*<i>/2 by A2,Def3,Def4;
hence 1_root_of_cubic(a0,a1,a2) * 2_root_of_cubic(a0,a1,a2) *
3_root_of_cubic(a0,a1,a2) = (t-a2/3)*(-t/2-a2/3+d*(2-root 3)*<i>/2)* (-t/2-a2/3
-d*(2-root 3)*<i>/2) by A2,Def2
.= (t-a2/3)*((t/2+a2/3)*(t/2+a2/3)+(2-root 3)*(2-root 3)*d*d/2/2)
.= (t-a2/3)*((t/2+a2/3)*(t/2+a2/3)+(2-root 3)|^2*d*d/2/2) by Th1
.= (t-a2/3)*((t/2+a2/3)*(t/2+a2/3)+3*d*d/2/2) by Th7
.= (s1*s1*s1+s2*s2*s2)+a2*(4*s1*s2)/4-a2*a2*a2/27
.= (s1|^3+s2*s2*s2)+a2*(s1*s2)-a2*a2*a2/27 by Th2
.= (s1|^3+(-q/s1)*(-q/s1)*(-q/s1))+a2*(-q)-a2*a2*a2/27 by A7
.= (s1|^3-(q/s1)*(q/s1)*(q/s1))-a2*q-a2*a2*a2/27
.= (s1|^3-(q*q)/(s1*s1)*(q/s1))-a2*q-a2*a2*a2/27 by XCMPLX_1:76
.= (s1|^3-(q*q*q)/(s1*s1*s1))-a2*q-a2*a2*a2/27 by XCMPLX_1:76
.= (s1|^3-(q*q*q)/(s1|^3))-a2*q-a2*a2*a2/27 by Th2
.= (s1|^3-(q*q*q)/(r+s))-a2*q-a2*a2*a2/27 by Th7
.= ((r+s)-(q*q*q)/(r+s))-a2*q-a2*a2*a2/27 by Th7
.= 2*(9*a2*a1 - 2*a2|^3 - 27*a0)/54-a2*q-a2|^3/27 by A6,Th2
.= (9*a2*a1 - 3*a2|^3)/27 -a2*q -a0
.= (9*a2*a1 - 3*(a2*a2*a2))/27 -a2*q -a0 by Th2
.= a2*(3*a1 - (a2*a2))/9 -a2*q -a0
.= a2*(3*a1 - a2|^2)/9 -a2*q -a0 by Th1
.= -a0;
end;
end;
theorem
a3 <> 0 implies (a3*z|^3 + a2*z|^2 + a1*z + a0 = 0 iff z =
1_root_of_cubic(a0/a3,a1/a3,a2/a3) or z = 2_root_of_cubic(a0/a3,a1/a3,a2/a3) or
z = 3_root_of_cubic(a0/a3,a1/a3,a2/a3))
proof
assume
A1: a3<>0;
set s3 = 3_root_of_cubic(a0/a3,a1/a3,a2/a3);
set s2 = 2_root_of_cubic(a0/a3,a1/a3,a2/a3);
set s1 = 1_root_of_cubic(a0/a3,a1/a3,a2/a3);
-a2/a3 = (s1+s2+s3) by Th17;
then
A2: a2/a3 = -(s1+s2+s3);
-a0/a3 = s1*s2*s3 by Th19;
then
A3: a0/a3 = -s1*s2*s3;
(z|^3 + (a2/a3)*z|^2 + (a1/a3)*z + a0/a3)*a3 = a3*z|^3 + (a2/a3*a3)*z|^2
+ (a1/a3*a3)*z + a0/a3*a3
.= a3*z|^3 + (a2/a3*a3)*z|^2 + (a1/a3*a3)*z + a0 by A1,XCMPLX_1:87
.= a3*z|^3 + (a2/a3*a3)*z|^2 + a1*z + a0 by A1,XCMPLX_1:87
.= a3*z|^3 + a2*z|^2 + a1*z + a0 by A1,XCMPLX_1:87;
then
A4: z|^3 + (a2/a3)*z|^2 + (a1/a3)*z + a0/a3 = 0 iff a3* z|^3 + a2*z|^2 + a1*
z + a0 = 0 by A1;
a1/a3 = s1*s2+s1*s3+s2*s3 by Th18;
hence thesis by A4,A2,A3,Th14;
end;
begin :: Solution of Quartic Equations
reserve a4,p,s4 for Complex;
theorem Th21:
z = x - a3/4 & p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3|^
3)/64 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 implies (z|^4+a3*z|^3
+a2*z|^2+a1*z+a0 = 0 iff x|^4+4*p*x|^2+8*q*x+4*r = 0)
proof
assume
A1: z = x - a3/4;
then
A2: 4*z = 4*x - a3;
A3: 16*z|^2 = (4*4)*z|^2 .= (4|^2*z|^2) by Th1
.= (4*z)|^2 by NEWTON:7
.= (4*x)|^2 -2*(4*x)*a3 +a3|^2 by A2,Th4
.= (4*x)*(4*x) -2*(4*x)*a3 +a3|^2 by Th1
.= 16*(x*x) -8*x*a3 +a3|^2
.= 16*x|^2 -8*x*a3 +a3|^2 by Th1;
A4: (4*x)|^3 = (4|^3)*(x|^3) by NEWTON:7
.= (4*4*4)*x|^3 by Th2
.= 64*x|^3;
A5: (4*x)|^2 = 4|^2*x|^2 by NEWTON:7
.= (4*4)*x|^2 by Th1
.= 16*x|^2;
A6: 4*a3*(64*z|^3) = 4*a3*(4*4*4*z|^3) .= 4*a3*(4|^3*z|^3) by Th2
.= 4*a3*((4*x) - a3)|^3 by A2,NEWTON:7
.= 4*a3*(64*x|^3-3*(16*x|^2)*a3+3*a3|^2*(4*x)-a3|^3) by A4,A5,Th5
.= 256*a3*x|^3-192*(a3*a3)*x|^2+48*(a3|^2*a3)*x-4*(a3|^3*a3)
.= 256*a3*x|^3-192*(a3|^2)*x|^2+48*(a3|^2*a3)*x-4*(a3|^3*a3) by Th1
.= 256*a3*x|^3-192*a3|^2*x|^2+48*(a3|^(2+1))*x-4*(a3|^3*a3) by NEWTON:6
.= 256*a3*x|^3-192*a3|^2*x|^2+48*(a3|^3)*x-4*(a3|^(3+1)) by NEWTON:6
.= 256*a3*x|^3-192*a3|^2*x|^2+48*a3|^3*x-4*a3|^4;
A7: (4*x)|^4 = (4|^4)*(x|^4) by NEWTON:7
.= (4*4*4*4)*x|^4 by Th3
.= 256*x|^4;
A8: 256*z|^4 = 4*4*4*4*z|^4 .= 4|^4*z|^4 by Th3
.= ((4*x) - a3)|^4 by A2,NEWTON:7
.= 256*x|^4-4*(64*x|^3)*a3+6*(16*x|^2)*a3|^2-4*a3|^3*(4*x)+a3|^4 by A7,A4
,A5,Th6
.= 256*x|^4-256*x|^3*a3+96*x|^2*a3|^2-16*a3|^3*x+a3|^4;
assume
A9: p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3|^3)/64 & r = (256*a0
-64 *a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024;
256*(z|^4+a3*z|^3+a2*z|^2+a1*z+a0) = 256*z|^4+4*a3*(64*z|^3)+16*a2*(16*
z|^2)+64*a1*(4*z)+256*a0
.= (256*x|^4-256*x|^3*a3+96*x|^2*a3|^2-16*a3|^3*x+a3|^4) +(256*a3*x|^3-
192*a3|^2*x|^2+48*a3|^3*x-4*a3|^4) +16*a2*(16*x|^2 -8*x*a3 +a3|^2)+64*a1*(4*x -
a3)+256*a0 by A1,A8,A6,A3
.= 256*(x|^4+4*p*x|^2+8*q*x+4*r) by A9;
hence thesis;
end;
theorem Th22:
a3 = -(s1+s2+s3+s4) & a2 = s1*s2+s1*s3+s1*s4+s2*s3+s2*s4+s3*s4 &
a1 = -(s1*s2*s3+s1*s2*s4+s1*s3*s4+s2*s3*s4) & a0=s1*s2*s3*s4 implies (z|^4 + a3
*z|^3 + a2*z|^2 + a1*z + a0 = 0 iff z = s1 or z = s2 or z = s3 or z = s4)
proof
assume a3 = -(s1+s2+s3+s4) & a2 = s1*s2+s1*s3+s1*s4+s2*s3+s2*s4+s3*s4 & a1
= -(s1*s2*s3+s1*s2*s4+s1*s3*s4+s2*s3*s4) & a0=s1*s2*s3*s4;
then
A1: (z-s1)*(z-s2)*(z-s3)*(z-s4) = z*z*z*z + a3*z*z*z +a2*z*z +a1*z +a0
.= z|^4 + a3*(z*z*z) + a2*z*z + a1*z + a0 by Th3
.= z|^4 + a3*z|^3 + a2*(z*z) + a1*z + a0 by Th2
.= z|^4 + a3*z|^3 + a2*z|^2 + a1*z + a0 by Th1;
hereby
assume z|^4 + a3*z|^3 + a2*z|^2 + a1*z + a0 = 0;
then
A2: (z-s1)*(z-s2)*(z-s3) = 0 or z-s4 = 0 by A1;
assume that
A3: ( not z = s1)& not z = s2 and
A4: not z = s3;
A5: z-s3<>0 by A4;
z-s1<>0 & z-s2<>0 by A3;
hence z = s4 by A2,A5;
end;
assume z = s1 or z = s2 or z = s3 or z = s4;
hence z|^4 + a3*z|^3 + a2*z|^2 + a1*z + a0 = 0 by A1;
end;
:: Descartes-Euler Solution
:: Mathematical Handbook for Scientists and Engineers (Korn) p.24
theorem Th23:
q <> 0 & s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*p)) & s2 = 2
-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1*s2) implies (z|^4+4*p*z
|^2+8*q*z+4*r = 0 iff z = s1+s2+s3 or z = s1-s2-s3 or z = -s1+s2-s3 or z = -s1-
s2+s3)
proof
set z1 = s1+s2+s3, z2 = s1-s2-s3, z3 = -s1+s2-s3, z4 = -s1-s2+s3;
assume q <> 0;
then
A1: q*q <> 0;
assume
A2: s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*p));
assume
A3: s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p));
A4: s2*s2 = s2|^2 by Th1
.= 2_root_of_cubic(-q|^2,p|^2-r,2*p) by A3,Th7;
A5: s1*s1 = s1|^2 by Th1
.= 1_root_of_cubic(-q|^2,p|^2-r,2*p) by A2,Th7;
then
A6: (s1*s1)*(s2*s2)*3_root_of_cubic(-q|^2,p|^2-r,2*p) = -(-q|^2) by A4,Th19;
then
A7: (s1*s1)*(s2*s2)<>0 by A1,Th1;
(s1*s2)*(s1*s2)<>0 by A1,A6,Th1;
then
A8: s1*s2<>0;
assume
A9: s3 = -q/(s1*s2);
then
A10: -(z1*z2*z3+z1*z2*z4+z1*z3*z4+z2*z3*z4) = -8*(s1*s2)*(-q/(s1*s2))
.= -8*(s1*s2)*((-q)/(s1*s2)) by XCMPLX_1:187
.= -8*((s1*s2)*((-q)/(s1*s2)))
.= -8*((-q)/((s1*s2)/(s1*s2))) by XCMPLX_1:81
.= -8*((-q)/1) by A8,XCMPLX_1:60
.= 8*q;
A11: s3*s3 = ((-q)/(s1*s2))*(-q/(s1*s2)) by A9,XCMPLX_1:187
.= ((-q)/(s1*s2))*((-q)/(s1*s2)) by XCMPLX_1:187
.= (-q)*(-q)/((s1*s2)*(s1*s2)) by XCMPLX_1:76
.= (q*q)/((s1*s1)*(s2*s2))
.= 3_root_of_cubic(-q|^2,p|^2-r,2*p)*((s1*s1)*(s2*s2)) /((s1*s1)*(s2*s2)
) by A6,Th1
.= 3_root_of_cubic(-q|^2,p|^2-r,2*p) by A7,XCMPLX_1:89;
then
A12: s1*s1+s2*s2+s3*s3 = -2*p by A5,A4,Th17;
then
A13: -(z1+z2+z3+z4) = 0 & z1*z2+z1*z3+z1*z4+z2*z3+z2*z4+z3*z4 = 4*p;
z1*z2*z3*z4 = (s1*s1+s2*s2+s3*s3)*(s1*s1+s2*s2+s3*s3) -4*((s1*s1)*(s2*
s2)+(s1*s1)*(s3*s3)+(s2*s2)*(s3*s3))
.= (-2*p)*(-2*p)-4*((s1*s1)*(s2*s2)+(s1*s1)*(s3*s3)+(s2*s2)*(s3*s3)) by A12
.= 4*(p*p)-4*(p|^2-r) by A5,A4,A11,Th18
.= 4*(p|^2)-4*(p|^2-r) by Th1
.= 4*r;
then z|^4 + 0*z|^3 + 4*p*z|^2 + 8*q*z + 4*r = 0 iff z = z1 or z = z2 or z =
z3 or z = z4 by A13,A10,Th22;
hence thesis;
end;
:: roots of quartic (I)
theorem
p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3|^3)/64 & q <> 0 & r =
(256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(1_root_of_cubic(-q
|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1
*s2) implies ( z|^4+a3*z|^3+a2*z|^2+a1*z+a0 = 0 iff z = s1+s2+s3-a3/4 or z = s1
-s2-s3-a3/4 or z = -s1+s2-s3-a3/4 or z = -s1-s2+s3-a3/4)
proof
assume
A1: p = (8*a2-3*a3|^2)/32;
set x = z + a3/4;
assume that
A2: q = (8*a1 -4*a2*a3 + a3|^3)/64 and
A3: q <> 0;
assume
A4: r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024;
A5: z = x - a3/4;
assume s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*p)) & s2 = 2-root(
2_root_of_cubic (-q|^2,p|^2-r,2*p)) & s3 = -q/(s1*s2);
then
x|^4+4*p*x|^2+8*q*x+4*r = 0 iff x = s1+s2+s3 or x = s1-s2-s3 or x = -s1+
s2-s3 or x = -s1-s2+s3 by A3,Th23;
hence thesis by A1,A2,A4,A5,Th21;
end;
:: roots of quartic (II)
theorem
p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3|^3)/64 & q = 0 & r = (
256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) implies ( z
|^4+a3*z|^3+a2*z|^2+a1*z+a0 = 0 iff z = 2-root(-2*(p-s1))-a3/4 or z = -2-root(-
2*(p-s1))-a3/4 or z = 2-root(-2*(p+s1))-a3/4 or z = -2-root(-2*(p+s1))-a3/4)
proof
assume
A1: p = (8*a2-3*a3|^2)/32;
set x = z + a3/4;
assume that
A2: q = (8*a1 -4*a2*a3 + a3|^3)/64 and
A3: q = 0;
A4: z = x - a3/4;
assume r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024;
then
A5: z|^4+a3*z|^3+a2*z|^2+a1*z+a0 = 0 iff x|^4+4*p*x|^2+8*q*x+4*r = 0 by A1,A2
,A4,Th21;
assume
A6: s1 = 2-root(p|^2-r);
set y = x|^2;
A7: y|^2 = x|^(2*2) by NEWTON:9
.= x|^4;
A8: x|^2 = -2*p+2-root(delta(4*r,4*p,1))/2 iff x = 2-root(-2*p+2-root(delta
(4*r,4*p,1))/2) or x = -2-root(-2*p+2-root(delta(4*r,4*p,1))/2) by Th10;
A9: x|^2 = -2*p-2-root(delta(4*r,4*p,1))/2 iff x = 2-root(-2*p-2-root(delta
(4*r,4*p,1))/2) or x = -2-root(-2*p-2-root(delta(4*r,4*p,1))/2) by Th10;
A10: 4|^2 = 4*4 by Th1
.= 16;
1*y|^2+4*p*y+4*r = 0 iff y = -(4*p)/(2*1)+2-root(delta(4*r,4*p,1))/(2*1
) or y = -(4*p)/(2*1)-2-root(delta(4*r,4*p,1))/(2*1) by Th12;
then
A11: 1*y|^2+4*p*y+4*r = 0 iff z = 2-root(-2*p+2-root(delta(4*r,4*p,1))/2)-a3
/4 or z = -2-root(-2*p+2-root(delta(4*r,4*p,1))/2)-a3/4 or z = 2-root(-2*p-2
-root(delta(4*r,4*p,1))/2)-a3/4 or z = -2-root(-2*p-2-root(delta(4*r,4*p,1))/2)
-a3/4 by A8,A9;
2-root 16 = 2-real-root 16 by Th8
.= 2-Root 16 by POWER:def 1
.= 4 by A10,PREPOWER:def 2;
then 2-root(delta(4*r,4*p,1))/4 = 2-root(16*(p*p-r)/16) by Th9
.= s1 by A6,Th1;
hence thesis by A3,A5,A7,A11;
end;
definition
let a0,a1,a2,a3 be Complex;
func 1_root_of_quartic(a0,a1,a2,a3) -> Complex means
:Def5:
ex p,r,s1
st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
s1 = 2-root(p|^2-r) & it = 2-root(-2*(p-s1))-a3/4 if 8*a1 -4*a2*a3 + a3|^3 = 0
otherwise ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3
|^3)/64 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(
1_root_of_cubic(-q|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2
*p)) & s3 = -q/(s1*s2) & it = s1+s2+s3-a3/4;
existence
proof
set p = (8*a2-3*a3|^2)/32, q = (8*a1 -4*a2*a3 + a3|^3)/64, r = (256*a0 -64
*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024, s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*
p)), s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)), s3 = -q/(s1*s2), IT = s1+
s2+s3-a3/4;
thus 8*a1 -4*a2*a3 + a3|^3 = 0 implies ex IT,p,r,s1 being Complex
st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
s1 = 2-root(p|^2-r) & IT = 2-root(-2*(p-s1))-a3/4
proof
set p = (8*a2-3*a3|^2)/32, r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/
1024, s1 = 2-root(p|^2-r), IT = 2-root(-2*(p-s1))-a3/4;
assume 8*a1 -4*a2*a3 + a3|^3 = 0;
take IT,p,r,s1;
thus thesis;
end;
assume 8*a1 -4*a2*a3 + a3|^3 <> 0;
take IT,p,q,r,s1,s2,s3;
thus thesis;
end;
uniqueness;
correctness;
func 2_root_of_quartic(a0,a1,a2,a3) -> Complex means
:Def6:
ex p,r,s1
st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
s1 = 2-root(p|^2-r) & it = -2-root(-2*(p-s1))-a3/4 if 8*a1 -4*a2*a3 + a3|^3 = 0
otherwise ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3
|^3)/64 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(
1_root_of_cubic(-q|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2
*p)) & s3 = -q/(s1*s2) & it = -s1-s2+s3-a3/4;
existence
proof
set p = (8*a2-3*a3|^2)/32, q = (8*a1 -4*a2*a3 + a3|^3)/64, r = (256*a0 -64
*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024, s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*
p)), s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)), s3 = -q/(s1*s2), IT = -s1-
s2+s3-a3/4;
thus 8*a1 -4*a2*a3 + a3|^3 = 0 implies ex IT,p,r,s1 being Complex
st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
s1 = 2-root(p|^2-r) & IT = -2-root(-2*(p-s1))-a3/4
proof
set p = (8*a2-3*a3|^2)/32, r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/
1024, s1 = 2-root(p|^2-r), IT = -2-root(-2*(p-s1))-a3/4;
assume 8*a1 -4*a2*a3 + a3|^3 = 0;
take IT,p,r,s1;
thus thesis;
end;
assume 8*a1 -4*a2*a3 + a3|^3 <> 0;
take IT,p,q,r,s1,s2,s3;
thus thesis;
end;
uniqueness;
correctness;
func 3_root_of_quartic(a0,a1,a2,a3) -> Complex means
:Def7:
ex p,r,s1
st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
s1 = 2-root(p|^2-r) & it = 2-root(-2*(p+s1))-a3/4 if 8*a1 -4*a2*a3 + a3|^3 = 0
otherwise ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3
|^3)/64 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(
1_root_of_cubic(-q|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2
*p)) & s3 = -q/(s1*s2) & it = -s1+s2-s3-a3/4;
existence
proof
set p = (8*a2-3*a3|^2)/32, q = (8*a1 -4*a2*a3 + a3|^3)/64, r = (256*a0 -64
*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024, s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*
p)), s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)), s3 = -q/(s1*s2), IT = -s1+
s2-s3-a3/4;
thus 8*a1 -4*a2*a3 + a3|^3 = 0 implies ex IT,p,r,s1 being Complex
st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
s1 = 2-root(p|^2-r) & IT = 2-root(-2*(p+s1))-a3/4
proof
set p = (8*a2-3*a3|^2)/32, r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/
1024, s1 = 2-root(p|^2-r), IT = 2-root(-2*(p+s1))-a3/4;
assume 8*a1 -4*a2*a3 + a3|^3 = 0;
take IT,p,r,s1;
thus thesis;
end;
assume 8*a1 -4*a2*a3 + a3|^3 <> 0;
take IT,p,q,r,s1,s2,s3;
thus thesis;
end;
uniqueness;
correctness;
func 4_root_of_quartic(a0,a1,a2,a3) -> Complex means
:Def8:
ex p,r,s1
st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
s1 = 2-root(p|^2-r) & it = -2-root(-2*(p+s1))-a3/4 if 8*a1 -4*a2*a3 + a3|^3 = 0
otherwise ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3
|^3)/64 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(
1_root_of_cubic(-q|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2
*p)) & s3 = -q/(s1*s2) & it = s1-s2-s3-a3/4;
existence
proof
set p = (8*a2-3*a3|^2)/32, q = (8*a1 -4*a2*a3 + a3|^3)/64, r = (256*a0 -64
*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024, s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*
p)), s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)), s3 = -q/(s1*s2), IT = s1-
s2-s3-a3/4;
thus 8*a1 -4*a2*a3 + a3|^3 = 0 implies ex IT,p,r,s1 being Complex
st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 &
s1 = 2-root(p|^2-r) & IT = -2-root(-2*(p+s1))-a3/4
proof
set p = (8*a2-3*a3|^2)/32, r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/
1024, s1 = 2-root(p|^2-r), IT = -2-root(-2*(p+s1))-a3/4;
assume 8*a1 -4*a2*a3 + a3|^3 = 0;
take IT,p,r,s1;
thus thesis;
end;
assume 8*a1 -4*a2*a3 + a3|^3 <> 0;
take IT,p,q,r,s1,s2,s3;
thus thesis;
end;
uniqueness;
correctness;
end;
theorem Th26:
1_root_of_quartic(a0,a1,a2,a3)+2_root_of_quartic(a0,a1,a2,a3)+
3_root_of_quartic(a0,a1,a2,a3)+4_root_of_quartic(a0,a1,a2,a3) = -a3
proof
per cases;
suppose
A1: 8*a1 -4*a2*a3 + a3|^3 = 0;
then
A2: ( ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2
*a2 -3*a3 |^4)/1024 & s1 = 2-root(p|^2-r) & 3_root_of_quartic(a0,a1,a2,a3) = 2
-root(-2*(p +s1))-a3/4)& ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*
a3*a1 +16*a3 |^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) & 4_root_of_quartic(a0
,a1,a2,a3) = -2-root(-2*(p+s1))-a3/4 by Def7,Def8;
( ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2
*a2 -3*a3 |^4)/1024 & s1 = 2-root(p|^2-r) & 1_root_of_quartic(a0,a1,a2,a3) = 2
-root(-2*(p -s1))-a3/4)& ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*
a3*a1 +16*a3 |^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) & 2_root_of_quartic(a0
,a1,a2,a3) = -2-root(-2*(p-s1))-a3/4 by A1,Def5,Def6;
hence thesis by A2;
end;
suppose
A3: 8*a1 -4*a2*a3 + a3|^3 <> 0;
then
A4: ( ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3
|^3)/64 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(
1_root_of_cubic (-q|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,
2*p)) & s3 = -q/ (s1*s2) & 3_root_of_quartic(a0,a1,a2,a3) = -s1+s2-s3-a3/4)& ex
p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3|^3)/64 & r =
(256*a0 -64*a3* a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(1_root_of_cubic(-q
|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1
*s2) & 4_root_of_quartic(a0,a1,a2,a3) = s1-s2-s3-a3/4 by Def7,Def8;
( ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3
|^3)/64 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(
1_root_of_cubic (-q|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,
2*p)) & s3 = -q/ (s1*s2) & 1_root_of_quartic(a0,a1,a2,a3) = s1+s2+s3-a3/4)& ex
p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3|^3)/64 & r =
(256*a0 -64*a3* a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(1_root_of_cubic(-q
|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1
*s2) & 2_root_of_quartic(a0,a1,a2,a3) = -s1-s2+s3-a3/4 by A3,Def5,Def6;
hence thesis by A4;
end;
end;
theorem Th27:
(1_root_of_quartic(a0,a1,a2,a3)*2_root_of_quartic(a0,a1,a2,a3)+
1_root_of_quartic(a0,a1,a2,a3)*3_root_of_quartic(a0,a1,a2,a3)+
1_root_of_quartic(a0,a1,a2,a3)*4_root_of_quartic(a0,a1,a2,a3))+
2_root_of_quartic(a0,a1,a2,a3)*3_root_of_quartic(a0,a1,a2,a3)+
2_root_of_quartic(a0,a1,a2,a3)*4_root_of_quartic(a0,a1,a2,a3)+
3_root_of_quartic(a0,a1,a2,a3)*4_root_of_quartic(a0,a1,a2,a3) = a2
proof
per cases;
suppose
A1: 8*a1 -4*a2*a3 + a3|^3 = 0;
set p = (8*a2-3*a3|^2)/32, r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/
1024, s1 = 2-root(p|^2-r);
set t1 = 2-root(-2*(p-s1)), t2 = 2-root(-2*(p+s1));
A2: ( ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2
*a2 -3*a3 |^4)/1024 & s1 = 2-root(p|^2-r) & 3_root_of_quartic(a0,a1,a2,a3) = 2
-root(-2*(p +s1))-a3/4)& ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*
a3*a1 +16*a3 |^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) & 4_root_of_quartic(a0
,a1,a2,a3) = -2-root(-2*(p+s1))-a3/4 by A1,Def7,Def8;
( ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2
*a2 -3*a3 |^4)/1024 & s1 = 2-root(p|^2-r) & 1_root_of_quartic(a0,a1,a2,a3) = 2
-root(-2*(p -s1))-a3/4)& ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*
a3*a1 +16*a3 |^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) & 2_root_of_quartic(a0
,a1,a2,a3) = -2-root(-2*(p-s1))-a3/4 by A1,Def5,Def6;
hence (1_root_of_quartic(a0,a1,a2,a3)*2_root_of_quartic(a0,a1,a2,a3)+
1_root_of_quartic(a0,a1,a2,a3)*3_root_of_quartic(a0,a1,a2,a3)+
1_root_of_quartic(a0,a1,a2,a3)*4_root_of_quartic(a0,a1,a2,a3))+
2_root_of_quartic(a0,a1,a2,a3)*3_root_of_quartic(a0,a1,a2,a3)+
2_root_of_quartic(a0,a1,a2,a3)*4_root_of_quartic(a0,a1,a2,a3)+
3_root_of_quartic(a0,a1,a2,a3)*4_root_of_quartic(a0,a1,a2,a3) = (4+1+1)*a3*a3/
16-t1*t1-t2*t2 by A2
.= 3*a3*a3/8-t1|^2-t2*t2 by Th1
.= 3*a3*a3/8-(-2*(p-s1))-t2*t2 by Th7
.= 3*a3*a3/8+2*(p-s1)-t2|^2 by Th1
.= 3*a3*a3/8+2*(p-s1)-(-2*(p+s1)) by Th7
.= 3*a3*a3/8+(8*a2-3*a3|^2)/8
.= 3*a3*a3/8+(8*a2-3*(a3*a3))/8 by Th1
.= a2;
end;
suppose
A3: 8*a1 -4*a2*a3 + a3|^3 <> 0;
then
A4: ( ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3
|^3)/64 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(
1_root_of_cubic (-q|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,
2*p)) & s3 = -q/ (s1*s2) & 3_root_of_quartic(a0,a1,a2,a3) = -s1+s2-s3-a3/4)& ex
p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3|^3)/64 & r =
(256*a0 -64*a3* a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(1_root_of_cubic(-q
|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1
*s2) & 4_root_of_quartic(a0,a1,a2,a3) = s1-s2-s3-a3/4 by Def7,Def8;
set p = (8*a2-3*a3|^2)/32, q = (8*a1 -4*a2*a3 + a3|^3)/64, r = (256*a0 -64
*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024, s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*
p)), s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)), s3 = -q/(s1*s2);
A5: s2*s2 = s2|^2 by Th1
.= 2_root_of_cubic(-q|^2,p|^2-r,2*p) by Th7;
A6: s1*s1 = s1|^2 by Th1
.= 1_root_of_cubic(-q|^2,p|^2-r,2*p) by Th7;
then
A7: (s1*s1)*(s2*s2)*3_root_of_cubic(-q|^2,p|^2-r,2*p) = -(-q|^2) by A5,Th19;
q*q <> 0 by A3;
then
A8: (s1*s1)*(s2*s2)<>0 by A7,Th1;
A9: s3*s3 = ((-q)/(s1*s2))*(-q/(s1*s2)) by XCMPLX_1:187
.= ((-q)/(s1*s2))*((-q)/(s1*s2)) by XCMPLX_1:187
.= (-q)*(-q)/((s1*s2)*(s1*s2)) by XCMPLX_1:76
.= (q*q)/((s1*s1)*(s2*s2))
.= 3_root_of_cubic(-q|^2,p|^2-r,2*p)*((s1*s1)*(s2*s2)) /((s1*s1)*(s2*
s2)) by A7,Th1
.= 3_root_of_cubic(-q|^2,p|^2-r,2*p) by A8,XCMPLX_1:89;
( ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3
|^3)/64 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(
1_root_of_cubic (-q|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,
2*p)) & s3 = -q/ (s1*s2) & 1_root_of_quartic(a0,a1,a2,a3) = s1+s2+s3-a3/4)& ex
p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3|^3)/64 & r =
(256*a0 -64*a3* a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(1_root_of_cubic(-q
|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1
*s2) & 2_root_of_quartic(a0,a1,a2,a3) = -s1-s2+s3-a3/4 by A3,Def5,Def6;
hence (1_root_of_quartic(a0,a1,a2,a3)*2_root_of_quartic(a0,a1,a2,a3)+
1_root_of_quartic(a0,a1,a2,a3)*3_root_of_quartic(a0,a1,a2,a3)+
1_root_of_quartic(a0,a1,a2,a3)*4_root_of_quartic(a0,a1,a2,a3))+
2_root_of_quartic(a0,a1,a2,a3)*3_root_of_quartic(a0,a1,a2,a3)+
2_root_of_quartic(a0,a1,a2,a3)*4_root_of_quartic(a0,a1,a2,a3)+
3_root_of_quartic(a0,a1,a2,a3)*4_root_of_quartic(a0,a1,a2,a3) = -2*(s1*s1+s2*s2
+s3*s3)+3*a3*a3/8 by A4
.= -2*(-2*p)+3*a3*a3/8 by A6,A5,A9,Th17
.= 4*(8*a2-3*a3|^2)/32+3*a3*a3/8
.= 4*(8*a2-3*(a3*a3))/32+3*a3*a3/8 by Th1
.= a2;
end;
end;
theorem Th28:
(1_root_of_quartic(a0,a1,a2,a3)*2_root_of_quartic(a0,a1,a2,a3)*
3_root_of_quartic(a0,a1,a2,a3)+ 1_root_of_quartic(a0,a1,a2,a3)*
2_root_of_quartic(a0,a1,a2,a3)* 4_root_of_quartic(a0,a1,a2,a3))+
1_root_of_quartic(a0,a1,a2,a3)*3_root_of_quartic(a0,a1,a2,a3)*
4_root_of_quartic(a0,a1,a2,a3)+ 2_root_of_quartic(a0,a1,a2,a3)*
3_root_of_quartic(a0,a1,a2,a3)* 4_root_of_quartic(a0,a1,a2,a3) = -a1
proof
per cases;
suppose
A1: 8*a1 -4*a2*a3 + a3|^3 = 0;
set p = (8*a2-3*a3|^2)/32, r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/
1024, s1 = 2-root(p|^2-r);
set t1 = 2-root(-2*(p-s1)), t2 = 2-root(-2*(p+s1));
A2: ( ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2
*a2 -3*a3 |^4)/1024 & s1 = 2-root(p|^2-r) & 3_root_of_quartic(a0,a1,a2,a3) = 2
-root(-2*(p +s1))-a3/4)& ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*
a3*a1 +16*a3 |^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) & 4_root_of_quartic(a0
,a1,a2,a3) = -2-root(-2*(p+s1))-a3/4 by A1,Def7,Def8;
( ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2
*a2 -3*a3 |^4)/1024 & s1 = 2-root(p|^2-r) & 1_root_of_quartic(a0,a1,a2,a3) = 2
-root(-2*(p -s1))-a3/4)& ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*
a3*a1 +16*a3 |^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) & 2_root_of_quartic(a0
,a1,a2,a3) = -2-root(-2*(p-s1))-a3/4 by A1,Def5,Def6;
hence (1_root_of_quartic(a0,a1,a2,a3)*2_root_of_quartic(a0,a1,a2,a3)*
3_root_of_quartic(a0,a1,a2,a3)+ 1_root_of_quartic(a0,a1,a2,a3)*
2_root_of_quartic(a0,a1,a2,a3)* 4_root_of_quartic(a0,a1,a2,a3))+
1_root_of_quartic(a0,a1,a2,a3)*3_root_of_quartic(a0,a1,a2,a3)*
4_root_of_quartic(a0,a1,a2,a3)+ 2_root_of_quartic(a0,a1,a2,a3)*
3_root_of_quartic(a0,a1,a2,a3)* 4_root_of_quartic(a0,a1,a2,a3) = (-(t1*t1)+a3*
a3/16)*(-a3/2)+(-(t2*t2)+a3*a3/16)*(-a3/2) by A2
.= (-t1|^2+a3*a3/16)*(-a3/2)+(-(t2*t2)+a3*a3/16)*(-a3/2) by Th1
.= (-t1|^2+a3*a3/16)*(-a3/2)+(-t2|^2+a3*a3/16)*(-a3/2) by Th1
.= (-(-2*(p-s1))+a3*a3/16)*(-a3/2)+(-t2|^2+a3*a3/16)*(-a3/2) by Th7
.= (-(-2*(p-s1))+a3*a3/16)*(-a3/2)+(-(-2*(p+s1))+a3*a3/16)*(-a3/2) by Th7
.= (a2-3*a3|^2/8+a3*a3/8)*(-a3/2)
.= (a2-3*(a3*a3)/8+a3*a3/8)*(-a3/2) by Th1
.= a3*a3*a3/8-a2*a3/2
.= a3|^3/8-4*a2*a3/8 by Th2
.= -a1 by A1;
end;
suppose
A3: 8*a1 -4*a2*a3 + a3|^3 <> 0;
then
A4: ( ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3
|^3)/64 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(
1_root_of_cubic (-q|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,
2*p)) & s3 = -q/ (s1*s2) & 3_root_of_quartic(a0,a1,a2,a3) = -s1+s2-s3-a3/4)& ex
p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3|^3)/64 & r =
(256*a0 -64*a3* a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(1_root_of_cubic(-q
|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1
*s2) & 4_root_of_quartic(a0,a1,a2,a3) = s1-s2-s3-a3/4 by Def7,Def8;
set p = (8*a2-3*a3|^2)/32, q = (8*a1 -4*a2*a3 + a3|^3)/64, r = (256*a0 -64
*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024, s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*
p)), s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)), s3 = -q/(s1*s2);
A5: s2*s2 = s2|^2 by Th1
.= 2_root_of_cubic(-q|^2,p|^2-r,2*p) by Th7;
A6: s1*s1 = s1|^2 by Th1
.= 1_root_of_cubic(-q|^2,p|^2-r,2*p) by Th7;
then
A7: (s1*s1)*(s2*s2)*3_root_of_cubic(-q|^2,p|^2-r,2*p) = -(-q|^2) by A5,Th19;
A8: q*q <> 0 by A3;
then
A9: (s1*s1)*(s2*s2)<>0 by A7,Th1;
(s1*s2)*(s1*s2)<>0 by A8,A7,Th1;
then
A10: s1*s2<>0;
A11: s3*s3 = ((-q)/(s1*s2))*(-q/(s1*s2)) by XCMPLX_1:187
.= ((-q)/(s1*s2))*((-q)/(s1*s2)) by XCMPLX_1:187
.= (-q)*(-q)/((s1*s2)*(s1*s2)) by XCMPLX_1:76
.= (q*q)/((s1*s1)*(s2*s2))
.= 3_root_of_cubic(-q|^2,p|^2-r,2*p)*((s1*s1)*(s2*s2)) /((s1*s1)*(s2*
s2)) by A7,Th1
.= 3_root_of_cubic(-q|^2,p|^2-r,2*p) by A9,XCMPLX_1:89;
( ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3
|^3)/64 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(
1_root_of_cubic (-q|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,
2*p)) & s3 = -q/ (s1*s2) & 1_root_of_quartic(a0,a1,a2,a3) = s1+s2+s3-a3/4)& ex
p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3|^3)/64 & r =
(256*a0 -64*a3* a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(1_root_of_cubic(-q
|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1
*s2) & 2_root_of_quartic(a0,a1,a2,a3) = -s1-s2+s3-a3/4 by A3,Def5,Def6;
hence (1_root_of_quartic(a0,a1,a2,a3)*2_root_of_quartic(a0,a1,a2,a3)*
3_root_of_quartic(a0,a1,a2,a3)+ 1_root_of_quartic(a0,a1,a2,a3)*
2_root_of_quartic(a0,a1,a2,a3)* 4_root_of_quartic(a0,a1,a2,a3))+
1_root_of_quartic(a0,a1,a2,a3)*3_root_of_quartic(a0,a1,a2,a3)*
4_root_of_quartic(a0,a1,a2,a3)+ 2_root_of_quartic(a0,a1,a2,a3)*
3_root_of_quartic(a0,a1,a2,a3)* 4_root_of_quartic(a0,a1,a2,a3) = (s1*s1+s2*s2+
s3*s3)*a3-a3*a3*a3/16+8*s1*s2*s3 by A4
.= (-2*p)*a3-a3*a3*a3/16+8*s1*s2*(-q/(s1*s2)) by A6,A5,A11,Th17
.= -16*a2/32*a3+6*a3|^2/32*a3-a3*a3*a3/16-8*s1*s2*(q/(s1*s2))
.= -a2/2*a3+6*(a3*a3)/32*a3-a3*a3*a3/16-8*s1*s2*(q/(s1*s2)) by Th1
.= -a2*a3/2+2*a3*a3*a3/16-8*((s1*s2)*(q/(s1*s2)))
.= -a2*a3/2+2*a3*a3*a3/16-8*(q/((s1*s2)/(s1*s2))) by XCMPLX_1:81
.= -a2*a3/2+2*a3*a3*a3/16-8*(q/1) by A10,XCMPLX_1:60
.= -a1+2*a3*a3*a3/16-8*a3|^3/64
.= -a1+2*a3*a3*a3/16-8*(a3*a3*a3)/64 by Th2
.= -a1;
end;
end;
theorem Th29:
1_root_of_quartic(a0,a1,a2,a3)*2_root_of_quartic(a0,a1,a2,a3)*
3_root_of_quartic(a0,a1,a2,a3)*4_root_of_quartic(a0,a1,a2,a3) = a0
proof
per cases;
suppose
A1: 8*a1 -4*a2*a3 + a3|^3 = 0;
set p = (8*a2-3*a3|^2)/32, r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/
1024, s1 = 2-root(p|^2-r);
set t1 = 2-root(-2*(p-s1)), t2 = 2-root(-2*(p+s1));
A2: ( ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2
*a2 -3*a3 |^4)/1024 & s1 = 2-root(p|^2-r) & 3_root_of_quartic(a0,a1,a2,a3) = 2
-root(-2*(p +s1))-a3/4)& ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*
a3*a1 +16*a3 |^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) & 4_root_of_quartic(a0
,a1,a2,a3) = -2-root(-2*(p+s1))-a3/4 by A1,Def7,Def8;
( ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*a3*a1 +16*a3|^2
*a2 -3*a3 |^4)/1024 & s1 = 2-root(p|^2-r) & 1_root_of_quartic(a0,a1,a2,a3) = 2
-root(-2*(p -s1))-a3/4)& ex p,r,s1 st p = (8*a2-3*a3|^2)/32 & r = (256*a0 -64*
a3*a1 +16*a3 |^2*a2 -3*a3|^4)/1024 & s1 = 2-root(p|^2-r) & 2_root_of_quartic(a0
,a1,a2,a3) = -2-root(-2*(p-s1))-a3/4 by A1,Def5,Def6;
hence 1_root_of_quartic(a0,a1,a2,a3)*2_root_of_quartic(a0,a1,a2,a3)*
3_root_of_quartic(a0,a1,a2,a3)*4_root_of_quartic(a0,a1,a2,a3) = (-(t1*t1)+a3*a3
/16)*(-(t2*t2)+a3*a3/16) by A2
.= (-(t1|^2)+a3*a3/16)*(-(t2*t2)+a3*a3/16) by Th1
.= (-(t1|^2)+a3*a3/16)*(-(t2|^2)+a3*a3/16) by Th1
.= (-(-2*(p-s1))+a3*a3/16)*(-(t2|^2)+a3*a3/16) by Th7
.= (-(-2*(p-s1))+a3*a3/16)*(-(-2*(p+s1))+a3*a3/16) by Th7
.= 4*p*p+2*2*p*a3*a3/16+a3*a3*a3*a3/16/16-4*(s1*s1)
.= 4*p*p+4*p*a3*a3/16+a3*a3*a3*a3/16/16-4*(s1|^2) by Th1
.= 4*(p*p)+4*p*a3*a3/16+a3*a3*a3*a3/16/16-4*(p|^2-r) by Th7
.= 4*(p|^2)+4*p*a3*a3/16+a3*a3*a3*a3/16/16-4*(p|^2-r) by Th1
.= p*a3*a3/4+a3*a3*(a3*a3)/16/16+4*r
.= p*a3*a3/4+a3*a3*a3|^2/16/16+4*r by Th1
.= p*a3*a3/4+a3*a3*a3|^2/256+(a0-a3*a1/4+a3|^2*a2/16-3*a3|^4/256)
.= p*a3*a3/4+a3*a3*a3|^2/256+(a0-a3*a1/4+a3|^2*a2/16 -3*(a3*a3*a3*a3)/
256) by Th3
.= p*a3*a3/4+a3*a3*a3|^2/256+(a0-a3*a1/4+a3|^2*a2/16 -3*a3*a3*(a3*a3)/
256)
.= p*a3*a3/4+a3*a3*a3|^2/256+(a0-a3*a1/4+a3|^2*a2/16 -3*a3*a3*(a3|^2)/
256) by Th1
.= (a0+a2*(a3*a3)/16)-4*a3|^2*a3*a3/128-a3*a1/4+a3|^2*a2/16
.= (a0+a2*(a3|^2)/16)-a3|^2*a3*a3/32-a3*a1/4+a3|^2*a2/16 by Th1
.= a0+2*a2*a3|^2/16-a3|^2*a3*a3/32-a3*a1/4
.= a0+2*a2*(a3*a3)/16-a3|^2*a3*a3/32-a3*a1/4 by Th1
.= a0+4*a2*a3*a3/32-a3*a3*a3*a3/32-8*a3*a1/32 by Th1
.= a0+(4*a2*a3-a3*a3*a3-8*a1)*a3/32
.= a0+(4*a2*a3-a3|^3-8*a1)*a3/32 by Th2
.= a0 by A1;
end;
suppose
A3: 8*a1 -4*a2*a3 + a3|^3 <> 0;
then
A4: ( ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3
|^3)/64 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(
1_root_of_cubic (-q|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,
2*p)) & s3 = -q/ (s1*s2) & 3_root_of_quartic(a0,a1,a2,a3) = -s1+s2-s3-a3/4)& ex
p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3|^3)/64 & r =
(256*a0 -64*a3* a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(1_root_of_cubic(-q
|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1
*s2) & 4_root_of_quartic(a0,a1,a2,a3) = s1-s2-s3-a3/4 by Def7,Def8;
set p = (8*a2-3*a3|^2)/32, q = (8*a1 -4*a2*a3 + a3|^3)/64, r = (256*a0 -64
*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024, s1 = 2-root(1_root_of_cubic(-q|^2,p|^2-r,2*
p)), s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)), s3 = -q/(s1*s2);
A5: s2*s2 = s2|^2 by Th1
.= 2_root_of_cubic(-q|^2,p|^2-r,2*p) by Th7;
set r1=s1*s1, r2=s2*s2, r3=s3*s3;
A6: s1*s1 = s1|^2 by Th1
.= 1_root_of_cubic(-q|^2,p|^2-r,2*p) by Th7;
then
A7: (s1*s1)*(s2*s2)*3_root_of_cubic(-q|^2,p|^2-r,2*p) = -(-q|^2) by A5,Th19;
A8: q*q <> 0 by A3;
then (s1*s2)*(s1*s2)<>0 by A7,Th1;
then
A9: s1*s2<>0;
A10: (s1*s1)*(s2*s2)<>0 by A8,A7,Th1;
A11: s3*s3 = ((-q)/(s1*s2))*(-q/(s1*s2)) by XCMPLX_1:187
.= ((-q)/(s1*s2))*((-q)/(s1*s2)) by XCMPLX_1:187
.= (-q)*(-q)/((s1*s2)*(s1*s2)) by XCMPLX_1:76
.= (q*q)/((s1*s1)*(s2*s2))
.= 3_root_of_cubic(-q|^2,p|^2-r,2*p)*((s1*s1)*(s2*s2)) /((s1*s1)*(s2*
s2)) by A7,Th1
.= 3_root_of_cubic(-q|^2,p|^2-r,2*p) by A10,XCMPLX_1:89;
then
A12: r1+r2+r3 = -2*p by A6,A5,Th17;
( ex p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3
|^3)/64 & r = (256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(
1_root_of_cubic (-q|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,
2*p)) & s3 = -q/ (s1*s2) & 1_root_of_quartic(a0,a1,a2,a3) = s1+s2+s3-a3/4)& ex
p,q,r,s1,s2,s3 st p = (8*a2-3*a3|^2)/32 & q = (8*a1 -4*a2*a3 + a3|^3)/64 & r =
(256*a0 -64*a3* a1 +16*a3|^2*a2 -3*a3|^4)/1024 & s1 = 2-root(1_root_of_cubic(-q
|^2,p|^2-r,2*p)) & s2 = 2-root(2_root_of_cubic(-q|^2,p|^2-r,2*p)) & s3 = -q/(s1
*s2) & 2_root_of_quartic(a0,a1,a2,a3) = -s1-s2+s3-a3/4 by A3,Def5,Def6;
hence 1_root_of_quartic(a0,a1,a2,a3)*2_root_of_quartic(a0,a1,a2,a3)*
3_root_of_quartic(a0,a1,a2,a3)*4_root_of_quartic(a0,a1,a2,a3) = (r1+r2+r3)*(r1+
r2+r3)-4*(r1*r2+r1*r3+r2*r3) -(r1+r2+r3)*a3*a3/8-2*s1*s2*s3*a3+a3*a3*a3*a3/16/
16 by A4
.= (-2*p)*(-2*p)-4*(p|^2-r) -(-2*p)*a3*a3/8-2*s1*s2*s3*a3+a3*a3*a3*a3/
16/16 by A6,A5,A11,A12,Th18
.= 4*p*p-4*(p|^2-r)+2*p*a3*a3/8-2*s1*s2*s3*a3+a3*a3*a3*a3/16/16
.= 4*p*p-4*((p*p)-r)+2*p*a3*a3/8-2*s1*s2*s3*a3+a3*a3*a3*a3/16/16 by Th1
.= 4*r+2*p*a3*a3/8+2*a3*((s1*s2)*(q/(s1*s2)))+a3*a3*a3*a3/16/16
.= 4*r+2*p*a3*a3/8+2*a3*(q/((s1*s2)/(s1*s2))) +a3*a3*a3*a3/16/16 by
XCMPLX_1:81
.= 4*r+2*p*a3*a3/8+2*a3*(q/1)+a3*a3*a3*a3/16/16 by A9,XCMPLX_1:60
.= 4*(256*a0 -64*a3*a1 +16*a3|^2*a2 -3*a3|^4)/1024 +(8*a2-3*a3|^2)/32*
a3*a3/4+2*a3*(8*a1 -4*a2*a3 + a3|^3)/64 +a3*a3*a3*a3/16/16
.= 4*(256*a0 -64*a3*a1 +16*(a3*a3)*a2 -3*a3|^4)/1024 +(8*a2-3*a3|^2)/
32*a3*a3/4+2*a3*(8*a1 -4*a2*a3 + a3|^3)/64 +a3*a3*a3*a3/16/16 by Th1
.= 4*(256*a0 -64*a3*a1 +16*(a3*a3)*a2 -3*a3|^4)/1024 +(8*a2-3*(a3*a3))
/32*a3*a3/4+2*a3*(8*a1 -4*a2*a3 + a3|^3)/64 +a3*a3*a3*a3/16/16 by Th1
.= 4*(256*a0 -64*a3*a1 +16*(a3*a3)*a2 -3*(a3*a3*a3*a3))/1024 +(8*a2-3*
(a3*a3))/32*a3*a3/4+2*a3*(8*a1 -4*a2*a3 + a3|^3)/64 +(a3*a3*a3*a3/16/16) by Th3
.= 4*(256*a0 -64*a3*a1 +16*(a3*a3)*a2 -3*(a3*a3*a3*a3))/1024 +(8*a2-3*
(a3*a3))/32*a3*a3/4+2*a3*(8*a1 -4*a2*a3 + (a3*a3*a3))/64 +a3*a3*a3*a3/16/16 by
Th2
.= a0;
end;
end;
::$N The Solution of the General Quartic Equation
::$L https://en.wikipedia.org/wiki/Quartic_equation The Solution of the General Quartic Equation
theorem
a4 <> 0 implies (a4*z|^4 + a3*z|^3 + a2*z|^2 + a1*z + a0 = 0 iff z =
1_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4) or z = 2_root_of_quartic(a0/a4,a1/a4
,a2/a4,a3/a4) or z = 3_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4) or z =
4_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4))
proof
assume
A1: a4<>0;
set s4 = 4_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4);
set s3 = 3_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4);
set s2 = 2_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4);
set s1 = 1_root_of_quartic(a0/a4,a1/a4,a2/a4,a3/a4);
-a3/a4 = (s1+s2+s3+s4) by Th26;
then
A2: a3/a4 = -(s1+s2+s3+s4);
-a1/a4 = s1*s2*s3+s1*s2*s4+s1*s3*s4+s2*s3*s4 by Th28;
then
A3: a1/a4 = -(s1*s2*s3+s1*s2*s4+s1*s3*s4+s2*s3*s4);
(z|^4 + (a3/a4)*z|^3 + (a2/a4)*z|^2 + (a1/a4)*z + a0/a4)*a4 = a4*z|^4 +
(a3/a4*a4)*z|^3 + (a2/a4*a4)*z|^2 + (a1/a4*a4)*z + a0/a4*a4
.= a4*z|^4 + (a3/a4*a4)*z|^3 + (a2/a4*a4)*z|^2 + (a1/a4*a4)*z + a0 by A1,
XCMPLX_1:87
.= a4*z|^4 + (a3/a4*a4)*z|^3 + (a2/a4*a4)*z|^2 + a1*z + a0 by A1,
XCMPLX_1:87
.= a4*z|^4 + (a3/a4*a4)*z|^3 + a2*z|^2 + a1*z + a0 by A1,XCMPLX_1:87
.= a4*z|^4 + a3*z|^3 + a2*z|^2 + a1*z + a0 by A1,XCMPLX_1:87;
then
A4: z|^4 + (a3/a4)*z|^3 + (a2/a4)*z|^2 + (a1/a4)*z + a0/a4 = 0 iff a4*z|^4 +
a3*z|^3 + a2*z|^2 + a1*z + a0 = 0 by A1;
a2/a4 = s1*s2+s1*s3+s1*s4+s2*s3+s2*s4+s3*s4 & a0/a4=s1*s2*s3*s4 by Th27,Th29;
hence thesis by A4,A2,A3,Th22;
end;