polyeq_3.miz
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 ;
:: original:
^2
redefine
::
POLYEQ_3:def1
func z
^2 ->
Element of
COMPLEX equals ((((
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
::$Canceled
let a, b, c, z;
:: original:
Polynom
redefine
func
Polynom (a,b,c,z) ->
Element of
COMPLEX ;
coherence by
XCMPLX_0:def 2;
end
theorem ::
POLYEQ_3:1
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,
COMPLEX1: 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,
COMPLEX1: 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 ::
POLYEQ_3:2
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,
COMPLEX1: 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,
XREAL_1: 63;
(((
- (a
* (y
^2 )))
+ (((b
* x)
+ (a
* (x
^2 )))
+ c))
+ (a
* (y
^2 )))
= (
0
+ (a
* (y
^2 ))) by
A5,
COMPLEX1: 4,
COMPLEX1: 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,
COMPLEX1: 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 ::
POLYEQ_3:3
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 ::
POLYEQ_3:4
for a,b,c be
Real, z,z1,z2 be
Complex st a
<>
0 & for z be
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 be
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;
::
POLYEQ_3:def3
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;
:: original:
Polynom
redefine
::
POLYEQ_3:def4
func
Polynom (a,b,c,d,z) equals ((((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 ::
POLYEQ_3:5
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 ::
POLYEQ_3:6
(for z be
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 be
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 ::
POLYEQ_3:7
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 ::
POLYEQ_3:8
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 ::
POLYEQ_3:9
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 ::
POLYEQ_3:10
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 ::
POLYEQ_3:11
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 ::
POLYEQ_3:12
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,
SQUARE_1: 29;
hence thesis;
end;
theorem ::
POLYEQ_3:13
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 ::
POLYEQ_3:14
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,
COMPLEX1: 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,
COMPLEX1: 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 ::
POLYEQ_3:15
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 ::
POLYEQ_3:16
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 ::
POLYEQ_3:17
(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 ::
POLYEQ_3:18
(((
- 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 ::
POLYEQ_3:19
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,
SQUARE_1: 23;
hence thesis by
COMPLEX1: 13;
end;
theorem ::
POLYEQ_3:20
(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 by
SQUARE_1: 17;
end;
theorem ::
POLYEQ_3:21
(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 by
SQUARE_1: 17;
end;
theorem ::
POLYEQ_3:22
(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,
SQUARE_1: 23;
hence thesis by
COMPLEX1: 13;
end;
theorem ::
POLYEQ_3:23
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,
SQUARE_1: 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,
SQUARE_1: 23;
hence thesis by
COMPLEX1: 13;
end;
end;
theorem ::
POLYEQ_3:24
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 ::
POLYEQ_3:25
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 ::
POLYEQ_3:26
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 ::
POLYEQ_3:27
(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 ::
POLYEQ_3:28
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 ::
POLYEQ_3:29
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 ::
POLYEQ_3:30
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 ::
POLYEQ_3:31
Th31: for x be
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 ::
POLYEQ_3:32
for z be
Element of
COMPLEX holds for n be
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 ::
POLYEQ_3:33
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 ::
POLYEQ_3:34
Th34: for z be
Complex holds 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 ::
POLYEQ_3:35
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 ::
POLYEQ_3:36
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 ::
POLYEQ_3:37
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 ::
POLYEQ_3:38
for n be non
zero
Element of
NAT , z be
Complex holds 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 ::
POLYEQ_3:39
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 ::
POLYEQ_3:40
for z,s be
Element of
COMPLEX , n be
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;