:: Solving Complex Roots of Polynomial Equation of Degree 2 and 3 with
:: Complex Coefficients
:: by Yuzhong Ding and Xiquan Liang
::
:: Received January 26, 2004
:: Copyright (c) 2004-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, REAL_1, SUBSET_1, RELAT_1, ARYTM_3, SQUARE_1, COMPLEX1,
ARYTM_1, XCMPLX_0, POLYEQ_1, CARD_1, FUNCT_3, XXREAL_0, NEWTON, POWER,
NAT_1, SIN_COS, COMPTRIG, FUNCT_1, POLYEQ_3;
notations SUBSET_1, XBOOLE_0, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
FUNCT_1, REAL_1, COMPLEX1, POLYEQ_1, SQUARE_1, NEWTON, QUIN_1, POWER,
NAT_1, SIN_COS, COMPTRIG;
constructors FUNCT_4, ARYTM_0, REAL_1, SQUARE_1, NAT_1, QUIN_1, PREPOWER,
POWER, POLYEQ_1, BINARITH, SIN_COS, COMPTRIG, VALUED_1, BINOP_2, NAT_D,
XREAL_0, ABIAN, NEWTON, XCMPLX_0;
registrations XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, NEWTON, POLYEQ_1,
VALUED_0, RELSET_1, POWER, SIN_COS, QUIN_1, ORDINAL1, CARD_1;
requirements ARITHM, SUBSET, REAL, NUMERALS;
equalities POLYEQ_1, SQUARE_1, XCMPLX_0, QUIN_1;
theorems COMPLEX1, POLYEQ_1, SQUARE_1, NEWTON, COMPTRIG, NAT_1, POWER,
SIN_COS, SIN_COS2, XCMPLX_0, XCMPLX_1, XREAL_1;
schemes NAT_1, COMPTRIG;
begin
reserve a,b,c,d,a9,b9,c9,d9,y,x1,u,v for Real,
s,t,h,z,z1,z2,z3,s1,s2,s3 for Complex;
definition
let z be Element of COMPLEX;
redefine func z^2 -> Element of COMPLEX equals :: redefines ^2 (SQUARE_1, definition)
(Re z)^2-(Im z)^2 + 2*(Re z*Im z)*<i>;
compatibility
proof
z = Re z +(Im z)*<i> by COMPLEX1:13;
hence thesis;
end;
correctness by XCMPLX_0:def 2;
end;
definition
::$CD
let a,b,c,z;
redefine func Polynom (a,b,c,z) -> Element of COMPLEX; :: redefines Polynom (POLYEQ_1, definition)
coherence by XCMPLX_0:def 2;
end;
theorem Th1:
a <> 0 & delta(a,b,c) >=0 & Polynom(a,b,c,z) = 0 implies z= (-b+
sqrt delta(a,b,c))/(2*a) or z= (-b-sqrt delta(a,b,c))/(2*a) or z= -b/(2*a)
proof
A1: a = a+0*<i>;
set y=Im z;
A2: z = Re z + (Im z)*<i> by COMPLEX1:13;
set x=Re z;
assume that
A3: a <> 0 and
A4: delta(a,b,c) >= 0;
assume Polynom(a,b,c,z) = 0;
then (a+0*<i>)*(x^2-y^2+2*(x*y)*<i>)+b*z+c = 0 by A2;
then
0 = Re a*Re (x^2-y^2+(2*x*y)*<i>) -Im a*Im (x^2-y^2+2*x*y*<i>)+ (Re a*Im
(x^2-y^2+2*x*y*<i>) +Re (x^2-y^2+2*x*y*<i>)*Im a)*<i> +b*z+c by
COMPLEX1:82
.=(a*Re (x^2-y^2+2*x*y*<i>)-Im a* Im (x^2-y^2+2*x*y*<i>))+(Re a*Im (x^2-
y^2+2*x*y*<i>) +Re (x^2-y^2+2*x*y*<i>)*Im a)*<i> +b*z+c by A1,COMPLEX1:12
.=(a*(x^2-y^2)-Im a* Im (x^2-y^2+2*x*y*<i>))+(Re a*Im (x^2-y^2+2*x*y*<i>
) +Re (x^2-y^2+2*x*y*<i>)*Im a)*<i> +b*z+c by COMPLEX1:12
.=(a*(x^2-y^2)-0*Im (x^2-y^2+2*x*y*<i>) )+(Re a*Im (x^2-y^2+2*x*y*<i>)+
Re (x^2-y^2+2*x*y*<i>) *Im a )*<i> +b*z+c by A1,COMPLEX1:12
.=(a*(x^2-y^2)-0)+(Re a*(2*x*y)+Re (x^2-y^2+2*x*y*<i>) *Im a )*<i> +b*z+
c by COMPLEX1:12
.=(a*(x^2-y^2)-0)+(a*(2*x*y)+Re (x^2-y^2+2*x*y*<i>) *Im a )*<i> +b*z+c
by A1,COMPLEX1:12
.=(a*(x^2-y^2)-0)+(a*(2*x*y)+(x^2-y^2) *Im a )*<i> +b*z+c by COMPLEX1:12
.=(a*(x^2-y^2)-0)+(a*(2*x*y)+(x^2-y^2)*0)*<i> +b*z+c by A1,COMPLEX1:12;
then
A5: (a*(x^2-y^2)-0*(2*x*y))+(0+a*(2*x*y))*<i> +(b+0*<i>)*(x+y*<i>)+c = 0 by
COMPLEX1:13;
then
A6: a*(x^2-y^2)+b*x+c+(a*(2*x*y)+b*y)*<i> = 0;
then
A7: (2*a*x+b)*y = 0 by COMPLEX1:4,12;
per cases by A7;
suppose
A8: y = 0;
then Polynom(a,b,c,x)=0 by A5;
then
Re z=(-b+sqrt delta(a,b,c))/(2*a) & Im z = 0 or Re z= (-b-sqrt delta(
a,b,c))/(2*a) & Im z = 0 by A3,A4,A8,POLYEQ_1:5;
then
z=(-b+sqrt delta(a,b,c))/(2*a)+0*<i> or z= (-b-sqrt delta(a,b,c))/(2*
a)+0*<i> by COMPLEX1:13;
hence thesis;
end;
suppose
2*a*x+b = 0;
then
A9: x= (-b)/(2*a) by A3,XCMPLX_1:89;
then a*((b/(2*a))^2-y^2)+b*(-b/(2*a))+c = 0 by A6,COMPLEX1:4,12;
then (b/(2*a))^2-y^2 = (-(b*(-b/(2*a))+c))/a-0 by A3,XCMPLX_1:89;
then (b/(2*a))^2- (-(b*(-b/(2*a))+c))/a= y^2-0;
then y^2 = (b/(2*a))^2+c*a"-((b^2/(2*a))*a");
then y^2 *((2*a)^2)=(b^2/(2*a)^2+c*a"-((b^2/(2*a))*a"))*((2*a)^2) by
XCMPLX_1:76
.=b^2/((2*a)^2)*((2*a)^2)+(c*a")*(2*a)^2 -(b^2*(2*a)"*a")*(2*a)^2;
then
A10: y
^2 *((2*a)^2)=b^2+(c*a")*(2*a)^2-(b^2*((2*a)"*a"))*(2*a)^2 by A3,XCMPLX_1:87
.=b^2+(c*a")*(2*a)^2-(b^2*((2*a)*a)")*(2*a)^2 by XCMPLX_1:204
.=b^2+(c*a")*(2*a)^2-(b^2*(2*(a*a))")*(2*a)^2;
set t = (b^2*(2*(a*a))")*(2*a)^2;
t*((2*a)^2)" = b^2*(2*(a*a))"*(((2*a)^2)*(1/(2*a)^2));
then t*((2*a)^2)" = b^2*(2*(a*a))"*1 by A3,XCMPLX_1:106;
then t*((2*a)^2)"*2" = b^2*(2*a^2)"*2";
then t*((2*a)^2)"*2" = b^2*((2*a^2)"*2");
then t*((2*a)^2)"*2" = b^2*((2*(a^2*2))") by XCMPLX_1:204;
then (t*2")/(2*a)^2*(2*a)^2 = b^2/(2*a)^2*(2*a)^2;
then t*2" = b^2/(2*a)^2*(2*a)^2 by A3,XCMPLX_1:87;
then
A11: t/2 = b^2 by A3,XCMPLX_1:87;
set t=(c*a")*(2*a)^2;
t=(c/a*a)*2*(2*a);
then
A12: t=c*2*(2*a) by A3,XCMPLX_1:87;
-delta(a,b,c) <= 0 by A4;
then (y *(2*a))^2 = 0 by A10,A11,A12,XREAL_1:63;
then Im z=0 by A3;
then z = -b/(2*a)+0*<i> by A9,COMPLEX1:13;
hence thesis;
end;
end;
theorem Th2:
a <> 0 & delta(a,b,c) < 0 & Polynom(a,b,c,z) = 0 implies z= -b/(2
*a)+(sqrt (-delta(a,b,c))/(2*a))*<i> or z= -b/(2*a)+(-sqrt (-delta(a,b,c))/(2*a
))*<i>
proof
assume that
A1: a <> 0 and
A2: delta(a,b,c) < 0;
A3: a= a+0*<i>;
now
set t2=(-b^2+c*a*4)/4;
let z;
set x=Re z;
set y=Im z;
A4: z = x + y*<i> by COMPLEX1:13;
assume Polynom(a,b,c,z) = 0;
then (a+0*<i>)*(x^2-y^2+(2*x*y)*<i>)+b*z+c = 0 by A4;
then
Re a*Re (x^2-y^2+2*x*y*<i>)-Im a*Im (x^2-y^2+(2*x*y)*<i>) +(Re a*Im (x
^2-y^2+2*x*y*<i>)+Re (x^2-y^2+2*x*y*<i>) *Im a)*<i>+b*z+c = 0 by
COMPLEX1:82;
then
(a*Re (x^2-y^2+2*x*y*<i>)-Im a*Im (x^2-y^2+2*x*y*<i>) )+(Re a*Im (x^2-
y^2+2*x*y*<i>)+Re (x^2-y^2+2*x*y*<i>) *Im a)*<i>+b*z+c = 0 by A3,COMPLEX1:12;
then (a*(x^2-y^2)-Im a*Im (x^2-y^2+2*x*y*<i>) )+(Re a*Im (x^2-y^2+2*x*y*
<i>)+Re (x^2-y^2+2*x*y*<i>) *Im a)*<i>+b*z+c = 0 by COMPLEX1:12;
then
(a*(x^2-y^2)-0*Im (x^2-y^2+2*x*y*<i>) )+(Re a*Im (x^2-y^2+2*x*y*<i>)+
Re (x^2-y^2+2*x*y*<i>) *Im a)*<i>+b*z+c = 0 by A3,COMPLEX1:12;
then
(a*(x^2-y^2)-0)+(Re a*(2*x*y)+Re (x^2-y^2+2*x*y*<i>) *Im a)*<i>+b*z+c
= 0 by COMPLEX1:12;
then (a*(x^2-y^2)-0)+(a*(2*x*y)+Re (x^2-y^2+2*x*y*<i>) *Im a)*<i>+b*z+c =
0 by A3,COMPLEX1:12;
then (a*(x^2-y^2)-0)+(a*(2*x*y)+(x^2-y^2) *Im a)*<i>+b*z+c = 0 by
COMPLEX1:12;
then (a*(x^2-y^2)-0)+(a*(2*x*y)+(x^2-y^2) *0)*<i>+b*z+c = 0 by A3,
COMPLEX1:12;
then (a*(x^2-y^2)-0*(2*x*y))+((x^2-y^2)*0+a*(2*x*y))*<i> +(b+0*<i>)*(x+y*
<i>)+c = 0 by COMPLEX1:13;
then
A5: a*(x^2-y^2)+b*x+c+(a*(2*x*y)+b*y)*<i> = 0;
then (a*(2*x))*y+b*y = 0 by COMPLEX1:4,12;
then
A6: (a*2*x)*y = (-b)*y;
set t = (b^2*(2*(a*a))")*(2*a)^2;
set t1= (x*a+b/2)^2;
0-delta(a,b,c)>0 by A2;
then
A7: 0+0<t1+t2 by XREAL_1:8,63;
-a*y^2+((b*x+a*x^2)+c )+a*y^2= 0+a*y^2 by A5,COMPLEX1:4,12;
then a*x^2*a+b*x*a+c*a = a*y^2*a by XCMPLX_1:9;
then y<>0 by A7;
then a*(2*x) = -b by A6,XCMPLX_1:5;
then 2*x = (-b)/a by A1,XCMPLX_1:89;
then x = 1/a*((-b)/2);
then
A8: x = (-b)/(2*a) by XCMPLX_1:103;
then a*((b/(2*a))^2-y^2)+b*(-b/(2*a))+c = 0 by A5,COMPLEX1:4,12;
then (b/(2*a))^2-y^2 = (-(b*(-b/(2*a))+c))/a-0 by A1,XCMPLX_1:89;
then (b/(2*a))^2- (-(b*(-b/(2*a))+c))/a= y^2-0;
then y^2 = (b/(2*a))^2+c*a"-((b^2/(2*a))*a");
then y^2 *((2*a)^2)=(b^2/(2*a)^2+c*a"-((b^2/(2*a))*a"))*((2*a)^2) by
XCMPLX_1:76
.=b^2/((2*a)^2)*((2*a)^2)+(c*a")*(2*a)^2 -(b^2*(2*a)"*a")*(2*a)^2;
then
A9: y
^2 *((2*a)^2)=b^2+(c*a")*(2*a)^2-(b^2*((2*a)"*a"))*(2*a)^2 by A1,XCMPLX_1:87
.=b^2+(c*a")*(2*a)^2-(b^2*((2*a)*a)")*(2*a)^2 by XCMPLX_1:204
.=b^2+(c*a")*(2*a)^2-(b^2*(2*(a*a))")*(2*a)^2;
t*((2*a)^2)" = b^2*(2*(a*a))"*(((2*a)^2)*(1/(2*a)^2));
then t*((2*a)^2)" = b^2*(2*(a*a))"*1 by A1,XCMPLX_1:106;
then t*((2*a)^2)"*2" = b^2*(2*a^2)"*2";
then t*((2*a)^2)"*2" = b^2*((2*a^2)"*2");
then t*((2*a)^2)"*2" = b^2*((2*(a^2*2))") by XCMPLX_1:204;
then (t*2")/(2*a)^2*(2*a)^2 = b^2/(2*a)^2*(2*a)^2;
then t*2" = b^2/(2*a)^2*(2*a)^2 by A1,XCMPLX_1:87;
then
A10: t/2 = b^2 by A1,XCMPLX_1:87;
set t=(c*a")*(2*a)^2;
t=(c/a*a)*2*(2*a);
then t=c*2*(2*a) by A1,XCMPLX_1:87;
then (y *(2*a))^2 =(sqrt (-delta(a,b,c)))^2 by A2,A9,A10,SQUARE_1:def 2;
then
((y *(2*a))+(sqrt (-delta(a,b,c))))* ((y *(2*a))-(sqrt (-delta(a,b,c)
)))=0;
then
((y *(2*a))+(sqrt (-delta(a,b,c))))=0 or ((y *(2*a))-(sqrt (-delta(a,
b,c))))=0;
then
y =(-sqrt (-delta(a,b,c)))/(2*a) or y *(2*a)/(2*a)=sqrt (-delta(a,b,c
))/(2*a) by A1,XCMPLX_1:89;
then Re z=-b/(2*a) & Im z=sqrt (-delta(a,b,c))/(2*a) or Re z= -b/(2*a) &
Im z= -sqrt (-delta(a,b,c))/(2*a) by A1,A8,XCMPLX_1:89;
hence z= -b/(2*a)+(sqrt(-delta(a,b,c))/(2*a))*<i> or z= -b/(2*a)+(-sqrt (-
delta(a,b,c))/(2*a))*<i> by COMPLEX1:13;
end;
hence thesis;
end;
theorem
b <> 0 & (for z holds Polynom(0,b,c,z) = 0) implies z = -c/b
proof
A1: 0 = 0+0*<i>;
assume
A2: b <> 0;
assume
A3: for z holds Polynom(0,b,c,z) = 0;
now
let z1;
Polynom(0,b,c,z1) = 0 by A3;
then b*(Re z1+(Im z1)*<i>)+c = 0 by COMPLEX1:13;
then
A4: (b*Re z1-0+c+(b*Im z1+0)*<i>)= 0+0*<i>;
then b*Re z1-0+c = Re 0 by COMPLEX1:12;
then b*(Re z1)-0+c = 0 by A1,COMPLEX1:12;
then
A5: Re z1 =(-c)/b by A2,XCMPLX_1:89;
b*Im z1= Im 0 by A4,COMPLEX1:12;
then Im z1 = 0 by A1,A2,COMPLEX1:12;
then z1 = -c/b+0*<i> by A5,COMPLEX1:13;
hence z1 = -c/b;
end;
hence thesis;
end;
theorem
for a,b,c being Real,z,z1,z2 being Complex st a <> 0 & for z
being Complex holds Polynom(a,b,c,z) = Quard(a,z1,z2,z) holds b/a =-(z1+
z2) & c/a = z1*z2
proof
let a,b,c be Real,z,z1,z2 be Complex;
assume
A1: a <> 0;
assume
A2: for z being Complex holds Polynom(a,b,c,z) = Quard(a,z1,z2,z);
then
A3: Polynom(a,b,c,0) = Quard(a,z1,z2,0);
Quard(a,z1,z2,1) = Polynom(a,b,c,1) by A2
.=a+b+c;
then a+b+c =a+a*(-(z1+z2))+c by A3;
hence thesis by A1,A3,XCMPLX_1:203;
end;
definition
let z be Complex;
func z^3 -> Element of COMPLEX equals
z^2*z;
correctness by XCMPLX_0:def 2;
end;
Lm1: for z be Complex holds z|^2= z*z
proof
let z be Complex;
z|^(1+1) = (z|^1)*z by NEWTON:6
.= z*z;
hence thesis;
end;
definition
let a,b,c,d,z be Complex;
redefine func Polynom(a,b,c,d,z) equals :: redefines Polynom (POLYEQ_1, definition)
a*z^3 + b*z^2 + c*z + d;
compatibility
proof
let x be set;
Polynom(a,b,c,d,z) = a*(z |^(2+1))+ b*z^2 +c*z +d
.= a*((z |^2)*z)+ b*z^2 +c*z +d by NEWTON:6;
hence thesis by Lm1;
end;
end;
theorem Th5:
Re z^3 = (Re z)|^3 - 3*Re z*(Im z)^2 & Im z^3 = -(Im z)|^ 3+3*( Re z)^2*Im z
proof
set x = Re z;
set y = Im z;
Re z + (Im z)*<i> = z by COMPLEX1:13;
then
z^3 = Re(x^2-y^2+(2*(x*y))*<i>) *Re (x+y*<i>)-Im(x^2-y^2+(2*(x*y))*<i>)
*Im (x+y*<i>)+(Re(x^2-y^2+(2*(x*y))*<i>) *Im (x+y*<i>)+ Re (x+y*<i>)*Im (x^2-y
^2+(2*(x*y))*<i>))*<i> by COMPLEX1:82
.= ((x^2-y^2) *Re (x+y*<i>)-Im(x^2-y^2+(2*(x*y))*<i>) *Im (x+y*<i>))+(Re
(x^2-y^2+(2*(x*y))*<i>) *Im (x+y*<i>)+ Re (x+y*<i>)*Im (x^2-y^2+(2*(x*y))*<i>))
*<i> by COMPLEX1:12
.= ((x^2-y^2) *Re (x+y*<i>)-(2*(x*y)) *Im (x+y*<i>))+(Re(x^2-y^2+(2*(x*y
))*<i>) *Im (x+y*<i>)+ Re (x+y*<i>)*Im (x^2-y^2+(2*(x*y))*<i>))*<i> by
COMPLEX1:12
.= ((x^2-y^2) *Re (x+y*<i>)-(2*(x*y)) *Im (x+y*<i>))+((x^2-y^2) *Im (x+y
*<i>)+ Re (x+y*<i>)*Im (x^2-y^2+(2*(x*y))*<i>))*<i> by COMPLEX1:12
.= ((x^2-y^2) *Re (x+y*<i>)-(2*(x*y))*Im (x+y*<i>) )+((x^2-y^2) *Im (x+y
*<i>)+Re (x+y*<i>)*(2*(x*y)))*<i> by COMPLEX1:12
.= ((x^2-y^2) *x-(2*(x*y))*Im (x+y*<i>) )+((x^2-y^2) *Im (x+y*<i>)+Re (x
+y*<i>)*(2*(x*y)))*<i> by COMPLEX1:12
.= ((x^2-y^2) *x-(2*(x*y))*y )+((x^2-y^2) *Im (x+y*<i>)+Re (x+y*<i>)*(2*
(x*y)))*<i> by COMPLEX1:12
.= ((x^2-y^2) *x-(2*(x*y))*y )+((x^2-y^2) *y+Re (x+y*<i>)*(2*(x*y)))*<i>
by COMPLEX1:12
.= ((x^2*x-y^2*x+0*x)-2*(x*y)*y)+((x^2-y^2+0)*y+x*(2*(x*y)))*<i> by
COMPLEX1:12
.= ((x|^1*x*x-y^2*x)-2*(x*y)*y)+((x^2*y-y^2*y)+x*(2*(x*y)))*<i>
.= ((x|^ (1+1)*x-y^2*x)-2*(x*y)*y)+((x^2*y-y^2*y)+x*(2*(x*y)))*<i> by
NEWTON:6
.= ((x|^(2+1)-y^2*x)-2*(x*y)*y)+((x^2*y-y^2*y)+x*(2*(x*y)))*<i> by NEWTON:6
.= ((x|^ 3-y^2*x)-2*(x*y)*y)+((x^2*y-y|^ 1*y*y)+x*(2*(x*y)))*<i>
.= ((x|^ 3-y^2*x)-2*(x*y)*y)+((x^2*y-y|^ (1+1)*y)+x*(2*(x*y)))*<i> by
NEWTON:6
.= ((x|^ 3-y^2*x)-2*(x*(y*y)))+((x^2*y-y|^ (2+1))+x*(2*(x*y)))*<i> by
NEWTON:6
.= (x|^ 3-3*x*y^2 )+(-y|^ 3+3*x^2*y)*<i>;
hence thesis by COMPLEX1:12;
end;
theorem
(for z being Complex holds Polynom(a,b,c,d,z) = Polynom(a9,b9,
c9,d9,z ) ) implies a = a9 & b = b9 & c = c9 & d = d9
proof
assume
A1: for z being Complex holds Polynom(a,b,c,d,z) = Polynom(a9,b9,
c9,d9,z);
then
A2: Polynom(a,b,c,d,0) = Polynom(a9,b9,c9,d9,0);
A3: Polynom(a,b,c,d,1) = Polynom(a9,b9,c9,d9,1) & Polynom(a,b,c,d,-1) =
Polynom( a9,b9,c9,d9,-1) by A1;
A4: Polynom(a,b,c,d,2) = Polynom(a9,b9,c9,d9,2) by A1;
hence a = a9 by A2,A3;
thus b = b9 by A2,A3;
thus c = c9 by A2,A3,A4;
thus thesis by A2;
end;
theorem
b<>0 & delta(b,c,d)>=0 & Polynom(0,b,c,d,z)=0 implies z = (-c+sqrt
delta(b,c,d))/(2*b) or z = (-c-sqrt delta(b,c,d))/(2*b) or z = -c/(2*b)
proof
assume that
A1: b<>0 & delta(b,c,d)>=0 and
A2: Polynom(0,b,c,d,z)=0;
Polynom(b,c,d,z)=0 by A2;
hence thesis by A1,Th1;
end;
theorem
b<>0 & delta(b,c,d)<0 & Polynom(0,b,c,d,z)=0 implies z = -c/(2*b)+(
sqrt (-delta(b,c,d))/(2*b))*<i> or z = -c/(2*b)+(-sqrt (-delta(b,c,d))/(2*b))*
<i>
proof
assume that
A1: b<>0 & delta(b,c,d)<0 and
A2: Polynom(0,b,c,d,z)=0;
Polynom(b,c,d,z)=0 by A2;
hence thesis by A1,Th2;
end;
theorem
a<>0 & 4*a*c <= 0 & Polynom(a,0,c,0,z)=0 implies z = (sqrt -4*a*c)/(2*
a) or z = (-sqrt -4*a*c)/(2*a) or z = 0
proof
assume that
A1: a<>0 & 4*a*c <= 0 and
A2: Polynom(a,0,c,0,z)=0;
(a*z^2+c)*z = 0 by A2;
then Polynom(a,0,c,z) = 0 or z = 0;
then
z = (-0+sqrt delta(a,0,c))/(2*a) or z = (-0-sqrt delta(a,0,c))/(2*a) or
z = 0 or z = 0/(2*a) by A1,Th1;
hence thesis;
end;
theorem
a<>0 & delta(a,b,c)>=0 & Polynom(a,b,c,0,z)=0 implies z = (-b+sqrt
delta(a,b,c))/(2*a) or z = (-b-sqrt delta(a,b,c))/(2*a) or z = -b/(2*a) or z =
0
proof
assume that
A1: a<>0 & delta(a,b,c)>=0 and
A2: Polynom(a,b,c,0,z)=0;
(a*z^2+b*z+c)*z = 0 by A2;
then Polynom(a,b,c,z) = 0 or z = 0;
hence thesis by A1,Th1;
end;
theorem
a<>0 & delta(a,b,c)<0 & Polynom(a,b,c,0,z)=0 implies z= -b/(2*a)+(sqrt
(-delta(a,b,c))/(2*a))*<i> or z= -b/(2*a)+(-sqrt (-delta(a,b,c))/(2*a))*<i> or
z = 0
proof
assume that
A1: a<>0 & delta(a,b,c)<0 and
A2: Polynom(a,b,c,0,z)=0;
(a*z^2+b*z+c)*z = 0 by A2;
then Polynom(a,b,c,z) = 0 or z = 0;
hence thesis by A1,Th2;
end;
theorem Th12:
y^2 = a implies y = sqrt a or y = -sqrt a
proof
assume
A1: y^2 = a;
then
A2: a >= 0 by XREAL_1:63;
Polynom(1,0,-a,y) =0 by A1;
then y=(-0+sqrt delta(1,0,-a))/(2*1) or y=(-0-sqrt delta(1,0,-a))/(2*1) by A2
,POLYEQ_1:5;
then y=(sqrt (4*a))/2 or y=(0-sqrt (4*a))/2;
then y= sqrt a * 2 /2 or y=(-(2 * sqrt a))/2 by A2,SQUARE_1:20,29;
hence thesis;
end;
theorem
a<>0 & Im z = 0 & Polynom(a,0,c,d,z)=0 implies for u,v st Re z = u+v &
3*v*u+c/a=0 holds z = 3-root(-d/(2*a)+sqrt(d^2/(4*a^2)+(c/(3*a)) |^ 3)) +3-root
(-d/(2*a)-sqrt(d^2/(4*a^2)+(c/(3*a)) |^ 3)) or z = 3-root(-d/(2*a)+sqrt(d^2/(4*
a^2)+(c/(3*a)) |^ 3)) +3-root(-d/(2*a)+sqrt(d^2/(4*a^2)+(c/(3*a)) |^ 3)) or z =
3-root(-d/(2*a)-sqrt(d^2/(4*a^2)+(c/(3*a)) |^ 3)) +3-root(-d/(2*a)-sqrt(d^2/(4*
a^2)+(c/(3*a)) |^ 3))
proof
assume
A1: a <> 0;
set y=Im z;
set x=Re z;
assume that
A2: Im z = 0 and
A3: Polynom(a,0,c,d,z)=0;
A4: a = a+0*<i>;
0 = a*(Re z^3+(Im z^3)*<i>)+0*z^2+c*z+d by A3,COMPLEX1:13
.= a*(((Re z)|^ 3 - 3*Re z*(Im z)^2)+(Im z^3)*<i>) +0*z^2+c*z+d by Th5
.= a*(((Re z)|^ 3 - 3*Re z*(Im z)^2)+(-(Im z)|^ 3+3*(Re z)^2 *Im z)*<i>)
+c*z+d by Th5
.= (a+0*<i>)*((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>) +c*(Re z+Im z*<i>)
+d by COMPLEX1:13
.=Re a *Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)-Im a *Im((x|^ 3 - 3*x
*y^2)+(-y|^ 3+3*x^2*y)*<i>)+(Re a *Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)+
Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)*Im a)*<i> +c*(Re z+Im z*<i>)+d by
COMPLEX1:82
.=(Re a *(x|^ 3 - 3*x*y^2)-Im a *Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*
<i>))+(Re a *Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)+ Re((x|^ 3 - 3*x*y^2)+(
-y|^ 3+3*x^2*y)*<i>)*Im a )*<i> +c*(Re z+Im z *<i>)+d by COMPLEX1:12
.=(Re a *(x|^ 3 - 3*x*y^2)-Im a*(-y|^ 3+3*x^2*y))+(Re a *Im((x|^ 3 - 3*x
*y^2)+(-y|^ 3+3*x^2*y)*<i>)+ Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)*Im a )*
<i> +c*(Re z+Im z *<i>)+d by COMPLEX1:12
.=(Re a *(x|^ 3 - 3*x*y^2)-Im a*(-y|^ 3+3*x^2*y))+(Re a *Im((x|^ 3 - 3*x
*y^2)+(-y|^ 3+3*x^2*y)*<i>)+ (x|^ 3 - 3*x*y^2)*Im a )*<i> +c*(Re z+Im z *<i>)+d
by COMPLEX1:12
.=(Re a *(x|^ 3 - 3*x*y^2)-Im a *(-y|^ 3+3*x^2*y))+(Re a*(-y|^ 3+3*x^2*y
)+ (x|^ 3 - 3*x*y^2)*Im a )*<i> +c*(Re z+Im z *<i>)+d by COMPLEX1:12
.=(a*(x|^ 3 - 3*x*y^2)-Im a *(-y|^ 3+3*x^2*y))+(Re a*(-y|^ 3+3*x^2*y)+ (
x|^ 3 - 3*x*y^2)*Im a )*<i> +c*(Re z+Im z *<i>)+d by A4,COMPLEX1:12
.=(a*(x|^ 3 - 3*x*y^2)-0*(-y|^ 3+3*x^2*y))+( Re a*(-y|^ 3+3*x^2*y)+(x|^
3 - 3*x*y^2)*Im a )*<i> +c*(Re z+Im z *<i>)+d by A4,COMPLEX1:12
.=(a*(x|^ 3 - 3*x*y^2)-0)+(a*(-y|^ 3+3*x^2*y) +(x|^ 3 - 3*x*y^2)*Im a )*
<i> +c*(Re z+Im z *<i>)+d by A4,COMPLEX1:12
.=(a*(x|^ 3 - 3*x*y^2)-0)+(a*(-y|^ 3+3*x^2*y) +(x|^ 3 - 3*x*y^2)*0 )*<i>
+c*(Re z+Im z *<i>)+d by A4,COMPLEX1:12
.= a*(x|^ 3 - 0)+c*x+d+(a*(-0))*<i> by A2,NEWTON:11
.= a*x|^ 3 +c*x+d;
then a"*(a*x|^ 3+c*x+d) = a"*0;
then x|^ 3*(a/a)+a"*c*x+a"*d = 0;
then
A5: Polynom(1,0,c/a,d/a,x) = 0 by A1,XCMPLX_1:88;
A6: (d/a)^2/4 =1/4*(d^2/a^2) by XCMPLX_1:76
.=d^2/(a^2*4) by XCMPLX_1:103;
let u,v;
assume
A7: Re z=u+v & 3*v*u+c/a=0;
A8: -(d/a)/2 = -1/2*(d/a) .= -d/(a*2) by XCMPLX_1:103;
A9: (c/a)/3 =1/3*(c/a) .=c/(a*3) by XCMPLX_1:103;
z = Re z+(Im z)*<i> by COMPLEX1:13
.= x by A2;
hence thesis by A7,A5,A8,A6,A9,POLYEQ_1:19;
end;
theorem
a<>0 & Im z <> 0 & Polynom(a,0,c,d,z)=0 implies for u,v st Re z = u+v
& 3*v*u+c/(4*a)=0 holds z=3-root(d/(16*a)+sqrt((d/(16*a))^2+(c/(12*a)) |^ 3)) +
3-root(d/(16*a)-sqrt((d/(16*a))^2+(c/(12*a)) |^ 3))+ sqrt(3*(3-root(d/(16*a)+
sqrt((d/(16*a))^2+(c/(12*a)) |^ 3)) + 3-root(d/(16*a)-sqrt((d/(16*a))^2+(c/(12*
a)) |^ 3)))^2+c/a)*<i> or z=3-root(d/(16*a)+sqrt((d/(16*a))^2+(c/(12*a)) |^ 3))
+3-root(d/(16*a)-sqrt((d/(16*a))^2+(c/(12*a)) |^ 3)) -sqrt(3*(3-root(d/(16*a)+
sqrt((d/(16*a))^2+(c/(12*a)) |^ 3)) +3-root(d/(16*a)-sqrt((d/(16*a))^2+(c/(12*a
)) |^ 3)))^2+c/a)*<i> or z=2*(3-root(d/(16*a)+sqrt((d/(16*a))^2+(c/(12*a)) |^ 3
)))+ sqrt(3*(2*(3-root(d/(16*a)+sqrt((d/(16*a))^2 +(c/(12*a)) |^ 3))))^2+c/a)*
<i> or z=2*(3-root(d/(16*a)+sqrt((d/(16*a))^2+(c/(12*a)) |^ 3))) -sqrt(3*(2*(3
-root(d/(16*a)+sqrt((d/(16*a))^2 +(c/(12*a)) |^ 3))))^2+c/a)*<i> or z=2*(3-root
(d/(16*a)-sqrt((d/(16*a))^2+(c/(12*a)) |^ 3)))+ sqrt(3*(2*(3-root(d/(16*a)-sqrt
((d/(16*a))^2 +(c/(12*a)) |^ 3))))^2+c/a)*<i> or z=2*(3-root(d/(16*a)-sqrt((d/(
16*a))^2+(c/(12*a)) |^ 3))) -sqrt(3*(2*(3-root(d/(16*a)-sqrt((d/(16*a))^2 +(c/(
12*a)) |^ 3))))^2+c/a)*<i>
proof
assume
A1: a <> 0;
set y=Im z;
set x=Re z;
assume that
A2: Im z <> 0 and
A3: Polynom(a,0,c,d,z)=0;
A4: a = a+0*<i>;
A5: 0 = a*(Re z^3+(Im z^3)*<i>)+0*z^2+c*z+d by A3,COMPLEX1:13
.= a*(((Re z)|^ 3 - 3*Re z*(Im z)^2)+(Im z^3)*<i>) +c*z+d by Th5
.= a*(((Re z)|^ 3 - 3*Re z*(Im z)^2)+(-(Im z)|^ 3+3*(Re z)^2 *Im z)*<i>)
+c*z+d by Th5
.= (a+0*<i>)*((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>) +c*(Re z+(Im z)*
<i>)+d by COMPLEX1:13
.=Re a *Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)-Im a *Im((x|^ 3 - 3*x
*y^2)+(-y|^ 3+3*x^2*y)*<i>)+(Re a *Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)+
Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)*Im a)*<i> +c*(Re z+Im z *<i>)+d
by COMPLEX1:82
.=(Re a *(x|^ 3 - 3*x*y^2)-Im a *Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*
<i>))+(Re a *Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)+ Re((x|^ 3 - 3*x*y^2)+(
-y|^ 3+3*x^2*y)*<i>)*Im a )*<i> +c*(Re z+Im z *<i>)+d by COMPLEX1:12
.=(Re a *(x|^ 3 - 3*x*y^2)-Im a *(-y|^ 3+3*x^2*y))+(Re a *Im((x|^ 3 - 3*
x*y^2)+(-y|^ 3+3*x^2*y)*<i>)+ Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)*Im a )
*<i> +c*(Re z+Im z *<i>)+d by COMPLEX1:12
.=(Re a *(x|^ 3 - 3*x*y^2)-Im a *(-y|^ 3+3*x^2*y))+(Re a *Im((x|^ 3 - 3*
x*y^2)+(-y|^ 3+3*x^2*y)*<i>)+ (x|^ 3 - 3*x*y^2)*Im a )*<i> +c*(Re z+Im z *<i>)+
d by COMPLEX1:12
.=(Re a *(x|^ 3 - 3*x*y^2)-Im a *(-y|^ 3+3*x^2*y))+(Re a*(-y|^ 3+3*x^2*y
)+ (x|^ 3 - 3*x*y^2)*Im a )*<i> +c*(Re z+Im z *<i>)+d by COMPLEX1:12
.=(a*(x|^ 3 - 3*x*y^2)-Im a *(-y|^ 3+3*x^2*y))+(Re a*(-y|^ 3+3*x^2*y)+ (
x|^ 3 - 3*x*y^2)*Im a)*<i> +c*(Re z+Im z *<i>)+d by A4,COMPLEX1:12
.=(a*(x|^ 3 - 3*x*y^2)-0*(-y|^ 3+3*x^2*y))+( Re a*(-y|^ 3+3*x^2*y)+(x|^
3 - 3*x*y^2)*Im a )*<i> +c*(Re z+Im z *<i>)+d by A4,COMPLEX1:12
.=(a*(x|^ 3 - 3*x*y^2)-0)+(a*(-y|^ 3+3*x^2*y) +(x|^ 3 - 3*x*y^2)*Im a )*
<i> +c*(Re z+Im z *<i>)+d by A4,COMPLEX1:12
.=(a*(x|^ 3 - 3*x*y^2)-0)+(a*(-y|^ 3+3*x^2*y) +(x|^ 3 - 3*x*y^2)*0 )*<i>
+c*(Re z+Im z *<i>)+d by A4,COMPLEX1:12
.= a*(x|^ 3 - 3*x*y^2)+c*x+d+(a*(-y|^ 3+3*x^2*y) +c*y+0)*<i>;
then a*(-y|^(2+1)+3*x^2*y)+c*y = 0 by COMPLEX1:4,12;
then a*(-y|^2*y+3*x^2*y)+c*y = 0 by NEWTON:6;
then (a*(-y|^2+3*x^2)+c+0)*y = 0;
then (a*(y|^2))+(-a*(y|^2)+(a*(3*x^2)+c))=(a*(y|^2))+0 by A2,XCMPLX_1:6;
then y|^(1+1) = (a*(3*x^2)+c)/a by A1,XCMPLX_1:89;
then y|^1*y = (a*(3*x^2)+c)/a by NEWTON:6;
then
A6: y^2 = (3*x^2)*a/a+c/a+0/a;
then
A7: z = x+y*<i> & y^2 = 3*x^2+c/a+0*a" by A1,COMPLEX1:13,XCMPLX_1:89;
set q = -d/(8*a);
set pp = c/(4*a);
let u,v;
set m = 3-root(-q/2+sqrt(q^2/4+(pp/3) |^ 3));
set n = 3-root(-q/2-sqrt(q^2/4+(pp/3) |^ 3));
A8: (c/(4*a))/3=1/3*(c/(4*a)) .=c/(a*4*3) by XCMPLX_1:103
.=c/(a*(4*3));
-q/2=1/2*(d/(8*a));
then
A9: -q/2=d/(a*8*2) by XCMPLX_1:103;
a*(-y|^ 3+3*x^2*y) +c*y+0 = 0 by A5,COMPLEX1:4,12;
then a*(x|^ 3 - 3*x*(3*x^2+c/a)+0)+c*x+d = 0 by A1,A5,A6,XCMPLX_1:89;
then 0 =a*x|^ 3 - a*(9*(x*x^2)+(3*x)*(c/a))+c*x+d
.=a*x|^ 3 - a*(9*(x|^1*x*x)+(3*x)*(c/a))+c*x+d
.=a*x|^ 3 - a*(9*(x|^(1+1)*x)+(3*x)*(c/a))+c*x+d by NEWTON:6
.=a*x|^ 3 - a*(9*(x|^(2+1))+(3*x)*(c/a)+0)+c*x+d by NEWTON:6
.=a*x|^ 3 - (a*(9*(x|^3))+(3*x)*(c*(a/a)))+c*x+d
.=a*x|^ 3 - (a*(9*(x|^3))+(3*x)*c)+c*x+d by A1,XCMPLX_1:88
.=(-8*a)*x|^3+(-2*c)*x+d;
then (-1)*0=(8*a)*x|^3+(2*c)*x+(-d);
then 0=x|^3*((8*a)/(8*a))+(8*a)"*((2*c)*x)+(8*a)"*(-d);
then 0=1*x|^3+0*x^2+((2*c)/(8*a))*x+((8*a)"*(-d)) by A1,XCMPLX_1:88;
then 0=1*x|^3+0*x^2+((2/8*c)/a)*x+((-d)/(8*a)) by XCMPLX_1:83;
then 0=1*x|^3+0*x^2+(1/a*(c/4))*x+((-d)/(8*a));
then
A10: Polynom(1,0,c/(4*a),-d/(8*a),x) = 0 by XCMPLX_1:103;
assume Re z=u+v & 3*v*u+c/(4*a)=0;
then
A11: x = 3-root(-q/2+sqrt(q^2/4+(pp/3) |^ 3)) + 3-root(-q/2-sqrt(q^2/4+(pp/3
) |^ 3)) or x = 3-root(-q/2+sqrt(q^2/4+(pp/3) |^ 3)) + 3-root(-q/2+sqrt(q^2/4+(
pp/3) |^ 3)) or x = 3-root(-q/2-sqrt(q^2/4+(pp/3) |^ 3)) + 3-root(-q/2-sqrt(q^2
/4+(pp/3) |^ 3)) by A10,POLYEQ_1:19;
A12: now
per cases by A11;
case
x = m + n;
hence
z=m+n+sqrt(3*(m + n )^2+c/a)*<i> or z=m+n+(-sqrt(3*(m + n )^2+c/a))
*<i> by A7,Th12;
end;
case
x = 2*m;
hence z=2*m+sqrt(3*(2*m)^2+c/a)*<i> or z=2*m+(-sqrt(3*(2*m)^2+c/a))*<i>
by A7,Th12;
end;
case
x = 2*n;
hence
z=2*n+sqrt(3*(2*n )^2+c/a)*<i> or z=2*n+(-sqrt(3*(2*n )^2+c/a))*<i>
by A7,Th12;
end;
end;
q^2/4=(1/2*(d/(8*a)))^2;
hence thesis by A9,A12,A8;
end;
theorem
a<>0 & Polynom(a,b,c,d,z)=0 & Im z=0 implies for u,v,x1 st x1=Re z + b
/(3*a) & Re z=u+v-b/(3*a) & 3*u*v+(3*a*c-b^2)/(3*a^2)=0 holds z =3-root(-(b/(3*
a)) |^ 3-(3*a*d-b*c)/(6*a^2) +sqrt((2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2))^2/4
+((3*a*c-b^2)/(9*a^2)) |^ 3)) + 3-root(-(b/(3*a)) |^ 3-(3*a*d-b*c)/(6*a^2) -
sqrt((2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2))^2/4 +((3*a*c-b^2)/(9*a^2)) |^ 3))
-b/(3*a)+0*<i> or z =3-root(-(b/(3*a)) |^ 3-(3*a*d-b*c)/(6*a^2) +sqrt((2*((b/(3
*a)) |^ 3)+(3*a*d-b*c)/(3*a^2))^2/4 +((3*a*c-b^2)/(9*a^2)) |^ 3)) + 3-root(-(b/
(3*a)) |^ 3-(3*a*d-b*c)/(6*a^2) +sqrt((2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2))
^2/4 +((3*a*c-b^2)/(9*a^2)) |^ 3))-b/(3*a)+0*<i> or z =3-root(-(b/(3*a)) |^ 3-(
3*a*d-b*c)/(6*a^2) -sqrt((2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2))^2/4 +((3*a*c-
b^2)/(9*a^2)) |^ 3)) + 3-root(-(b/(3*a)) |^ 3-(3*a*d-b*c)/(6*a^2) -sqrt((2*((b/
(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2))^2/4 +((3*a*c-b^2)/(9*a^2)) |^ 3))-b/(3*a)+0*
<i>
proof
assume
A1: a<>0;
set p = (3*a*c-b^2)/(3*a^2);
set b9=c/a;
A2: a = a+0*<i>;
set q = 2*((b/(3*a)) |^ 3)+(3*a*d-b*c)/(3*a^2);
set c9=d/a;
set a9=b/a;
set y=Im z;
set x=Re z;
assume that
A3: Polynom(a,b,c,d,z)=0 and
A4: Im z=0;
A5: z = x + y*<i> by COMPLEX1:13;
0 = a*(Re z^3+(Im z^3)*<i>)+b*z^2+c*z+d by A3,COMPLEX1:13
.= a*(((Re z)|^ 3 - 3*Re z*(Im z)^2)+(Im z^3)*<i>) +b*z^2+c*z+d by Th5
.= a*(((Re z)|^ 3 - 3*Re z*(Im z)^2)+(-(Im z)|^ 3+3*(Re z)^2 *Im z)*<i>)
+b*z^2+c*z+d by Th5
.= (a+0*<i>)*((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>) +b*z^2+c*(Re z+Im
z *<i>)+d by COMPLEX1:13
.= Re a*Re ((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>) -Im a*Im((x|^ 3 - 3*
x*y^2)+(-y|^ 3+3*x^2*y)*<i>)+ (Re a*Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)
+Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)*Im a)*<i> +b*z^2+c*(Re z+Im z *<i>)
+d by COMPLEX1:82
.= (Re a*Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>) -0*Im((x|^ 3 - 3*x*y
^2)+(-y|^ 3+3*x^2*y)*<i>))+( Re a*Im((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>) +
Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)*Im a )*<i> +b*z^2+c*(Re z+Im z *<i>)
+d by A2,COMPLEX1:12
.= (Re a*Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>) -0)+(Re a*Im((x|^ 3
- 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>) +Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>)*0
)*<i> +b*z^2+c*(Re z+Im z *<i>)+d by A2,COMPLEX1:12
.= (Re a*Re((x|^ 3 - 3*x*y^2)+(-y|^ 3+3*x^2*y)*<i>) -0)+(Re a*(-y|^ 3+3*
x^2*y)+0 )*<i> +b*z^2+c*(Re z+Im z *<i>)+d by COMPLEX1:12
.= (Re a*(x|^ 3 - 3*x*y^2)-0)+(Re a*(-y|^ 3+3*x^2*y))*<i> +b*z^2+c*(Re z
+Im z *<i>)+d by COMPLEX1:12
.= (a*(x|^ 3 - 3*x*y^2)-0)+(Re a*(-y|^ 3+3*x^2*y))*<i> +b*z^2+c*(Re z+Im
z *<i>)+d by A2,COMPLEX1:12
.= a*(x|^ 3 - 3*x*y^2)+(a*(-y|^ 3+3*x^2*y))*<i> +b*(x^2-y^2+(2*x*y)*<i>)
+(c*x+(c*y)*<i>)+d by A2,A5,COMPLEX1:12;
then 0 = a*(x|^ 3 - 3*x*0)+b*(x^2-0)+c*x+d +(a*(-0|^ 3+0)+b*0+0)*<i> by A4
.= (a*x|^ 3+b*x^2+c*x+d)+(a*0+0)*<i> by NEWTON:11;
then
A6: Polynom(a,b,c,d,x) = 0;
A7: c9=d/a;
p/3=1/3*((3*a*c-b^2)/(3*a^2));
then
A8: p/3=(3*a*c-b^2)/(a^2*3*3) by XCMPLX_1:103;
A9: -q/2=-((b/(3*a)) |^ 3+1/2*((3*a*d-b*c)/(3*a^2)))
.=-((b/(3*a)) |^ 3+(3*a*d-b*c)/(a^2*3*2)) by XCMPLX_1:103
.=-(b/(3*a)) |^ 3-(3*a*d-b*c)/(6*a^2);
let u,v,x1;
assume that
A10: x1=Re z +b/(3*a) & Re z=u+v-b/(3*a) and
A11: 3*u*v+(3*a*c-b^2)/(3*a^2)=0;
a9=b/a & b9=c/a;
then Polynom(1,0,p,q,x1) = 0 by A1,A10,A6,A7,POLYEQ_1:16;
then
x1 = 3-root(-q/2+sqrt(q^2/4+(p/3) |^ 3)) + 3-root(-q/2-sqrt(q^2/4+(p/3)
|^ 3)) or x1 = 3-root(-q/2+sqrt(q^2/4+(p/3) |^ 3)) + 3-root(-q/2+sqrt(q^2/4+(p/
3) |^ 3)) or x1 = 3-root(-q/2-sqrt(q^2/4+(p/3) |^ 3)) + 3-root(-q/2-sqrt(q^2/4+
(p/3) |^ 3)) by A10,A11,POLYEQ_1:19;
hence thesis by A4,A10,A8,A9,COMPLEX1:13;
end;
theorem Th16:
z1 <> 0 & Polynom(z1,z2,z) = 0 implies z = -(z2/z1)
proof
assume z1 <> 0 & Polynom(z1,z2,z) = 0;
then z = (-z2)*z1" by XCMPLX_1:203;
hence thesis;
end;
begin
theorem
(for z holds Polynom(z1,z2,z3,z) = Polynom(s1,s2,s3,z)) implies z1 =
s1 & z2 = s2 & z3 = s3
proof
assume
A1: for z holds Polynom(z1,z2,z3,z) = Polynom(s1,s2,s3,z);
then
A2: Polynom(z1,z2,z3,-1r) = Polynom(s1,s2,s3,-1r);
Polynom(z1,z2,z3,0c) = Polynom(s1,s2,s3,0c) & Polynom(z1,z2,z3,1r) =
Polynom (s1,s2,s3,1r) by A1;
hence thesis by A2,COMPLEX1:def 4;
end;
theorem
(-a+sqrt (a^2+b^2))/2 >=0 & (a+sqrt (a^2+b^2))/2>=0
proof
A1: b^2>=0 by XREAL_1:63;
A2: a^2>=0 by XREAL_1:63;
then
A3: sqrt (a^2+b^2)>=0 by A1,SQUARE_1:def 2;
a^2+b^2>=0+a^2 by A1,XREAL_1:7;
then
A4: sqrt(a^2+b^2)>=sqrt(a^2) by A2,SQUARE_1:26;
per cases;
suppose
A5: a>=0;
then sqrt(a^2+b^2)>=a by A4,SQUARE_1:22;
then sqrt(a^2+b^2)-a>=a-a by XREAL_1:9;
hence thesis by A3,A5;
end;
suppose
A6: a<0;
then sqrt(a^2+b^2) >= -a by A4,SQUARE_1:23;
then sqrt(a^2+b^2)-(-a) >= -a-(-a) by XREAL_1:9;
hence thesis by A3,A6;
end;
end;
theorem Th19:
z^2 = s & Im s >= 0 implies z=sqrt (( Re s+sqrt ((Re s)^2+(Im s)
^2))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*<i> or z=-sqrt (( Re s+
sqrt ((Re s)^2+(Im s)^2))/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*<i>
proof
set a=Re s;
set b=Im s;
set u=Re z;
set v=Im z;
A1: z = u+v*<i> by COMPLEX1:13;
assume z^2=s;
then
A2: u^2-v^2+2*u*v*<i> =a+b*<i> by A1,COMPLEX1:13;
assume Im s >=0;
then
A3: u<=0 & v<=0 or u>=0 & v>=0 by A2,COMPLEX1:77;
A4: u^2>=0 & v^2>=0 by XREAL_1:63;
A5: u^2-v^2=a by A2,COMPLEX1:77;
then (u^2+v^2)^2=a^2+b^2 by A2;
then u^2+v^2=sqrt (a^2+b^2) by A4,SQUARE_1:22;
then
-u=sqrt ((a+sqrt (a^2+b^2))/2) & -v=sqrt ((-a+sqrt (a^2+b^2))/ 2) or u=
sqrt ((a+sqrt (a^2+b^2))/2) & v=sqrt ((-a+sqrt (a^2+b^2))/2) by A5,A3,
SQUARE_1:22,23;
hence thesis by COMPLEX1:13;
end;
theorem
z^2 = s & Im s = 0 & Re s > 0 implies z=sqrt(Re s) or z=-sqrt(Re s)
proof
assume
A1: z^2=s;
assume that
A2: Im s =0 and
A3: Re s >0;
z=sqrt (( Re s+sqrt ((Re s)^2+0))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+0))/2
))*<i> or z=-sqrt (( Re s+sqrt ((Re s)^2+0))/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+
0^2))/2))*<i> by A1,A2,Th19;
then z=sqrt (( Re s+Re s)/2)+ sqrt ((-Re s+sqrt ((Re s)^2+0))/2)*<i> or z=-
sqrt (( Re s+sqrt ((Re s)^2+0))/2)+ -sqrt ((-Re s+sqrt ((Re s)^2+0))/2)*<i> by
A3,SQUARE_1:22;
then
z=sqrt (( Re s+Re s)/2)+ sqrt ((-Re s+Re s)/2)*<i> or z=-sqrt (( Re s+Re
s)/2) + -sqrt ((-Re s+sqrt ((Re s)^2+0))/2)*<i> by A3,SQUARE_1:22;
then
z=sqrt (Re s)+ sqrt ((0+(Re s-Re s))/2)*<i> or z=-sqrt (Re s)+-sqrt ((0+
(Re s-Re s))/2)*<i> by A3,SQUARE_1:22;
hence thesis;
end;
theorem
z^2 = s & Im s = 0 & Re s < 0 implies z= sqrt (-Re s)*<i> or z= -sqrt
(-Re s)*<i>
proof
assume
A1: z^2=s;
assume that
A2: Im s =0 and
A3: Re s < 0;
z=sqrt (( Re s+sqrt ((Re s)^2+0))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+0))/2
))*<i> or z=-sqrt (( Re s+sqrt ((Re s)^2+0))/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+
0^2))/2))*<i> by A1,A2,Th19;
then
z=sqrt (( Re s+-Re s)/2)+ sqrt ((-Re s+sqrt ((Re s)^2+0))/2)*<i> or z=-
sqrt (( Re s+sqrt ((Re s)^2+0))/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+0))/2))*<i>
by A3,SQUARE_1:23;
then
z=sqrt (( Re s+-Re s)/2)+ sqrt ((-Re s+-Re s)/2)*<i> or z=-sqrt (( Re s+
-Re s)/2)+(-sqrt ((-Re s+sqrt ((Re s)^2+0))/2))*<i> by A3,SQUARE_1:23;
then
z=sqrt (( Re s+-Re s)/2)+ sqrt ((-Re s+-Re s)/2)*<i> or z=-sqrt (( Re s+
-Re s)/2)+(-sqrt ((-Re s+-Re s)/2))*<i> by A3,SQUARE_1:23;
hence thesis;
end;
theorem
z^2 = s & Im s <0 implies z= sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)
+ (-sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*<i> or z=-sqrt (( Re s+sqrt ((Re
s)^2+(Im s)^2))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*<i>
proof
assume
A1: z^2=s;
set v=Im z;
set u=Re z;
set b=Im s;
set a=Re s;
z = u + v*<i> by COMPLEX1:13;
then
A2: s=a+b*<i> & z^2 = u^2-v^2 + 2*u*v*<i> by COMPLEX1:13;
assume Im s<0;
then 2*(u*v)<0 by A1,A2,COMPLEX1:77;
then u*v<0;
then
A3: u<0 & v>0 or u>0 & v<0 by XREAL_1:133;
A4: u^2>=0 & v^2>=0 by XREAL_1:63;
A5: u^2-v^2=a by A1,A2,COMPLEX1:77;
then sqrt (u^2+v^2)^2=sqrt (a^2+b^2) by A1,A2;
then u^2+v^2=sqrt (a^2+b^2) by A4,SQUARE_1:22;
then -u=sqrt ((a+sqrt (a^2+b^2))/2) & v=sqrt ((-a+sqrt (a^2+b^2))/2) or u=
sqrt ((a+sqrt (a^2+b^2))/2) & -v=sqrt ((-a+sqrt (a^2+b^2))/2) by A5,A3,
SQUARE_1:22,23;
hence thesis by COMPLEX1:13;
end;
theorem Th23:
z^2 = s implies z=sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (
sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*<i> or z=-sqrt (( Re s+sqrt ((Re s)
^2+(Im s)^2))/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*<i> or z= sqrt (
( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2
))*<i> or z=-sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (sqrt ((-Re s+sqrt ((Re
s)^2+(Im s)^2))/2))*<i>
proof
set a=Re s;
set b=Im s;
set u=Re z;
set v=Im z;
A1: u^2>=0 & v^2>=0 by XREAL_1:63;
z = u + v*<i> by COMPLEX1:13;
then
A2: s=a+b*<i> & z^2 = u^2-v^2 + 2*u*v*<i> by COMPLEX1:13;
assume
A3: z^2=s;
then
A4: u^2-v^2=a by A2,COMPLEX1:77;
then sqrt (u^2+v^2)^2=sqrt (a^2+b^2) by A3,A2;
then
A5: u^2+v^2=sqrt (a^2+b^2) by A1,SQUARE_1:22;
per cases;
suppose
b>=0;
then u<=0 & v<=0 or u>=0 & v>=0 by A3,A2,COMPLEX1:77;
then -u=sqrt ((a+sqrt (a^2+b^2))/2) & -v=sqrt ((-a+sqrt (a^2+b^2))/ 2) or
u=sqrt ((a+sqrt (a^2+b^2))/2) & v=sqrt ((-a+sqrt (a^2+b^2))/2) by A4,A5,
SQUARE_1:22,23;
hence thesis by COMPLEX1:13;
end;
suppose
b<0;
then 2*(u*v)<0 by A3,A2,COMPLEX1:77;
then u*v<0;
then u<0 & v>0 or u>0 & v<0 by XREAL_1:133;
then
-u=sqrt ((a+sqrt (a^2+b^2))/2) & v=sqrt ((-a+sqrt (a^2+b^2))/2) or u=
sqrt ((a+sqrt (a^2+b^2))/2) & -v=sqrt ((-a+sqrt (a^2+b^2))/2) by A4,A5,
SQUARE_1:22,23;
hence thesis by COMPLEX1:13;
end;
end;
theorem
z1<>0 & Polynom(z1,z2,0,z)=0 implies z=-(z2/z1) or z=0
proof
assume that
A1: z1<>0 and
A2: Polynom(z1,z2,0,z)=0;
0 =(z1*z+z2)*z by A2;
then Polynom(z1,z2,z) = 0 or z=0;
hence thesis by A1,Th16;
end;
theorem Th25:
z1<>0 & Polynom(z1,0,z3,z)=0 implies for s st s=-(z3/z1) holds z
= sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+(Im s
)^2))/2))*<i> or z=-sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (-sqrt ((-Re s+
sqrt ((Re s)^2+(Im s)^2))/2))*<i> or z= sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/
2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*<i> or z=-sqrt (( Re s+sqrt ((
Re s)^2+(Im s)^2))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*<i>
proof
assume z1<>0 & Polynom(z1,0,z3,z)=0;
then
A1: z^2=(-z3)/z1 by XCMPLX_1:89;
let s;
assume s=-(z3/z1);
hence thesis by A1,Th23;
end;
theorem Th26:
z1<>0 & Polynom(z1,z2,z3,z)=0 implies for h,t st h=(z2/(2*z1))^2
-z3/z1 & t=z2/(2*z1) holds z= sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (sqrt
((-Re h+sqrt ((Re h)^2+(Im h)^2))/2))*<i>-t or z=-sqrt (( Re h+sqrt ((Re h)^2+(
Im h)^2))/2)+ (-sqrt ((-Re h+sqrt ((Re h)^2+(Im h)^2))/2))*<i>-t or z= sqrt ((
Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (-sqrt ((-Re h+sqrt ((Re h)^2+(Im h)^2))/2))
*<i>-t or z=-sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (sqrt ((-Re h+sqrt ((Re
h)^2+(Im h)^2))/2))*<i>-t
proof
assume that
A1: z1<>0 and
A2: Polynom(z1,z2,z3,z)=0;
(z1*z^2+z2*z+z3)/z1=0 by A2;
then (z^2*z1)/z1+(z2*z)/z1+z3/z1=0;
then z^2+(z2/z1)*z+z3/z1=0 by A1,XCMPLX_1:89;
then z^2+2*z2/(2*z1)*z+z3/z1=0 by XCMPLX_1:91;
then
A3: (z+(z2/(2*z1)))^2-((z2/(2*z1))^2-z3/z1)=0;
let h,t;
assume h=(z2/(2*z1))^2-z3/z1 & t=z2/(2*z1);
then
z+t-t= sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (sqrt ((-Re h+sqrt ((
Re h)^2+(Im h)^2))/2))*<i>-t or z+t-t=-sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2
)+ (-sqrt ((-Re h+sqrt ((Re h)^2+(Im h)^2))/2))*<i>-t or z+t-t= sqrt (( Re h+
sqrt ((Re h)^2+(Im h)^2))/2)+ (-sqrt ((-Re h+sqrt ((Re h)^2+(Im h)^2))/2))*<i>-
t or z+t-t=-sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (sqrt ((-Re h+sqrt ((Re
h)^2+(Im h)^2))/2))*<i>-t by A3,Th23;
hence thesis;
end;
theorem
z|^ 3=z*z*z & z|^ 3=z^2*z & z|^ 3 = z^3
proof
z|^ 3 = z|^(2+1) .= z|^(1+1)*z by NEWTON:6
.= z|^1*z*z by NEWTON:6
.= z*z*z;
hence thesis;
end;
theorem
z1<>0 & Polynom(z1,z2,0,0,z)=0 implies z=-z2/z1 or z=0
proof
assume that
A1: z1<>0 and
A2: Polynom(z1,z2,0,0,z)=0;
0 =(z1*z +z2)*z^2 by A2;
then Polynom(z1,z2,z)=0 or 1*z^2+0*z+0=0;
hence thesis by A1,Th16;
end;
theorem
z1<>0 & Polynom(z1,0,z3,0,z)=0 implies for s st s=-(z3/z1) holds z=0
or z=sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+(
Im s)^2))/2))*<i> or z=-sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2))/2)+ (-sqrt ((-Re
s+sqrt ((Re s)^2+(Im s)^2))/2))*<i> or z= sqrt (( Re s+sqrt ((Re s)^2+(Im s)^2)
)/2)+ (-sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*<i> or z=-sqrt (( Re s+sqrt
((Re s)^2+(Im s)^2))/2)+ (sqrt ((-Re s+sqrt ((Re s)^2+(Im s)^2))/2))*<i>
proof
assume that
A1: z1<>0 and
A2: Polynom(z1,0,z3,0,z)=0;
let s;
0 =(z1*z^2+z3)*z by A2;
then
A3: Polynom(z1,0,z3,z)=0 or z=0;
assume s=-(z3/z1);
hence thesis by A1,A3,Th25;
end;
theorem
z1<>0 & Polynom(z1,z2,z3,0,z)=0 implies for s,h,t st h=(z2/(2*z1))^2-
z3/z1 & t=z2/(2*z1) holds z=0 or z= sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+
(sqrt ((-Re h+sqrt ((Re h)^2+(Im h)^2))/2))*<i>-t or z=-sqrt (( Re h+sqrt ((Re
h)^2+(Im h)^2))/2)+ (-sqrt ((-Re h+sqrt ((Re h)^2+(Im h)^2))/2))*<i>-t or z=
sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (-sqrt ((-Re h+sqrt ((Re h)^2+(Im h)
^2))/2))*<i>-t or z=-sqrt (( Re h+sqrt ((Re h)^2+(Im h)^2))/2)+ (sqrt ((-Re h+
sqrt ((Re h)^2+(Im h)^2))/2))*<i>-t
proof
assume that
A1: z1<>0 and
A2: Polynom(z1,z2,z3,0,z)=0;
let s,h,t;
0 =Polynom(z1,z2,z3,z)*z by A2;
then
A3: z=0 or Polynom(z1,z2,z3,z)=0;
assume h=(z2/(2*z1))^2-z3/z1 & t=z2/(2*z1);
hence thesis by A1,A3,Th26;
end;
Lm2: for n be Nat st n>0 holds 0 |^ n = 0
proof
let n be Nat;
assume n>0;
then n >= 0+1 by NAT_1:13;
hence thesis by NEWTON:11;
end;
theorem Th31:
for x being Real, n be Nat holds (cos x + sin
x*<i>) |^ n = cos (n*x) + sin (n*x)*<i>
proof
let x be Real;
defpred P[Nat] means (cos x +sin x*<i>)|^ $1 = cos ($1*x)+sin ($1*x)*<i>;
A1: now
let n be Nat;
assume P[n];
then
(cos x + sin x*<i>) |^ (n+1) = (cos(n*x)+sin(n*x)*<i>)*(cos x+(sin x)*
<i>) by NEWTON:6
.= cos(n*x)*cos x - sin(n*x)*sin x+ (cos(n*x)*sin x+cos x*sin(n*x))*
<i>
.= cos(n*x+x)+(cos(n*x)*sin x+cos x*sin(n*x))*<i> by SIN_COS:75
.= cos((n+1)*x)+sin((n+1)*x)*<i> by SIN_COS:75;
hence P[n+1];
end;
A2: P[0] by NEWTON:4,SIN_COS:31;
thus for n be Nat holds P[n] from NAT_1:sch 2(A2,A1);
end;
theorem
for z being Element of COMPLEX for n being Element of NAT
holds z|^ n = (|.z.| to_power n)*cos (n*Arg z) + (|.z.| to_power n)*sin (
n*Arg z)*<i>
proof
let z be Element of COMPLEX;
let n be Element of NAT;
z|^ n =(|.z.|*cos Arg z-0*sin Arg z+(|.z.|*sin Arg z+cos Arg z*0)*<i>)
|^ n by COMPTRIG:62
.=(|.z.|*(cos Arg z+sin Arg z*<i>))|^ n
.= |.z.||^ n*(cos Arg z+sin Arg z*<i>)|^ n by NEWTON:7;
hence z|^ n = (|.z.| to_power n)*(cos (n*Arg z)+sin (n*Arg z)*<i>) by Th31
.= (|.z.| to_power n)*cos(n*Arg z)+(|.z.| to_power n)*sin(n*Arg z)*<i>;
end;
theorem Th33:
for n,k be Element of NAT,x be Real st n <> 0 holds (cos((x+2*PI
*k)/n) + sin((x+2*PI*k)/n)*<i>)|^ n = cos x + (sin x)*<i>
proof
let n,k be Element of NAT,x be Real;
assume
A1: n <> 0;
thus (cos((x+2*PI*k)/n)+ sin((x+2*PI*k)/n)*<i>)|^ n = cos (n*((x+2*PI*k)/n))
+sin (n*((x+2*PI*k)/n))*<i> by Th31
.= cos(x+2*PI*k)+sin(n*((x+2*PI*k)/n))*<i> by A1,XCMPLX_1:87
.= cos(x+2*PI*k)+sin(x+2*PI*k)*<i> by A1,XCMPLX_1:87
.= cos.(x+2*PI*k)+sin(x+2*PI*k)*<i> by SIN_COS:def 19
.= cos.(x+2*PI*k)+(sin.(x+2*PI*k))*<i> by SIN_COS:def 17
.= cos.(x+2*PI*k)+(sin.x)*<i> by SIN_COS2:10
.= cos.x + (sin.x)*<i> by SIN_COS2:11
.= cos.x + (sin x)*<i> by SIN_COS:def 17
.= cos x + (sin x)*<i> by SIN_COS:def 19;
end;
theorem Th34:
for z be Complex for n,k be Element of NAT st n <> 0
holds z = ((n-root |.z.|)*cos((Arg z+2*PI*k)/n) + (n-root |.z.|)*sin((Arg z+2*
PI*k)/n)*<i>)|^ n
proof
let z be Complex;
let n,k be Element of NAT;
assume
A1: n <> 0;
then
A2: n >= 0+1 by NAT_1:13;
per cases;
suppose
z <> 0;
then
A3: |.z.| > 0 by COMPLEX1:47;
thus ((n-root |.z.|)*cos((Arg z+2*PI*k)/n)+ (n-root |.z.|)*sin((Arg z+2*PI
*k)/n)*<i>)|^ n = ((n-root |.z.|)* (cos((Arg z+2*PI*k)/n)+sin((Arg z+2*PI*k)/n)
*<i>))|^ n
.= ((n-root |.z.|)|^ n) *((cos((Arg z+2*PI*k)/n)+sin((Arg z+2*PI*k)/n)
*<i>)|^ n) by NEWTON:7
.= ((n-root |.z.|)|^ n)*(cos Arg z+(sin Arg z)*<i>) by A1,Th33
.= |.z.|*(cos Arg z+(sin Arg z)*<i>) by A1,A3,COMPTRIG:4
.= |.z.|*cos Arg z-0*sin Arg z+(|.z.|*sin Arg z+0*cos Arg z)*<i>
.= z by COMPTRIG:62;
end;
suppose
A4: z = 0;
hence
((n-root |.z.|)*cos((Arg z+2*PI*k)/n)+ (n-root |.z.|)*sin((Arg z+2*PI
*k)/n)*<i>)|^ n =((0*cos((Arg z+2*PI*k)/n)+ (n-root 0)*sin((Arg z+2*PI*k)/n)*
<i>)|^ n) by A2,COMPLEX1:44,POWER:5
.= (0*sin((Arg z+2*PI*k)/n)*<i>)|^ n by A2,POWER:5
.= z by A1,A4,Lm2;
end;
end;
theorem
for z be Element of COMPLEX, n be non zero Element of NAT, k be
Element of NAT holds (n-root |.z.|)*cos((Arg z+2*PI*k)/n)+ (n-root |.z.|)*sin((
Arg z+2*PI*k)/n)*<i> is CRoot of n,z
proof
let z be Element of COMPLEX, n be non zero Element of NAT,k be Element of
NAT;
((n-root |.z.|)*cos((Arg z+2*PI*k)/n)+ (n-root |.z.|)*sin((Arg z+2*PI*k)
/n)*<i>)|^ n=z by Th34;
hence thesis by COMPTRIG:def 2;
end;
theorem
for z be Complex, v be CRoot of 1,z holds v = z
proof
let z be Complex, v be CRoot of 1,z;
v|^ 1 = z by COMPTRIG:def 2;
hence thesis;
end;
theorem
for n be non zero Nat, v be CRoot of n,0 holds v = 0
proof
let n be non zero Nat, v be CRoot of n,0;
defpred P[Nat] means v|^ $1 = 0;
A1: now
let k be non zero Nat;
assume that
A2: k <> 1 and
A3: P[k];
consider t be Nat such that
A4: k = t+1 by NAT_1:6;
t <> 0 by A2,A4;
then reconsider t as non zero Nat;
take t;
thus t < k by A4,NAT_1:13;
v|^ k = (v|^ t)*v by A4,NEWTON:6;
then v|^ t = 0 or v = 0 by A3;
hence P[t] by Lm2;
end;
A5: ex n be non zero Nat st P[n]
proof
take n;
thus thesis by COMPTRIG:def 2;
end;
P[1] from COMPTRIG:sch 1(A5,A1);
hence thesis;
end;
theorem
for n be non zero Element of NAT, z be Complex for v be CRoot
of n,z st v = 0 holds z = 0
proof
let n be non zero Element of NAT, z be Complex;
let v be CRoot of n,z;
assume v = 0;
then 0|^ n = z by COMPTRIG:def 2;
hence thesis by Lm2;
end;
theorem
for n be non zero Element of NAT, k be Element of NAT holds cos(2*PI*
k/n) + sin(2*PI*k/n)*<i> is CRoot of n,1
proof
let n be non zero Element of NAT,k be Element of NAT;
(cos(2*PI*k/n)+sin(2*PI*k/n)*<i>)|^n =cos(n*((2*PI*k)/n))+sin(n*((2*PI*k
)/n))*<i> by Th31
.=cos(2*PI*k)+(sin(n*((2*PI*k)/n)))*<i> by XCMPLX_1:87
.=cos(2*PI*k+0)+(sin(2*PI*k+0))*<i> by XCMPLX_1:87
.=cos.(2*PI*k+0)+(sin(2*PI*k+0))*<i> by SIN_COS:def 19
.=cos.(2*PI*k+0)+(sin.(2*PI*k+0))*<i> by SIN_COS:def 17
.=cos.(2*PI*k+0)+(sin.0)*<i> by SIN_COS2:10
.=1 by SIN_COS:30,SIN_COS2:11;
hence thesis by COMPTRIG:def 2;
end;
theorem
for z,s being Element of COMPLEX, n being Element of NAT st s<>0 & z<>
0 & n>=1 & s|^ n=z|^ n holds |.s.| = |.z.|
proof
let z,s be Element of COMPLEX, n be Element of NAT;
assume that
A1: s<>0 and
A2: z<>0 and
A3: n>=1 and
A4: s|^ n=z|^ n;
z|^ n = (|.s.|*cos Arg s + |.s.|*sin Arg s *<i>)|^ n by A4,COMPTRIG:62
.=(|.s.|*(cos Arg s+sin Arg s *<i>))|^ n
.=(|.s.||^ n)*((cos Arg s+sin Arg s *<i>)|^ n) by NEWTON:7
.=(|.s.| to_power n)*(cos (n*Arg s)+sin (n*Arg s)*<i>) by Th31
.= ((|.s.| to_power n)*cos (n*Arg s) )+((|.s.| to_power n)*sin (n*Arg s)
)*<i>;
then
A5: ((|.s.| to_power n)*cos (n*Arg s)) +((|.s.| to_power n)*sin (n*Arg s ))*
<i> = (|.z.|*cos Arg z + |.z.|*sin Arg z *<i>)|^ n by COMPTRIG:62
.=(|.z.|*(cos Arg z+sin Arg z *<i>))|^ n
.=(|.z.||^ n)*((cos Arg z+sin Arg z *<i>)|^ n) by NEWTON:7
.=(|.z.| to_power n)*(cos (n*Arg z)+sin (n*Arg z)*<i>) by Th31
.= ((|.z.| to_power n)*cos (n*Arg z))+((|.z.| to_power n) *sin (n*Arg z)
)*<i>;
then (|.s.| to_power n)*cos (n*Arg s)=(|.z.| to_power n)*cos (n*Arg z) by
COMPLEX1:77;
then
(|.s.| to_power n) ^2*(cos (n*Arg s))^2+ ((|.s.| to_power n)*sin (n*Arg
s))^2 =((|.z.| to_power n)*cos (n*Arg z))^2+ ((|.z.| to_power n)*sin (n*Arg z))
^2 by A5,SQUARE_1:9;
then (|.s.| to_power n) ^2*((cos (n*Arg s))^2+(sin (n*Arg s))^2) =((|.z.|
to_power n))^2*((cos (n*Arg z))^2+(sin (n*Arg z))^2);
then (|.s.| to_power n) ^2*((cos (n*Arg s))^2+(sin (n*Arg s))^2) =((|.z.|
to_power n))^2*1 by SIN_COS:29;
then
A6: (|.s.| to_power n) ^2*1=((|.z.| to_power n))^2 by SIN_COS:29;
A7: |.s.|>0 by A1,COMPLEX1:47;
then |.s.| to_power n > 0 by POWER:34;
then
A8: (|.s.| to_power n) =sqrt ((|.z.| to_power n))^2 by A6,SQUARE_1:22;
A9: |.z.|>0 by A2,COMPLEX1:47;
then |.z.| to_power n > 0 by POWER:34;
then |.s.| |^ n=|.z.| |^ n by A8,SQUARE_1:22;
then |.s.| = n-root (|.z.| |^ n) by A3,A7,POWER:4;
hence thesis by A3,A9,POWER:4;
end;