polyeq_5.miz
begin
reserve a,b for
Complex;
theorem ::
POLYEQ_5:1
Th1: (a
* a)
= (a
|^ 2)
proof
thus (a
* a)
= ((a
|^ 1)
* a)
.= (a
|^ (1
+ 1)) by
NEWTON: 6
.= (a
|^ 2);
end;
theorem ::
POLYEQ_5:2
Th2: ((a
* a)
* a)
= (a
|^ 3)
proof
thus ((a
* a)
* a)
= ((a
|^ 2)
* a) by
Th1
.= (a
|^ (2
+ 1)) by
NEWTON: 6
.= (a
|^ 3);
end;
theorem ::
POLYEQ_5:3
Th3: (((a
* a)
* a)
* a)
= (a
|^ 4)
proof
thus (((a
* a)
* a)
* a)
= ((a
|^ 3)
* a) by
Th2
.= (a
|^ (3
+ 1)) by
NEWTON: 6
.= (a
|^ 4);
end;
theorem ::
POLYEQ_5:4
Th4: ((a
- b)
|^ 2)
= (((a
|^ 2)
- ((2
* a)
* b))
+ (b
|^ 2))
proof
thus ((a
- b)
|^ 2)
= ((a
- b)
* (a
- b)) by
Th1
.= (((a
^2 )
- ((2
* a)
* b))
+ (b
^2 ))
.= (((a
|^ 2)
- ((2
* a)
* b))
+ (b
* b)) by
Th1
.= (((a
|^ 2)
- ((2
* a)
* b))
+ (b
|^ 2)) by
Th1;
end;
theorem ::
POLYEQ_5:5
Th5: ((a
- b)
|^ 3)
= ((((a
|^ 3)
- ((3
* (a
|^ 2))
* b))
+ ((3
* (b
|^ 2))
* a))
- (b
|^ 3))
proof
((a
- b)
|^ (2
+ 1))
= (((a
- b)
|^ 2)
* (a
- b)) by
NEWTON: 6
.= ((((a
|^ 2)
- ((2
* a)
* b))
+ (b
|^ 2))
* (a
- b)) by
Th4
.= (((((a
|^ 2)
* a)
- ((a
|^ 2)
* b))
- ((((2
* a)
* b)
* a)
- (((2
* a)
* b)
* b)))
+ (((b
|^ 2)
* a)
- ((b
|^ 2)
* b)))
.= (((((a
|^ 2)
* a)
- ((a
|^ 2)
* b))
- ((((2
* a)
* b)
* a)
- (((2
* a)
* b)
* b)))
+ (((b
|^ 2)
* a)
- (b
|^ (2
+ 1)))) by
NEWTON: 6
.= ((((a
|^ 3)
- ((a
|^ 2)
* b))
- (((2
* (a
* a))
* b)
- (((2
* a)
* b)
* b)))
+ (((b
|^ 2)
* a)
- (b
|^ 3))) by
NEWTON: 6
.= ((((a
|^ 3)
- ((a
|^ 2)
* b))
- (((2
* ((a
|^ 1)
* a))
* b)
- (((2
* a)
* b)
* b)))
+ (((b
|^ 2)
* a)
- (b
|^ 3)))
.= ((((a
|^ 3)
- ((a
|^ 2)
* b))
- (((2
* (a
|^ (1
+ 1)))
* b)
- (((2
* a)
* b)
* b)))
+ (((b
|^ 2)
* a)
- (b
|^ 3))) by
NEWTON: 6
.= (((((a
|^ 3)
- ((3
* (a
|^ 2))
* b))
+ ((2
* (b
* b))
* a))
+ ((b
|^ 2)
* a))
- (b
|^ 3))
.= (((((a
|^ 3)
- ((3
* (a
|^ 2))
* b))
+ ((2
* ((b
|^ 1)
* b))
* a))
+ ((b
|^ 2)
* a))
- (b
|^ 3))
.= (((((a
|^ 3)
- ((3
* (a
|^ 2))
* b))
+ ((2
* (b
|^ (1
+ 1)))
* a))
+ ((b
|^ 2)
* a))
- (b
|^ 3)) by
NEWTON: 6
.= ((((a
|^ 3)
- ((3
* (a
|^ 2))
* b))
+ ((3
* (b
|^ 2))
* a))
- (b
|^ 3));
hence thesis;
end;
theorem ::
POLYEQ_5:6
Th6: ((a
- b)
|^ 4)
= (((((a
|^ 4)
- ((4
* (a
|^ 3))
* b))
+ ((6
* (a
|^ 2))
* (b
|^ 2)))
- ((4
* (b
|^ 3))
* a))
+ (b
|^ 4))
proof
((a
- b)
|^ (3
+ 1))
= (((a
- b)
|^ 3)
* (a
- b)) by
NEWTON: 6
.= (((((a
|^ 3)
- ((3
* (a
|^ 2))
* b))
+ ((3
* (b
|^ 2))
* a))
- (b
|^ 3))
* (a
- b)) by
Th5
.= ((((((a
|^ 3)
* a)
- ((a
|^ 3)
* b))
+ ((
- (((3
* (a
|^ 2))
* b)
* a))
+ (((3
* (a
|^ 2))
* b)
* b)))
+ ((((3
* (b
|^ 2))
* a)
* a)
- (((3
* (b
|^ 2))
* a)
* b)))
+ ((
- ((b
|^ 3)
* a))
+ ((b
|^ 3)
* b)))
.= ((((((a
|^ 3)
* a)
- ((a
|^ 3)
* b))
+ ((
- (((3
* (a
|^ 2))
* b)
* a))
+ (((3
* (a
|^ 2))
* b)
* b)))
+ ((((3
* (b
|^ 2))
* a)
* a)
- (((3
* (b
|^ 2))
* a)
* b)))
+ ((
- ((b
|^ 3)
* a))
+ (b
|^ (3
+ 1)))) by
NEWTON: 6
.= (((((a
|^ 4)
- ((a
|^ 3)
* b))
+ ((
- ((3
* ((a
|^ 2)
* a))
* b))
+ (((3
* (a
|^ 2))
* b)
* b)))
+ ((((3
* (b
|^ 2))
* a)
* a)
- (((3
* (b
|^ 2))
* a)
* b)))
+ ((
- ((b
|^ 3)
* a))
+ (b
|^ 4))) by
NEWTON: 6
.= (((((a
|^ 4)
- ((a
|^ 3)
* b))
+ ((
- ((3
* (a
|^ (2
+ 1)))
* b))
+ (((3
* (a
|^ 2))
* b)
* b)))
+ ((((3
* (b
|^ 2))
* a)
* a)
- (((3
* (b
|^ 2))
* a)
* b)))
+ ((
- ((b
|^ 3)
* a))
+ (b
|^ 4))) by
NEWTON: 6
.= (((((a
|^ 4)
- ((a
|^ 3)
* b))
+ ((
- ((3
* (a
|^ 3))
* b))
+ ((3
* (a
|^ 2))
* (b
* b))))
+ ((((3
* (b
|^ 2))
* a)
* a)
- (((3
* (b
|^ 2))
* a)
* b)))
+ ((
- ((b
|^ 3)
* a))
+ (b
|^ 4)))
.= (((((a
|^ 4)
- ((a
|^ 3)
* b))
+ ((
- ((3
* (a
|^ 3))
* b))
+ ((3
* (a
|^ 2))
* ((b
|^ 1)
* b))))
+ ((((3
* (b
|^ 2))
* a)
* a)
- (((3
* (b
|^ 2))
* a)
* b)))
+ ((
- ((b
|^ 3)
* a))
+ (b
|^ 4)))
.= (((((a
|^ 4)
- ((a
|^ 3)
* b))
+ ((
- ((3
* (a
|^ 3))
* b))
+ ((3
* (a
|^ 2))
* (b
|^ (1
+ 1)))))
+ ((((3
* (b
|^ 2))
* a)
* a)
- (((3
* (b
|^ 2))
* a)
* b)))
+ ((
- ((b
|^ 3)
* a))
+ (b
|^ 4))) by
NEWTON: 6
.= (((((a
|^ 4)
- ((a
|^ 3)
* b))
+ ((
- ((3
* (a
|^ 3))
* b))
+ ((3
* (a
|^ 2))
* (b
|^ 2))))
+ (((3
* (b
|^ 2))
* (a
* a))
- (((3
* (b
|^ 2))
* a)
* b)))
+ ((
- ((b
|^ 3)
* a))
+ (b
|^ 4)))
.= (((((a
|^ 4)
- ((a
|^ 3)
* b))
+ ((
- ((3
* (a
|^ 3))
* b))
+ ((3
* (a
|^ 2))
* (b
|^ 2))))
+ (((3
* (b
|^ 2))
* ((a
|^ 1)
* a))
- (((3
* (b
|^ 2))
* b)
* a)))
+ ((
- ((b
|^ 3)
* a))
+ (b
|^ 4)))
.= (((((a
|^ 4)
- ((a
|^ 3)
* b))
+ ((
- ((3
* (a
|^ 3))
* b))
+ ((3
* (a
|^ 2))
* (b
|^ 2))))
+ (((3
* (b
|^ 2))
* (a
|^ (1
+ 1)))
- ((3
* ((b
|^ 2)
* b))
* a)))
+ ((
- ((b
|^ 3)
* a))
+ (b
|^ 4))) by
NEWTON: 6
.= (((((a
|^ 4)
- ((a
|^ 3)
* b))
+ ((
- ((3
* (a
|^ 3))
* b))
+ ((3
* (a
|^ 2))
* (b
|^ 2))))
+ (((3
* (b
|^ 2))
* (a
|^ 2))
- ((3
* (b
|^ (2
+ 1)))
* a)))
+ ((
- ((b
|^ 3)
* a))
+ (b
|^ 4))) by
NEWTON: 6
.= (((((a
|^ 4)
- ((4
* (a
|^ 3))
* b))
+ ((6
* (a
|^ 2))
* (b
|^ 2)))
- ((4
* (b
|^ 3))
* a))
+ (b
|^ 4));
hence thesis;
end;
notation
let n be
Nat;
let r be
Real;
synonym n
-real-root r for n
-root r;
end
definition
let n be non
zero
Nat;
let z be
Complex;
::
POLYEQ_5:def1
func n
-root z ->
Complex equals ((n
-real-root
|.z.|)
* ((
cos ((
Arg z)
/ n))
+ ((
sin ((
Arg z)
/ n))
*
<i> )));
correctness ;
end
reserve z for
Complex;
reserve n0 for non
zero
Nat;
theorem ::
POLYEQ_5:7
Th7: ((n0
-root z)
|^ n0)
= z
proof
reconsider n = n0 as
Element of
NAT by
ORDINAL1:def 12;
thus ((n0
-root z)
|^ n0)
= ((((n
-real-root
|.z.|)
* (
cos (((
Arg z)
+ ((2
*
PI )
*
0 ))
/ n)))
+ (((n
-real-root
|.z.|)
* (
sin (((
Arg z)
+ ((2
*
PI )
*
0 ))
/ n)))
*
<i> ))
|^ n)
.= z by
POLYEQ_3: 34;
end;
theorem ::
POLYEQ_5:8
Th8: for r be
Real st r
>=
0 holds (n0
-root r)
= (n0
-real-root r)
proof
let r be
Real;
reconsider r9 = r as
Real;
assume
A1: r
>=
0 ;
then (
Arg r9)
=
0 by
COMPTRIG: 35;
hence thesis by
A1,
COMPLEX1: 43,
SIN_COS: 31;
end;
theorem ::
POLYEQ_5:9
Th9: for r be
Real st r
>
0 holds (n0
-root (z
/ r))
= ((n0
-root z)
/ (n0
-root r))
proof
let r be
Real;
reconsider r9 = (1
/ r) as
Real;
reconsider n = n0 as
Element of
NAT by
ORDINAL1:def 12;
A1: n
>= (
0
+ 1) by
NAT_1: 13;
assume
A2: r
>
0 ;
then
A3:
|.r.|
>
0 by
COMPLEX1: 47;
(z
/ r)
= (z
* (1
/ r)) & (
Arg (z
* r9))
= (
Arg z) by
A2,
COMPLEX2: 27,
XCMPLX_1: 99;
hence (n0
-root (z
/ r))
= ((n
-real-root (
|.z.|
/
|.r.|))
* ((
cos ((
Arg z)
/ n))
+ ((
sin ((
Arg z)
/ n))
*
<i> ))) by
COMPLEX1: 67
.= (((n
-real-root
|.z.|)
/ (n
-real-root
|.r.|))
* ((
cos ((
Arg z)
/ n))
+ ((
sin ((
Arg z)
/ n))
*
<i> ))) by
A3,
A1,
COMPLEX1: 46,
POWER: 13
.= (((
cos ((
Arg z)
/ n))
+ ((
sin ((
Arg z)
/ n))
*
<i> ))
/ ((n
-real-root
|.r.|)
/ (n
-real-root
|.z.|))) by
XCMPLX_1: 79
.= (((n
-real-root
|.z.|)
* ((
cos ((
Arg z)
/ n))
+ ((
sin ((
Arg z)
/ n))
*
<i> )))
/ (n
-real-root
|.r.|)) by
XCMPLX_1: 77
.= ((n0
-root z)
/ (n
-real-root r)) by
A2,
COMPLEX1: 43
.= ((n0
-root z)
/ (n0
-root r)) by
A2,
Th8;
end;
theorem ::
POLYEQ_5:10
Th10: (z
|^ 2)
= a iff z
= (2
-root a) or z
= (
- (2
-root a))
proof
A1: a
= ((2
-root a)
|^ 2) by
Th7
.= ((2
-root a)
* (2
-root a)) by
Th1;
hereby
assume (z
|^ 2)
= a;
then
A2: (z
* z)
= a by
Th1;
assume not z
= (2
-root a);
then
A3: (z
- (2
-root a))
<>
0 ;
assume not z
= (
- (2
-root a));
then (z
+ (2
-root a))
<>
0 ;
then ((z
- (2
-root a))
* (z
+ (2
-root a)))
<>
0 by
A3;
hence contradiction by
A1,
A2;
end;
assume z
= (2
-root a) or z
= (
- (2
-root a));
then ((z
* z)
- ((2
-root a)
* (2
-root a)))
=
0 ;
hence (z
|^ 2)
= a by
A1,
Th1;
end;
begin
reserve a0,a1,a2,s1,s2 for
Complex;
theorem ::
POLYEQ_5:11
Th11: a1
= (
- (s1
+ s2)) & a0
= (s1
* s2) implies ((((z
|^ 2)
+ (a1
* z))
+ a0)
=
0 iff z
= s1 or z
= s2)
proof
assume a1
= (
- (s1
+ s2)) & a0
= (s1
* s2);
then
A1: ((z
- s1)
* (z
- s2))
= (((z
* z)
+ (a1
* z))
+ a0)
.= (((z
|^ 2)
+ (a1
* z))
+ a0) by
Th1;
hereby
assume (((z
|^ 2)
+ (a1
* z))
+ a0)
=
0 ;
then
A2: (z
- s1)
=
0 or (z
- s2)
=
0 by
A1;
assume not z
= s1;
hence z
= s2 by
A2;
end;
assume z
= s1 or z
= s2;
hence (((z
|^ 2)
+ (a1
* z))
+ a0)
=
0 by
A1;
end;
theorem ::
POLYEQ_5:12
Th12: a2
<>
0 implies ((((a2
* (z
|^ 2))
+ (a1
* z))
+ a0)
=
0 iff z
= ((
- (a1
/ (2
* a2)))
+ ((2
-root (
delta (a0,a1,a2)))
/ (2
* a2))) or z
= ((
- (a1
/ (2
* a2)))
- ((2
-root (
delta (a0,a1,a2)))
/ (2
* a2))))
proof
set s1 = ((
- (a1
/ (2
* a2)))
+ ((2
-root (
delta (a0,a1,a2)))
/ (2
* a2)));
set s2 = ((
- (a1
/ (2
* a2)))
- ((2
-root (
delta (a0,a1,a2)))
/ (2
* a2)));
A1: (
- (s1
+ s2))
= ((a1
/ (2
* a2))
+ (a1
/ (2
* a2)))
.= (((1
/ 2)
* (a1
/ a2))
+ (a1
/ (2
* a2))) by
XCMPLX_1: 103
.= (((1
/ 2)
* (a1
/ a2))
+ ((1
/ 2)
* (a1
/ a2))) by
XCMPLX_1: 103
.= (a1
/ a2);
assume
A2: a2
<>
0 ;
then (((a2
* (z
|^ 2))
+ (a1
* z))
+ a0)
= (((((a2
* (z
|^ 2))
+ (a1
* z))
+ a0)
/ a2)
* a2) by
XCMPLX_1: 87
.= (((((a2
* (z
|^ 2))
/ a2)
+ ((a1
* z)
/ a2))
+ (a0
/ a2))
* a2) by
XCMPLX_1: 63
.= ((((z
|^ 2)
+ ((a1
* z)
/ a2))
+ (a0
/ a2))
* a2) by
A2,
XCMPLX_1: 89
.= ((((z
|^ 2)
+ (a1
* (z
/ a2)))
+ (a0
/ a2))
* a2) by
XCMPLX_1: 74
.= ((((z
|^ 2)
+ (z
/ (a2
/ a1)))
+ (a0
/ a2))
* a2) by
XCMPLX_1: 81
.= ((((z
|^ 2)
+ ((a1
/ a2)
* z))
+ (a0
/ a2))
* a2) by
XCMPLX_1: 79;
then
A3: (((a2
* (z
|^ 2))
+ (a1
* z))
+ a0)
=
0 iff (((z
|^ 2)
+ ((a1
/ a2)
* z))
+ (a0
/ a2))
=
0 by
A2;
(s1
* s2)
= (((a1
/ (2
* a2))
* (a1
/ (2
* a2)))
- (((2
-root (
delta (a0,a1,a2)))
/ (2
* a2))
* ((2
-root (
delta (a0,a1,a2)))
/ (2
* a2))))
.= (((a1
* a1)
/ ((2
* a2)
* (2
* a2)))
- (((2
-root (
delta (a0,a1,a2)))
/ (2
* a2))
* ((2
-root (
delta (a0,a1,a2)))
/ (2
* a2)))) by
XCMPLX_1: 76
.= (((a1
* a1)
/ ((4
* a2)
* a2))
- (((2
-root (
delta (a0,a1,a2)))
* (2
-root (
delta (a0,a1,a2))))
/ ((2
* a2)
* (2
* a2)))) by
XCMPLX_1: 76
.= (((a1
* a1)
/ ((4
* a2)
* a2))
- (((2
-root (
delta (a0,a1,a2)))
|^ 2)
/ ((2
* a2)
* (2
* a2)))) by
Th1
.= (((a1
* a1)
/ ((4
* a2)
* a2))
- ((
delta (a0,a1,a2))
/ ((2
* a2)
* (2
* a2)))) by
Th7
.= (((a1
* a1)
- (
delta (a0,a1,a2)))
/ ((4
* a2)
* a2)) by
XCMPLX_1: 120
.= ((a0
* (4
* a2))
/ (a2
* (4
* a2)))
.= ((a0
/ a2)
* ((4
* a2)
/ (4
* a2))) by
XCMPLX_1: 76
.= ((a0
/ a2)
* 1) by
A2,
XCMPLX_1: 60
.= (a0
/ a2);
hence thesis by
A3,
A1,
Th11;
end;
begin
reserve a3,x,q,r,s,s3 for
Complex;
theorem ::
POLYEQ_5:13
Th13: z
= (x
- (a2
/ 3)) & q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) implies (((((z
|^ 3)
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 iff (((x
|^ 3)
+ ((3
* q)
* x))
- (2
* r))
=
0 )
proof
assume
A1: z
= (x
- (a2
/ 3));
then
A2: (3
* z)
= ((3
* x)
- a2);
A3: ((3
* x)
|^ 2)
= ((3
|^ 2)
* (x
|^ 2)) by
NEWTON: 7
.= ((3
* 3)
* (x
|^ 2)) by
Th1
.= (9
* (x
|^ 2));
A4: ((3
* x)
|^ 3)
= ((3
|^ 3)
* (x
|^ 3)) by
NEWTON: 7
.= (((3
* 3)
* 3)
* (x
|^ 3)) by
Th2
.= (27
* (x
|^ 3));
A5: (27
* (z
|^ 3))
= (((3
* 3)
* 3)
* (z
|^ 3))
.= ((3
|^ 3)
* (z
|^ 3)) by
Th2
.= (((3
* x)
- a2)
|^ 3) by
A2,
NEWTON: 7
.= ((((27
* (x
|^ 3))
- ((3
* (9
* (x
|^ 2)))
* a2))
+ ((3
* (a2
|^ 2))
* (3
* x)))
- (a2
|^ 3)) by
A4,
A3,
Th5
.= ((((27
* (x
|^ 3))
- ((27
* a2)
* (x
|^ 2)))
+ ((9
* (a2
|^ 2))
* x))
- (a2
|^ 3));
assume
A6: q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54);
A7: ((27
* a1)
* z)
= (((27
* a1)
* x)
- ((9
* a2)
* a1)) by
A1;
(((27
* 1)
* a2)
* (z
|^ 2))
= ((((3
* a2)
* (3
* 3))
* (1
* 1))
* (z
|^ 2))
.= (((3
* a2)
* (3
|^ 2))
* (z
|^ 2)) by
Th1
.= ((3
* a2)
* ((3
|^ 2)
* (z
|^ 2)))
.= ((3
* a2)
* ((3
* z)
|^ 2)) by
NEWTON: 7
.= ((3
* a2)
* ((((3
* x)
|^ 2)
- ((2
* (3
* x))
* a2))
+ (a2
|^ 2))) by
A2,
Th4
.= ((3
* a2)
* ((((3
* x)
* (3
* x))
- ((2
* (3
* x))
* a2))
+ (a2
|^ 2))) by
Th1
.= (((((27
* a2)
* x)
* x)
- (((2
* (3
* x))
* a2)
* (3
* a2)))
+ ((a2
|^ 2)
* (3
* a2)))
.= ((((27
* a2)
* (x
* x))
- ((18
* (a2
* a2))
* x))
+ ((3
* a2)
* (a2
* a2))) by
Th1
.= ((((27
* a2)
* (x
|^ 2))
- ((18
* (a2
* a2))
* x))
+ (((3
* a2)
* a2)
* a2)) by
Th1
.= ((((27
* a2)
* (x
|^ 2))
- ((18
* (a2
|^ 2))
* x))
+ (3
* ((a2
* a2)
* a2))) by
Th1
.= ((((27
* a2)
* (x
|^ 2))
- ((18
* (a2
|^ 2))
* x))
+ (3
* (a2
|^ 3))) by
Th2;
then (27
* ((((z
|^ 3)
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0))
= (((27
* (x
|^ 3))
+ (((
- (9
* (a2
|^ 2)))
+ (27
* a1))
* x))
+ (((2
* (a2
|^ 3))
- ((9
* a2)
* a1))
+ (27
* a0))) by
A5,
A7
.= (27
* (((x
|^ 3)
+ ((3
* q)
* x))
- (2
* r))) by
A6;
hence thesis;
end;
theorem ::
POLYEQ_5:14
Th14: a2
= (
- ((s1
+ s2)
+ s3)) & a1
= (((s1
* s2)
+ (s1
* s3))
+ (s2
* s3)) & a0
= (
- ((s1
* s2)
* s3)) implies (((((z
|^ 3)
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 iff z
= s1 or z
= s2 or z
= s3)
proof
assume a2
= (
- ((s1
+ s2)
+ s3)) & a1
= (((s1
* s2)
+ (s1
* s3))
+ (s2
* s3)) & a0
= (
- ((s1
* s2)
* s3));
then
A1: (((z
- s1)
* (z
- s2))
* (z
- s3))
= (((((z
* z)
* z)
+ ((a2
* z)
* z))
+ (a1
* z))
+ a0)
.= ((((z
|^ 3)
+ (a2
* (z
* z)))
+ (a1
* z))
+ a0) by
Th2
.= ((((z
|^ 3)
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0) by
Th1;
hereby
assume ((((z
|^ 3)
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 ;
then
A2: ((z
- s1)
* (z
- s2))
=
0 or (z
- s3)
=
0 by
A1;
assume ( not z
= s1) & not z
= s2;
then (z
- s1)
<>
0 & (z
- s2)
<>
0 ;
hence z
= s3 by
A2;
end;
assume z
= s1 or z
= s2 or z
= s3;
hence ((((z
|^ 3)
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 by
A1;
end;
theorem ::
POLYEQ_5:15
q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & q
<>
0 & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s
= (2
-root ((q
|^ 3)
+ (r
|^ 2))) & s1
= (3
-root (r
+ s)) & s2
= (
- (q
/ s1)) implies (((((z
|^ 3)
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 iff z
= ((s1
+ s2)
- (a2
/ 3)) or z
= (((
- ((s1
+ s2)
/ 2))
- (a2
/ 3))
+ ((((s1
- s2)
* (2
-root 3))
*
<i> )
/ 2)) or z
= (((
- ((s1
+ s2)
/ 2))
- (a2
/ 3))
- ((((s1
- s2)
* (2
-root 3))
*
<i> )
/ 2)))
proof
assume that
A1: q
= (((3
* a1)
- (a2
|^ 2))
/ 9) and
A2: q
<>
0 ;
assume
A3: r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54);
set t = ((s1
+ s2)
/ 2), d = ((s1
- s2)
/ 2);
set x = (z
+ (a2
/ 3));
set x1 = (2
* t), x2 = ((
- t)
+ ((d
* (2
-root 3))
*
<i> )), x3 = ((
- t)
- ((d
* (2
-root 3))
*
<i> ));
A4: (
- ((x1
+ x2)
+ x3))
=
0 ;
assume
A5: s
= (2
-root ((q
|^ 3)
+ (r
|^ 2)));
assume
A6: s1
= (3
-root (r
+ s));
A7: s1
<>
0
proof
assume s1
=
0 ;
then
A8:
0
= (s1
|^ 3) by
NEWTON: 11
.= (r
+ s) by
A6,
Th7;
((q
|^ 3)
+ (r
|^ 2))
= (s
|^ 2) by
A5,
Th7
.= (s
* s) by
Th1
.= ((
- s)
* (
- s))
.= (r
|^ 2) by
A8,
Th1;
then ((q
* q)
* q)
=
0 by
Th2;
hence contradiction by
A2;
end;
assume
A9: s2
= (
- (q
/ s1));
then
A10: ((s2
* s2)
* s2)
= (
- (((q
/ s1)
* (q
/ s1))
* (q
/ s1)))
.= (
- (((q
* q)
/ (s1
* s1))
* (q
/ s1))) by
XCMPLX_1: 76
.= (
- (((q
* q)
* q)
/ ((s1
* s1)
* s1))) by
XCMPLX_1: 76
.= (
- (((q
* q)
* q)
/ ((3
-root (r
+ s))
|^ 3))) by
A6,
Th2
.= (
- (((q
* q)
* q)
/ (r
+ s))) by
Th7
.= (
- ((q
|^ 3)
/ (r
+ s))) by
Th2;
A11: ((s1
* s1)
* s1)
= (s1
|^ 3) by
Th2
.= (r
+ s) by
A6,
Th7;
A12: (((x1
* x2)
+ (x1
* x3))
+ (x2
* x3))
= ((
- ((3
* t)
* t))
- (((d
* d)
* ((2
-root 3)
* (2
-root 3)))
* (
- 1)))
.= ((
- ((3
* t)
* t))
- (((d
* d)
* ((2
-root 3)
|^ 2))
* (
- 1))) by
Th1
.= ((
- ((3
* t)
* t))
- (((d
* d)
* 3)
* (
- 1))) by
Th7
.= (3
* (s1
* (q
/ s1))) by
A9
.= (3
* ((s1
* q)
/ s1)) by
XCMPLX_1: 74
.= (3
* q) by
A7,
XCMPLX_1: 89;
(
- ((x1
* x2)
* x3))
= ((
- (2
* t))
* ((t
* t)
- (((d
* d)
* ((2
-root 3)
* (2
-root 3)))
* (
- 1))))
.= ((
- (2
* t))
* ((t
* t)
- (((d
* d)
* ((2
-root 3)
|^ 2))
* (
- 1)))) by
Th1
.= ((
- (2
* t))
* ((t
* t)
- (((d
* d)
* 3)
* (
- 1)))) by
Th7
.= (
- ((r
+ s)
- ((q
|^ 3)
/ (r
+ s)))) by
A11,
A10
.= (
- ((((r
+ s)
* (r
+ s))
/ (r
+ s))
- ((q
|^ 3)
/ (r
+ s)))) by
A11,
A7,
XCMPLX_1: 89
.= (
- (((((r
* r)
+ ((2
* s)
* r))
+ (s
* s))
- (q
|^ 3))
/ (r
+ s))) by
XCMPLX_1: 120
.= (
- (((((r
* r)
+ ((2
* s)
* r))
+ ((2
-root ((q
|^ 3)
+ (r
|^ 2)))
|^ 2))
- (q
|^ 3))
/ (r
+ s))) by
A5,
Th1
.= (
- (((((r
* r)
+ ((2
* s)
* r))
+ ((q
|^ 3)
+ (r
|^ 2)))
- (q
|^ 3))
/ (r
+ s))) by
Th7
.= (
- ((((r
* r)
+ ((2
* s)
* r))
+ (r
|^ 2))
/ (r
+ s)))
.= (
- ((((r
* r)
+ ((2
* s)
* r))
+ (r
* r))
/ (r
+ s))) by
Th1
.= (
- (((2
* r)
* (r
+ s))
/ (r
+ s)))
.= (
- (2
* r)) by
A11,
A7,
XCMPLX_1: 89;
then
A13: ((((x
|^ 3)
+ (
0
* (x
|^ 2)))
+ ((3
* q)
* x))
+ (
- (2
* r)))
=
0 iff x
= x1 or x
= x2 or x
= x3 by
A4,
A12,
Th14;
z
= (x
- (a2
/ 3));
then ((((z
|^ 3)
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 iff (((x
|^ 3)
+ ((3
* q)
* x))
- (2
* r))
=
0 by
A1,
A3,
Th13;
hence thesis by
A13;
end;
theorem ::
POLYEQ_5:16
q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & q
=
0 & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) implies (((((z
|^ 3)
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 iff z
= (s1
- (a2
/ 3)) or z
= (((
- (s1
/ 2))
- (a2
/ 3))
+ (((s1
* (2
-root 3))
*
<i> )
/ 2)) or z
= (((
- (s1
/ 2))
- (a2
/ 3))
- (((s1
* (2
-root 3))
*
<i> )
/ 2)))
proof
assume that
A1: q
= (((3
* a1)
- (a2
|^ 2))
/ 9) and
A2: q
=
0 ;
set t = (s1
/ 2);
set x1 = (2
* t), x2 = ((
- t)
+ ((t
* (2
-root 3))
*
<i> )), x3 = ((
- t)
- ((t
* (2
-root 3))
*
<i> ));
A3: (((x1
* x2)
+ (x1
* x3))
+ (x2
* x3))
= ((
- ((3
* t)
* t))
- (((t
* t)
* ((2
-root 3)
* (2
-root 3)))
* (
- 1)))
.= ((
- ((3
* t)
* t))
- (((t
* t)
* ((2
-root 3)
|^ 2))
* (
- 1))) by
Th1
.= ((
- ((3
* t)
* t))
- (((t
* t)
* 3)
* (
- 1))) by
Th7
.= (3
* q) by
A2;
set x = (z
+ (a2
/ 3));
assume
A4: r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54);
assume
A5: s1
= (3
-root (2
* r));
A6: (
- ((x1
+ x2)
+ x3))
=
0 ;
A7: ((s1
* s1)
* s1)
= (s1
|^ 3) by
Th2
.= (2
* r) by
A5,
Th7;
(
- ((x1
* x2)
* x3))
= ((
- (2
* t))
* ((t
* t)
- (((t
* t)
* ((2
-root 3)
* (2
-root 3)))
* (
- 1))))
.= ((
- (2
* t))
* ((t
* t)
- (((t
* t)
* ((2
-root 3)
|^ 2))
* (
- 1)))) by
Th1
.= ((
- (2
* t))
* ((t
* t)
- (((t
* t)
* 3)
* (
- 1)))) by
Th7
.= (
- (2
* r)) by
A7;
then
A8: ((((x
|^ 3)
+ (
0
* (x
|^ 2)))
+ ((3
* q)
* x))
+ (
- (2
* r)))
=
0 iff x
= x1 or x
= x2 or x
= x3 by
A6,
A3,
Th14;
z
= (x
- (a2
/ 3));
then ((((z
|^ 3)
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 iff (((x
|^ 3)
+ ((3
* q)
* x))
- (2
* r))
=
0 by
A1,
A4,
Th13;
hence thesis by
A8;
end;
definition
let a0,a1,a2 be
Complex;
::
POLYEQ_5:def2
func
1_root_of_cubic (a0,a1,a2) ->
Complex means
:
Def2: ex r, s1 st r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) & it
= (s1
- (a2
/ 3)) if ((3
* a1)
- (a2
|^ 2))
=
0
otherwise ex q, r, s, s1, s2 st q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s
= (2
-root ((q
|^ 3)
+ (r
|^ 2))) & s1
= (3
-root (r
+ s)) & s2
= (
- (q
/ s1)) & it
= ((s1
+ s2)
- (a2
/ 3));
existence
proof
set q = (((3
* a1)
- (a2
|^ 2))
/ 9), r = (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54), s = (2
-root ((q
|^ 3)
+ (r
|^ 2))), s1 = (3
-root (r
+ s)), s2 = (
- (q
/ s1)), IT = ((s1
+ s2)
- (a2
/ 3));
thus ((3
* a1)
- (a2
|^ 2))
=
0 implies ex IT,r,s1 be
Complex st r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) & IT
= (s1
- (a2
/ 3))
proof
set r = (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54), s1 = (3
-root (2
* r)), IT = (s1
- (a2
/ 3));
assume ((3
* a1)
- (a2
|^ 2))
=
0 ;
take IT, r, s1;
thus thesis;
end;
assume ((3
* a1)
- (a2
|^ 2))
<>
0 ;
take IT, q, r, s, s1, s2;
thus thesis;
end;
uniqueness ;
correctness ;
::
POLYEQ_5:def3
func
2_root_of_cubic (a0,a1,a2) ->
Complex means
:
Def3: ex r, s1 st r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) & it
= (((
- (s1
/ 2))
- (a2
/ 3))
+ (((s1
* (2
-root 3))
*
<i> )
/ 2)) if ((3
* a1)
- (a2
|^ 2))
=
0
otherwise ex q, r, s, s1, s2 st q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s
= (2
-root ((q
|^ 3)
+ (r
|^ 2))) & s1
= (3
-root (r
+ s)) & s2
= (
- (q
/ s1)) & it
= (((
- ((s1
+ s2)
/ 2))
- (a2
/ 3))
+ ((((s1
- s2)
* (2
-root 3))
*
<i> )
/ 2));
existence
proof
set q = (((3
* a1)
- (a2
|^ 2))
/ 9), r = (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54), s = (2
-root ((q
|^ 3)
+ (r
|^ 2))), s1 = (3
-root (r
+ s)), s2 = (
- (q
/ s1)), IT = (((
- ((s1
+ s2)
/ 2))
- (a2
/ 3))
+ ((((s1
- s2)
* (2
-root 3))
*
<i> )
/ 2));
thus ((3
* a1)
- (a2
|^ 2))
=
0 implies ex IT,r,s1 be
Complex st r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) & IT
= (((
- (s1
/ 2))
- (a2
/ 3))
+ (((s1
* (2
-root 3))
*
<i> )
/ 2))
proof
set r = (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54), s1 = (3
-root (2
* r)), IT = (((
- (s1
/ 2))
- (a2
/ 3))
+ (((s1
* (2
-root 3))
*
<i> )
/ 2));
assume ((3
* a1)
- (a2
|^ 2))
=
0 ;
take IT, r, s1;
thus thesis;
end;
assume ((3
* a1)
- (a2
|^ 2))
<>
0 ;
take IT, q, r, s, s1, s2;
thus thesis;
end;
uniqueness ;
correctness ;
::
POLYEQ_5:def4
func
3_root_of_cubic (a0,a1,a2) ->
Complex means
:
Def4: ex r, s1 st r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) & it
= (((
- (s1
/ 2))
- (a2
/ 3))
- (((s1
* (2
-root 3))
*
<i> )
/ 2)) if ((3
* a1)
- (a2
|^ 2))
=
0
otherwise ex q, r, s, s1, s2 st q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s
= (2
-root ((q
|^ 3)
+ (r
|^ 2))) & s1
= (3
-root (r
+ s)) & s2
= (
- (q
/ s1)) & it
= (((
- ((s1
+ s2)
/ 2))
- (a2
/ 3))
- ((((s1
- s2)
* (2
-root 3))
*
<i> )
/ 2));
existence
proof
set q = (((3
* a1)
- (a2
|^ 2))
/ 9), r = (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54), s = (2
-root ((q
|^ 3)
+ (r
|^ 2))), s1 = (3
-root (r
+ s)), s2 = (
- (q
/ s1)), IT = (((
- ((s1
+ s2)
/ 2))
- (a2
/ 3))
- ((((s1
- s2)
* (2
-root 3))
*
<i> )
/ 2));
thus ((3
* a1)
- (a2
|^ 2))
=
0 implies ex IT,r,s1 be
Complex st r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) & IT
= (((
- (s1
/ 2))
- (a2
/ 3))
- (((s1
* (2
-root 3))
*
<i> )
/ 2))
proof
set r = (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54), s1 = (3
-root (2
* r)), IT = (((
- (s1
/ 2))
- (a2
/ 3))
- (((s1
* (2
-root 3))
*
<i> )
/ 2));
assume ((3
* a1)
- (a2
|^ 2))
=
0 ;
take IT, r, s1;
thus thesis;
end;
assume ((3
* a1)
- (a2
|^ 2))
<>
0 ;
take IT, q, r, s, s1, s2;
thus thesis;
end;
uniqueness ;
correctness ;
end
theorem ::
POLYEQ_5:17
Th17: (((
1_root_of_cubic (a0,a1,a2))
+ (
2_root_of_cubic (a0,a1,a2)))
+ (
3_root_of_cubic (a0,a1,a2)))
= (
- a2)
proof
per cases ;
suppose
A1: ((3
* a1)
- (a2
|^ 2))
=
0 ;
then
A2: ex r, s1 st r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) & (
3_root_of_cubic (a0,a1,a2))
= (((
- (s1
/ 2))
- (a2
/ 3))
- (((s1
* (2
-root 3))
*
<i> )
/ 2)) by
Def4;
(ex r, s1 st r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) & (
1_root_of_cubic (a0,a1,a2))
= (s1
- (a2
/ 3))) & ex r, s1 st r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) & (
2_root_of_cubic (a0,a1,a2))
= (((
- (s1
/ 2))
- (a2
/ 3))
+ (((s1
* (2
-root 3))
*
<i> )
/ 2)) by
A1,
Def2,
Def3;
hence thesis by
A2;
end;
suppose
A3: ((3
* a1)
- (a2
|^ 2))
<>
0 ;
then
A4: ex q, r, s, s1, s2 st q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s
= (2
-root ((q
|^ 3)
+ (r
|^ 2))) & s1
= (3
-root (r
+ s)) & s2
= (
- (q
/ s1)) & (
3_root_of_cubic (a0,a1,a2))
= (((
- ((s1
+ s2)
/ 2))
- (a2
/ 3))
- ((((s1
- s2)
* (2
-root 3))
*
<i> )
/ 2)) by
Def4;
(ex q, r, s, s1, s2 st q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s
= (2
-root ((q
|^ 3)
+ (r
|^ 2))) & s1
= (3
-root (r
+ s)) & s2
= (
- (q
/ s1)) & (
1_root_of_cubic (a0,a1,a2))
= ((s1
+ s2)
- (a2
/ 3))) & ex q, r, s, s1, s2 st q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s
= (2
-root ((q
|^ 3)
+ (r
|^ 2))) & s1
= (3
-root (r
+ s)) & s2
= (
- (q
/ s1)) & (
2_root_of_cubic (a0,a1,a2))
= (((
- ((s1
+ s2)
/ 2))
- (a2
/ 3))
+ ((((s1
- s2)
* (2
-root 3))
*
<i> )
/ 2)) by
A3,
Def2,
Def3;
hence thesis by
A4;
end;
end;
theorem ::
POLYEQ_5:18
Th18: ((((
1_root_of_cubic (a0,a1,a2))
* (
2_root_of_cubic (a0,a1,a2)))
+ ((
1_root_of_cubic (a0,a1,a2))
* (
3_root_of_cubic (a0,a1,a2))))
+ ((
2_root_of_cubic (a0,a1,a2))
* (
3_root_of_cubic (a0,a1,a2))))
= a1
proof
per cases ;
suppose
A1: ((3
* a1)
- (a2
|^ 2))
=
0 ;
set r = (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54), s1 = (3
-root (2
* r));
A2: (ex r, s1 st r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) & (
2_root_of_cubic (a0,a1,a2))
= (((
- (s1
/ 2))
- (a2
/ 3))
+ (((s1
* (2
-root 3))
*
<i> )
/ 2))) & ex r, s1 st r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) & (
3_root_of_cubic (a0,a1,a2))
= (((
- (s1
/ 2))
- (a2
/ 3))
- (((s1
* (2
-root 3))
*
<i> )
/ 2)) by
A1,
Def3,
Def4;
thus ((((
1_root_of_cubic (a0,a1,a2))
* (
2_root_of_cubic (a0,a1,a2)))
+ ((
1_root_of_cubic (a0,a1,a2))
* (
3_root_of_cubic (a0,a1,a2))))
+ ((
2_root_of_cubic (a0,a1,a2))
* (
3_root_of_cubic (a0,a1,a2))))
= (((
1_root_of_cubic (a0,a1,a2))
* ((
2_root_of_cubic (a0,a1,a2))
+ (
3_root_of_cubic (a0,a1,a2))))
+ ((
2_root_of_cubic (a0,a1,a2))
* (
3_root_of_cubic (a0,a1,a2))))
.= (((s1
- (a2
/ 3))
* ((((
- (s1
/ 2))
- (a2
/ 3))
+ (((s1
* (2
-root 3))
*
<i> )
/ 2))
+ (((
- (s1
/ 2))
- (a2
/ 3))
- (((s1
* (2
-root 3))
*
<i> )
/ 2))))
+ ((((
- (s1
/ 2))
- (a2
/ 3))
+ (((s1
* (2
-root 3))
*
<i> )
/ 2))
* (((
- (s1
/ 2))
- (a2
/ 3))
- (((s1
* (2
-root 3))
*
<i> )
/ 2)))) by
A1,
A2,
Def2
.= (((((
- (((3
* s1)
* s1)
/ 4))
- ((a2
* s1)
/ 3))
+ (((3
* a2)
* a2)
/ 9))
+ ((a2
* s1)
/ 3))
- (((((s1
* s1)
* ((2
-root 3)
* (2
-root 3)))
* (
- 1))
/ 2)
/ 2))
.= (((
- (((3
* s1)
* s1)
/ 4))
+ ((a2
* a2)
/ 3))
- (((((s1
* s1)
* ((2
-root 3)
|^ 2))
* (
- 1))
/ 2)
/ 2)) by
Th1
.= (((
- (((3
* s1)
* s1)
/ 4))
+ ((a2
* a2)
/ 3))
- (((((s1
* s1)
* 3)
* (
- 1))
/ 2)
/ 2)) by
Th7
.= ((a2
|^ 2)
/ 3) by
Th1
.= a1 by
A1;
end;
suppose
A3: ((3
* a1)
- (a2
|^ 2))
<>
0 ;
set q = (((3
* a1)
- (a2
|^ 2))
/ 9), r = (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54), s = (2
-root ((q
|^ 3)
+ (r
|^ 2))), s1 = (3
-root (r
+ s)), s2 = (
- (q
/ s1));
A4: s1
<>
0
proof
assume s1
=
0 ;
then
A5:
0
= (s1
|^ 3) by
NEWTON: 11
.= (r
+ s) by
Th7;
((q
|^ 3)
+ (r
|^ 2))
= (s
|^ 2) by
Th7
.= (s
* s) by
Th1
.= ((
- s)
* (
- s))
.= (r
|^ 2) by
A5,
Th1;
then ((q
* q)
* q)
=
0 by
Th2;
hence contradiction by
A3;
end;
A6: (ex q, r, s, s1, s2 st q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s
= (2
-root ((q
|^ 3)
+ (r
|^ 2))) & s1
= (3
-root (r
+ s)) & s2
= (
- (q
/ s1)) & (
2_root_of_cubic (a0,a1,a2))
= (((
- ((s1
+ s2)
/ 2))
- (a2
/ 3))
+ ((((s1
- s2)
* (2
-root 3))
*
<i> )
/ 2))) & ex q, r, s, s1, s2 st q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s
= (2
-root ((q
|^ 3)
+ (r
|^ 2))) & s1
= (3
-root (r
+ s)) & s2
= (
- (q
/ s1)) & (
3_root_of_cubic (a0,a1,a2))
= (((
- ((s1
+ s2)
/ 2))
- (a2
/ 3))
- ((((s1
- s2)
* (2
-root 3))
*
<i> )
/ 2)) by
A3,
Def3,
Def4;
set t = (s1
+ s2), d = (s1
- s2);
thus ((((
1_root_of_cubic (a0,a1,a2))
* (
2_root_of_cubic (a0,a1,a2)))
+ ((
1_root_of_cubic (a0,a1,a2))
* (
3_root_of_cubic (a0,a1,a2))))
+ ((
2_root_of_cubic (a0,a1,a2))
* (
3_root_of_cubic (a0,a1,a2))))
= (((
1_root_of_cubic (a0,a1,a2))
* ((
2_root_of_cubic (a0,a1,a2))
+ (
3_root_of_cubic (a0,a1,a2))))
+ ((
2_root_of_cubic (a0,a1,a2))
* (
3_root_of_cubic (a0,a1,a2))))
.= (((t
- (a2
/ 3))
* ((((
- (t
/ 2))
- (a2
/ 3))
+ (((d
* (2
-root 3))
*
<i> )
/ 2))
+ (((
- (t
/ 2))
- (a2
/ 3))
- (((d
* (2
-root 3))
*
<i> )
/ 2))))
+ ((((
- (t
/ 2))
- (a2
/ 3))
+ (((d
* (2
-root 3))
*
<i> )
/ 2))
* (((
- (t
/ 2))
- (a2
/ 3))
- (((d
* (2
-root 3))
*
<i> )
/ 2)))) by
A3,
A6,
Def2
.= (((((
- (((3
* t)
* t)
/ 4))
- ((a2
* t)
/ 3))
+ (((3
* a2)
* a2)
/ 9))
+ ((a2
* t)
/ 3))
- ((((d
* d)
* ((2
-root 3)
* (2
-root 3)))
* (
- 1))
/ 4))
.= (((
- (((3
* t)
* t)
/ 4))
+ ((a2
* a2)
/ 3))
- ((((d
* d)
* ((2
-root 3)
|^ 2))
* (
- 1))
/ 4)) by
Th1
.= (((
- (((3
* t)
* t)
/ 4))
+ ((a2
* a2)
/ 3))
- ((((d
* d)
* 3)
* (
- 1))
/ 4)) by
Th7
.= (((3
* s1)
* (q
/ s1))
+ ((a2
* a2)
/ 3))
.= ((3
* q)
+ ((a2
* a2)
/ 3)) by
A4,
XCMPLX_1: 90
.= ((3
* q)
+ ((a2
|^ 2)
/ 3)) by
Th1
.= a1;
end;
end;
theorem ::
POLYEQ_5:19
Th19: (((
1_root_of_cubic (a0,a1,a2))
* (
2_root_of_cubic (a0,a1,a2)))
* (
3_root_of_cubic (a0,a1,a2)))
= (
- a0)
proof
per cases ;
suppose
A1: ((3
* a1)
- (a2
|^ 2))
=
0 ;
set r = (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54), s1 = (3
-root (2
* r));
(ex r, s1 st r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) & (
2_root_of_cubic (a0,a1,a2))
= (((
- (s1
/ 2))
- (a2
/ 3))
+ (((s1
* (2
-root 3))
*
<i> )
/ 2))) & ex r, s1 st r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s1
= (3
-root (2
* r)) & (
3_root_of_cubic (a0,a1,a2))
= (((
- (s1
/ 2))
- (a2
/ 3))
- (((s1
* (2
-root 3))
*
<i> )
/ 2)) by
A1,
Def3,
Def4;
hence (((
1_root_of_cubic (a0,a1,a2))
* (
2_root_of_cubic (a0,a1,a2)))
* (
3_root_of_cubic (a0,a1,a2)))
= (((s1
- (a2
/ 3))
* (((
- (s1
/ 2))
- (a2
/ 3))
+ (((s1
* (2
-root 3))
*
<i> )
/ 2)))
* (((
- (s1
/ 2))
- (a2
/ 3))
- (((s1
* (2
-root 3))
*
<i> )
/ 2))) by
A1,
Def2
.= ((s1
- (a2
/ 3))
* ((((s1
/ 2)
+ (a2
/ 3))
* ((s1
/ 2)
+ (a2
/ 3)))
+ ((((((2
-root 3)
* (2
-root 3))
* s1)
* s1)
/ 2)
/ 2)))
.= ((s1
- (a2
/ 3))
* ((((s1
/ 2)
+ (a2
/ 3))
* ((s1
/ 2)
+ (a2
/ 3)))
+ ((((((2
-root 3)
|^ 2)
* s1)
* s1)
/ 2)
/ 2))) by
Th1
.= ((s1
- (a2
/ 3))
* ((((s1
/ 2)
+ (a2
/ 3))
* ((s1
/ 2)
+ (a2
/ 3)))
+ ((((3
* s1)
* s1)
/ 2)
/ 2))) by
Th7
.= (((s1
* s1)
* s1)
- (((((a2
* a2)
* a2)
/ 3)
/ 3)
/ 3))
.= ((s1
|^ 3)
- (((a2
* a2)
* a2)
/ 27)) by
Th2
.= ((2
* r)
- (((a2
* a2)
* a2)
/ 27)) by
Th7
.= ((((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 27)
- ((a2
|^ 3)
/ 27)) by
Th2
.= (((((3
* a2)
* a1)
- (a2
|^ (2
+ 1)))
/ 9)
- a0)
.= (((((3
* a2)
* a1)
- ((a2
|^ 2)
* a2))
/ 9)
- a0) by
NEWTON: 6
.= (
- a0) by
A1;
end;
suppose
A2: ((3
* a1)
- (a2
|^ 2))
<>
0 ;
set q = (((3
* a1)
- (a2
|^ 2))
/ 9), r = (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54), s = (2
-root ((q
|^ 3)
+ (r
|^ 2))), s1 = (3
-root (r
+ s)), s2 = (
- (q
/ s1));
A3: s1
<>
0
proof
assume s1
=
0 ;
then
A4:
0
= (s1
|^ 3) by
NEWTON: 11
.= (r
+ s) by
Th7;
((q
|^ 3)
+ (r
|^ 2))
= (s
|^ 2) by
Th7
.= (s
* s) by
Th1
.= ((
- s)
* (
- s))
.= (r
|^ 2) by
A4,
Th1;
then ((q
* q)
* q)
=
0 by
Th2;
hence contradiction by
A2;
end;
A5: ((s1
* s1)
* s1)
= (s1
|^ 3) by
Th2
.= (r
+ s) by
Th7;
then
A6: ((r
+ s)
- (((q
* q)
* q)
/ (r
+ s)))
= ((((r
+ s)
* (r
+ s))
/ (r
+ s))
- (((q
* q)
* q)
/ (r
+ s))) by
A3,
XCMPLX_1: 89
.= ((((r
+ s)
* (r
+ s))
- ((q
* q)
* q))
/ (r
+ s)) by
XCMPLX_1: 120
.= (((((r
* r)
+ ((2
* r)
* s))
+ (s
* s))
- (q
|^ 3))
/ (r
+ s)) by
Th2
.= (((((r
* r)
+ ((2
* r)
* s))
+ (s
|^ 2))
- (q
|^ 3))
/ (r
+ s)) by
Th1
.= (((((r
* r)
+ ((2
* r)
* s))
+ ((q
|^ 3)
+ (r
|^ 2)))
- (q
|^ 3))
/ (r
+ s)) by
Th7
.= ((((r
* r)
+ ((2
* r)
* s))
+ (r
|^ 2))
/ (r
+ s))
.= ((((r
* r)
+ ((2
* r)
* s))
+ (r
* r))
/ (r
+ s)) by
Th1
.= (((2
* r)
* (r
+ s))
/ (r
+ s))
.= (2
* r) by
A5,
A3,
XCMPLX_1: 89;
set t = (s1
+ s2), d = (s1
- s2);
A7: (s1
* s2)
= (
- ((q
/ s1)
* s1))
.= (
- q) by
A3,
XCMPLX_1: 87;
(ex q, r, s, s1, s2 st q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s
= (2
-root ((q
|^ 3)
+ (r
|^ 2))) & s1
= (3
-root (r
+ s)) & s2
= (
- (q
/ s1)) & (
2_root_of_cubic (a0,a1,a2))
= (((
- ((s1
+ s2)
/ 2))
- (a2
/ 3))
+ ((((s1
- s2)
* (2
-root 3))
*
<i> )
/ 2))) & ex q, r, s, s1, s2 st q
= (((3
* a1)
- (a2
|^ 2))
/ 9) & r
= (((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0))
/ 54) & s
= (2
-root ((q
|^ 3)
+ (r
|^ 2))) & s1
= (3
-root (r
+ s)) & s2
= (
- (q
/ s1)) & (
3_root_of_cubic (a0,a1,a2))
= (((
- ((s1
+ s2)
/ 2))
- (a2
/ 3))
- ((((s1
- s2)
* (2
-root 3))
*
<i> )
/ 2)) by
A2,
Def3,
Def4;
hence (((
1_root_of_cubic (a0,a1,a2))
* (
2_root_of_cubic (a0,a1,a2)))
* (
3_root_of_cubic (a0,a1,a2)))
= (((t
- (a2
/ 3))
* (((
- (t
/ 2))
- (a2
/ 3))
+ (((d
* (2
-root 3))
*
<i> )
/ 2)))
* (((
- (t
/ 2))
- (a2
/ 3))
- (((d
* (2
-root 3))
*
<i> )
/ 2))) by
A2,
Def2
.= ((t
- (a2
/ 3))
* ((((t
/ 2)
+ (a2
/ 3))
* ((t
/ 2)
+ (a2
/ 3)))
+ ((((((2
-root 3)
* (2
-root 3))
* d)
* d)
/ 2)
/ 2)))
.= ((t
- (a2
/ 3))
* ((((t
/ 2)
+ (a2
/ 3))
* ((t
/ 2)
+ (a2
/ 3)))
+ ((((((2
-root 3)
|^ 2)
* d)
* d)
/ 2)
/ 2))) by
Th1
.= ((t
- (a2
/ 3))
* ((((t
/ 2)
+ (a2
/ 3))
* ((t
/ 2)
+ (a2
/ 3)))
+ ((((3
* d)
* d)
/ 2)
/ 2))) by
Th7
.= (((((s1
* s1)
* s1)
+ ((s2
* s2)
* s2))
+ ((a2
* ((4
* s1)
* s2))
/ 4))
- (((a2
* a2)
* a2)
/ 27))
.= ((((s1
|^ 3)
+ ((s2
* s2)
* s2))
+ (a2
* (s1
* s2)))
- (((a2
* a2)
* a2)
/ 27)) by
Th2
.= ((((s1
|^ 3)
+ (((
- (q
/ s1))
* (
- (q
/ s1)))
* (
- (q
/ s1))))
+ (a2
* (
- q)))
- (((a2
* a2)
* a2)
/ 27)) by
A7
.= ((((s1
|^ 3)
- (((q
/ s1)
* (q
/ s1))
* (q
/ s1)))
- (a2
* q))
- (((a2
* a2)
* a2)
/ 27))
.= ((((s1
|^ 3)
- (((q
* q)
/ (s1
* s1))
* (q
/ s1)))
- (a2
* q))
- (((a2
* a2)
* a2)
/ 27)) by
XCMPLX_1: 76
.= ((((s1
|^ 3)
- (((q
* q)
* q)
/ ((s1
* s1)
* s1)))
- (a2
* q))
- (((a2
* a2)
* a2)
/ 27)) by
XCMPLX_1: 76
.= ((((s1
|^ 3)
- (((q
* q)
* q)
/ (s1
|^ 3)))
- (a2
* q))
- (((a2
* a2)
* a2)
/ 27)) by
Th2
.= ((((s1
|^ 3)
- (((q
* q)
* q)
/ (r
+ s)))
- (a2
* q))
- (((a2
* a2)
* a2)
/ 27)) by
Th7
.= ((((r
+ s)
- (((q
* q)
* q)
/ (r
+ s)))
- (a2
* q))
- (((a2
* a2)
* a2)
/ 27)) by
Th7
.= ((((2
* ((((9
* a2)
* a1)
- (2
* (a2
|^ 3)))
- (27
* a0)))
/ 54)
- (a2
* q))
- ((a2
|^ 3)
/ 27)) by
A6,
Th2
.= ((((((9
* a2)
* a1)
- (3
* (a2
|^ 3)))
/ 27)
- (a2
* q))
- a0)
.= ((((((9
* a2)
* a1)
- (3
* ((a2
* a2)
* a2)))
/ 27)
- (a2
* q))
- a0) by
Th2
.= ((((a2
* ((3
* a1)
- (a2
* a2)))
/ 9)
- (a2
* q))
- a0)
.= ((((a2
* ((3
* a1)
- (a2
|^ 2)))
/ 9)
- (a2
* q))
- a0) by
Th1
.= (
- a0);
end;
end;
theorem ::
POLYEQ_5:20
a3
<>
0 implies (((((a3
* (z
|^ 3))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 iff z
= (
1_root_of_cubic ((a0
/ a3),(a1
/ a3),(a2
/ a3))) or z
= (
2_root_of_cubic ((a0
/ a3),(a1
/ a3),(a2
/ a3))) or z
= (
3_root_of_cubic ((a0
/ a3),(a1
/ a3),(a2
/ a3))))
proof
assume
A1: a3
<>
0 ;
set s3 = (
3_root_of_cubic ((a0
/ a3),(a1
/ a3),(a2
/ a3)));
set s2 = (
2_root_of_cubic ((a0
/ a3),(a1
/ a3),(a2
/ a3)));
set s1 = (
1_root_of_cubic ((a0
/ a3),(a1
/ a3),(a2
/ a3)));
(
- (a2
/ a3))
= ((s1
+ s2)
+ s3) by
Th17;
then
A2: (a2
/ a3)
= (
- ((s1
+ s2)
+ s3));
(
- (a0
/ a3))
= ((s1
* s2)
* s3) by
Th19;
then
A3: (a0
/ a3)
= (
- ((s1
* s2)
* s3));
(((((z
|^ 3)
+ ((a2
/ a3)
* (z
|^ 2)))
+ ((a1
/ a3)
* z))
+ (a0
/ a3))
* a3)
= ((((a3
* (z
|^ 3))
+ (((a2
/ a3)
* a3)
* (z
|^ 2)))
+ (((a1
/ a3)
* a3)
* z))
+ ((a0
/ a3)
* a3))
.= ((((a3
* (z
|^ 3))
+ (((a2
/ a3)
* a3)
* (z
|^ 2)))
+ (((a1
/ a3)
* a3)
* z))
+ a0) by
A1,
XCMPLX_1: 87
.= ((((a3
* (z
|^ 3))
+ (((a2
/ a3)
* a3)
* (z
|^ 2)))
+ (a1
* z))
+ a0) by
A1,
XCMPLX_1: 87
.= ((((a3
* (z
|^ 3))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0) by
A1,
XCMPLX_1: 87;
then
A4: ((((z
|^ 3)
+ ((a2
/ a3)
* (z
|^ 2)))
+ ((a1
/ a3)
* z))
+ (a0
/ a3))
=
0 iff ((((a3
* (z
|^ 3))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 by
A1;
(a1
/ a3)
= (((s1
* s2)
+ (s1
* s3))
+ (s2
* s3)) by
Th18;
hence thesis by
A4,
A2,
A3,
Th14;
end;
begin
reserve a4,p,s4 for
Complex;
theorem ::
POLYEQ_5:21
Th21: z
= (x
- (a3
/ 4)) & p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) implies ((((((z
|^ 4)
+ (a3
* (z
|^ 3)))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 iff ((((x
|^ 4)
+ ((4
* p)
* (x
|^ 2)))
+ ((8
* q)
* x))
+ (4
* r))
=
0 )
proof
assume
A1: z
= (x
- (a3
/ 4));
then
A2: (4
* z)
= ((4
* x)
- a3);
A3: (16
* (z
|^ 2))
= ((4
* 4)
* (z
|^ 2))
.= ((4
|^ 2)
* (z
|^ 2)) by
Th1
.= ((4
* z)
|^ 2) by
NEWTON: 7
.= ((((4
* x)
|^ 2)
- ((2
* (4
* x))
* a3))
+ (a3
|^ 2)) by
A2,
Th4
.= ((((4
* x)
* (4
* x))
- ((2
* (4
* x))
* a3))
+ (a3
|^ 2)) by
Th1
.= (((16
* (x
* x))
- ((8
* x)
* a3))
+ (a3
|^ 2))
.= (((16
* (x
|^ 2))
- ((8
* x)
* a3))
+ (a3
|^ 2)) by
Th1;
A4: ((4
* x)
|^ 3)
= ((4
|^ 3)
* (x
|^ 3)) by
NEWTON: 7
.= (((4
* 4)
* 4)
* (x
|^ 3)) by
Th2
.= (64
* (x
|^ 3));
A5: ((4
* x)
|^ 2)
= ((4
|^ 2)
* (x
|^ 2)) by
NEWTON: 7
.= ((4
* 4)
* (x
|^ 2)) by
Th1
.= (16
* (x
|^ 2));
A6: ((4
* a3)
* (64
* (z
|^ 3)))
= ((4
* a3)
* (((4
* 4)
* 4)
* (z
|^ 3)))
.= ((4
* a3)
* ((4
|^ 3)
* (z
|^ 3))) by
Th2
.= ((4
* a3)
* (((4
* x)
- a3)
|^ 3)) by
A2,
NEWTON: 7
.= ((4
* a3)
* ((((64
* (x
|^ 3))
- ((3
* (16
* (x
|^ 2)))
* a3))
+ ((3
* (a3
|^ 2))
* (4
* x)))
- (a3
|^ 3))) by
A4,
A5,
Th5
.= (((((256
* a3)
* (x
|^ 3))
- ((192
* (a3
* a3))
* (x
|^ 2)))
+ ((48
* ((a3
|^ 2)
* a3))
* x))
- (4
* ((a3
|^ 3)
* a3)))
.= (((((256
* a3)
* (x
|^ 3))
- ((192
* (a3
|^ 2))
* (x
|^ 2)))
+ ((48
* ((a3
|^ 2)
* a3))
* x))
- (4
* ((a3
|^ 3)
* a3))) by
Th1
.= (((((256
* a3)
* (x
|^ 3))
- ((192
* (a3
|^ 2))
* (x
|^ 2)))
+ ((48
* (a3
|^ (2
+ 1)))
* x))
- (4
* ((a3
|^ 3)
* a3))) by
NEWTON: 6
.= (((((256
* a3)
* (x
|^ 3))
- ((192
* (a3
|^ 2))
* (x
|^ 2)))
+ ((48
* (a3
|^ 3))
* x))
- (4
* (a3
|^ (3
+ 1)))) by
NEWTON: 6
.= (((((256
* a3)
* (x
|^ 3))
- ((192
* (a3
|^ 2))
* (x
|^ 2)))
+ ((48
* (a3
|^ 3))
* x))
- (4
* (a3
|^ 4)));
A7: ((4
* x)
|^ 4)
= ((4
|^ 4)
* (x
|^ 4)) by
NEWTON: 7
.= ((((4
* 4)
* 4)
* 4)
* (x
|^ 4)) by
Th3
.= (256
* (x
|^ 4));
A8: (256
* (z
|^ 4))
= ((((4
* 4)
* 4)
* 4)
* (z
|^ 4))
.= ((4
|^ 4)
* (z
|^ 4)) by
Th3
.= (((4
* x)
- a3)
|^ 4) by
A2,
NEWTON: 7
.= (((((256
* (x
|^ 4))
- ((4
* (64
* (x
|^ 3)))
* a3))
+ ((6
* (16
* (x
|^ 2)))
* (a3
|^ 2)))
- ((4
* (a3
|^ 3))
* (4
* x)))
+ (a3
|^ 4)) by
A7,
A4,
A5,
Th6
.= (((((256
* (x
|^ 4))
- ((256
* (x
|^ 3))
* a3))
+ ((96
* (x
|^ 2))
* (a3
|^ 2)))
- ((16
* (a3
|^ 3))
* x))
+ (a3
|^ 4));
assume
A9: p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024);
(256
* (((((z
|^ 4)
+ (a3
* (z
|^ 3)))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0))
= (((((256
* (z
|^ 4))
+ ((4
* a3)
* (64
* (z
|^ 3))))
+ ((16
* a2)
* (16
* (z
|^ 2))))
+ ((64
* a1)
* (4
* z)))
+ (256
* a0))
.= (((((((((256
* (x
|^ 4))
- ((256
* (x
|^ 3))
* a3))
+ ((96
* (x
|^ 2))
* (a3
|^ 2)))
- ((16
* (a3
|^ 3))
* x))
+ (a3
|^ 4))
+ (((((256
* a3)
* (x
|^ 3))
- ((192
* (a3
|^ 2))
* (x
|^ 2)))
+ ((48
* (a3
|^ 3))
* x))
- (4
* (a3
|^ 4))))
+ ((16
* a2)
* (((16
* (x
|^ 2))
- ((8
* x)
* a3))
+ (a3
|^ 2))))
+ ((64
* a1)
* ((4
* x)
- a3)))
+ (256
* a0)) by
A1,
A8,
A6,
A3
.= (256
* ((((x
|^ 4)
+ ((4
* p)
* (x
|^ 2)))
+ ((8
* q)
* x))
+ (4
* r))) by
A9;
hence thesis;
end;
theorem ::
POLYEQ_5:22
Th22: a3
= (
- (((s1
+ s2)
+ s3)
+ s4)) & a2
= ((((((s1
* s2)
+ (s1
* s3))
+ (s1
* s4))
+ (s2
* s3))
+ (s2
* s4))
+ (s3
* s4)) & a1
= (
- (((((s1
* s2)
* s3)
+ ((s1
* s2)
* s4))
+ ((s1
* s3)
* s4))
+ ((s2
* s3)
* s4))) & a0
= (((s1
* s2)
* s3)
* s4) implies ((((((z
|^ 4)
+ (a3
* (z
|^ 3)))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 iff z
= s1 or z
= s2 or z
= s3 or z
= s4)
proof
assume a3
= (
- (((s1
+ s2)
+ s3)
+ s4)) & a2
= ((((((s1
* s2)
+ (s1
* s3))
+ (s1
* s4))
+ (s2
* s3))
+ (s2
* s4))
+ (s3
* s4)) & a1
= (
- (((((s1
* s2)
* s3)
+ ((s1
* s2)
* s4))
+ ((s1
* s3)
* s4))
+ ((s2
* s3)
* s4))) & a0
= (((s1
* s2)
* s3)
* s4);
then
A1: ((((z
- s1)
* (z
- s2))
* (z
- s3))
* (z
- s4))
= (((((((z
* z)
* z)
* z)
+ (((a3
* z)
* z)
* z))
+ ((a2
* z)
* z))
+ (a1
* z))
+ a0)
.= (((((z
|^ 4)
+ (a3
* ((z
* z)
* z)))
+ ((a2
* z)
* z))
+ (a1
* z))
+ a0) by
Th3
.= (((((z
|^ 4)
+ (a3
* (z
|^ 3)))
+ (a2
* (z
* z)))
+ (a1
* z))
+ a0) by
Th2
.= (((((z
|^ 4)
+ (a3
* (z
|^ 3)))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0) by
Th1;
hereby
assume (((((z
|^ 4)
+ (a3
* (z
|^ 3)))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 ;
then
A2: (((z
- s1)
* (z
- s2))
* (z
- s3))
=
0 or (z
- s4)
=
0 by
A1;
assume that
A3: ( not z
= s1) & not z
= s2 and
A4: not z
= s3;
A5: (z
- s3)
<>
0 by
A4;
(z
- s1)
<>
0 & (z
- s2)
<>
0 by
A3;
hence z
= s4 by
A2,
A5;
end;
assume z
= s1 or z
= s2 or z
= s3 or z
= s4;
hence (((((z
|^ 4)
+ (a3
* (z
|^ 3)))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 by
A1;
end;
theorem ::
POLYEQ_5:23
Th23: q
<>
0 & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) implies (((((z
|^ 4)
+ ((4
* p)
* (z
|^ 2)))
+ ((8
* q)
* z))
+ (4
* r))
=
0 iff z
= ((s1
+ s2)
+ s3) or z
= ((s1
- s2)
- s3) or z
= (((
- s1)
+ s2)
- s3) or z
= (((
- s1)
- s2)
+ s3))
proof
set z1 = ((s1
+ s2)
+ s3), z2 = ((s1
- s2)
- s3), z3 = (((
- s1)
+ s2)
- s3), z4 = (((
- s1)
- s2)
+ s3);
assume q
<>
0 ;
then
A1: (q
* q)
<>
0 ;
assume
A2: s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))));
assume
A3: s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))));
A4: (s2
* s2)
= (s2
|^ 2) by
Th1
.= (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))) by
A3,
Th7;
A5: (s1
* s1)
= (s1
|^ 2) by
Th1
.= (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))) by
A2,
Th7;
then
A6: (((s1
* s1)
* (s2
* s2))
* (
3_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))))
= (
- (
- (q
|^ 2))) by
A4,
Th19;
then
A7: ((s1
* s1)
* (s2
* s2))
<>
0 by
A1,
Th1;
((s1
* s2)
* (s1
* s2))
<>
0 by
A1,
A6,
Th1;
then
A8: (s1
* s2)
<>
0 ;
assume
A9: s3
= (
- (q
/ (s1
* s2)));
then
A10: (
- (((((z1
* z2)
* z3)
+ ((z1
* z2)
* z4))
+ ((z1
* z3)
* z4))
+ ((z2
* z3)
* z4)))
= (
- ((8
* (s1
* s2))
* (
- (q
/ (s1
* s2)))))
.= (
- ((8
* (s1
* s2))
* ((
- q)
/ (s1
* s2)))) by
XCMPLX_1: 187
.= (
- (8
* ((s1
* s2)
* ((
- q)
/ (s1
* s2)))))
.= (
- (8
* ((
- q)
/ ((s1
* s2)
/ (s1
* s2))))) by
XCMPLX_1: 81
.= (
- (8
* ((
- q)
/ 1))) by
A8,
XCMPLX_1: 60
.= (8
* q);
A11: (s3
* s3)
= (((
- q)
/ (s1
* s2))
* (
- (q
/ (s1
* s2)))) by
A9,
XCMPLX_1: 187
.= (((
- q)
/ (s1
* s2))
* ((
- q)
/ (s1
* s2))) by
XCMPLX_1: 187
.= (((
- q)
* (
- q))
/ ((s1
* s2)
* (s1
* s2))) by
XCMPLX_1: 76
.= ((q
* q)
/ ((s1
* s1)
* (s2
* s2)))
.= (((
3_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))
* ((s1
* s1)
* (s2
* s2)))
/ ((s1
* s1)
* (s2
* s2))) by
A6,
Th1
.= (
3_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))) by
A7,
XCMPLX_1: 89;
then
A12: (((s1
* s1)
+ (s2
* s2))
+ (s3
* s3))
= (
- (2
* p)) by
A5,
A4,
Th17;
then
A13: (
- (((z1
+ z2)
+ z3)
+ z4))
=
0 & ((((((z1
* z2)
+ (z1
* z3))
+ (z1
* z4))
+ (z2
* z3))
+ (z2
* z4))
+ (z3
* z4))
= (4
* p);
(((z1
* z2)
* z3)
* z4)
= (((((s1
* s1)
+ (s2
* s2))
+ (s3
* s3))
* (((s1
* s1)
+ (s2
* s2))
+ (s3
* s3)))
- (4
* ((((s1
* s1)
* (s2
* s2))
+ ((s1
* s1)
* (s3
* s3)))
+ ((s2
* s2)
* (s3
* s3)))))
.= (((
- (2
* p))
* (
- (2
* p)))
- (4
* ((((s1
* s1)
* (s2
* s2))
+ ((s1
* s1)
* (s3
* s3)))
+ ((s2
* s2)
* (s3
* s3))))) by
A12
.= ((4
* (p
* p))
- (4
* ((p
|^ 2)
- r))) by
A5,
A4,
A11,
Th18
.= ((4
* (p
|^ 2))
- (4
* ((p
|^ 2)
- r))) by
Th1
.= (4
* r);
then (((((z
|^ 4)
+ (
0
* (z
|^ 3)))
+ ((4
* p)
* (z
|^ 2)))
+ ((8
* q)
* z))
+ (4
* r))
=
0 iff z
= z1 or z
= z2 or z
= z3 or z
= z4 by
A13,
A10,
Th22;
hence thesis;
end;
theorem ::
POLYEQ_5:24
p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & q
<>
0 & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) implies ((((((z
|^ 4)
+ (a3
* (z
|^ 3)))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 iff z
= (((s1
+ s2)
+ s3)
- (a3
/ 4)) or z
= (((s1
- s2)
- s3)
- (a3
/ 4)) or z
= ((((
- s1)
+ s2)
- s3)
- (a3
/ 4)) or z
= ((((
- s1)
- s2)
+ s3)
- (a3
/ 4)))
proof
assume
A1: p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32);
set x = (z
+ (a3
/ 4));
assume that
A2: q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) and
A3: q
<>
0 ;
assume
A4: r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024);
A5: z
= (x
- (a3
/ 4));
assume s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2)));
then ((((x
|^ 4)
+ ((4
* p)
* (x
|^ 2)))
+ ((8
* q)
* x))
+ (4
* r))
=
0 iff x
= ((s1
+ s2)
+ s3) or x
= ((s1
- s2)
- s3) or x
= (((
- s1)
+ s2)
- s3) or x
= (((
- s1)
- s2)
+ s3) by
A3,
Th23;
hence thesis by
A1,
A2,
A4,
A5,
Th21;
end;
theorem ::
POLYEQ_5:25
p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & q
=
0 & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) implies ((((((z
|^ 4)
+ (a3
* (z
|^ 3)))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 iff z
= ((2
-root (
- (2
* (p
- s1))))
- (a3
/ 4)) or z
= ((
- (2
-root (
- (2
* (p
- s1)))))
- (a3
/ 4)) or z
= ((2
-root (
- (2
* (p
+ s1))))
- (a3
/ 4)) or z
= ((
- (2
-root (
- (2
* (p
+ s1)))))
- (a3
/ 4)))
proof
assume
A1: p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32);
set x = (z
+ (a3
/ 4));
assume that
A2: q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) and
A3: q
=
0 ;
A4: z
= (x
- (a3
/ 4));
assume r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024);
then
A5: (((((z
|^ 4)
+ (a3
* (z
|^ 3)))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 iff ((((x
|^ 4)
+ ((4
* p)
* (x
|^ 2)))
+ ((8
* q)
* x))
+ (4
* r))
=
0 by
A1,
A2,
A4,
Th21;
assume
A6: s1
= (2
-root ((p
|^ 2)
- r));
set y = (x
|^ 2);
A7: (y
|^ 2)
= (x
|^ (2
* 2)) by
NEWTON: 9
.= (x
|^ 4);
A8: (x
|^ 2)
= ((
- (2
* p))
+ ((2
-root (
delta ((4
* r),(4
* p),1)))
/ 2)) iff x
= (2
-root ((
- (2
* p))
+ ((2
-root (
delta ((4
* r),(4
* p),1)))
/ 2))) or x
= (
- (2
-root ((
- (2
* p))
+ ((2
-root (
delta ((4
* r),(4
* p),1)))
/ 2)))) by
Th10;
A9: (x
|^ 2)
= ((
- (2
* p))
- ((2
-root (
delta ((4
* r),(4
* p),1)))
/ 2)) iff x
= (2
-root ((
- (2
* p))
- ((2
-root (
delta ((4
* r),(4
* p),1)))
/ 2))) or x
= (
- (2
-root ((
- (2
* p))
- ((2
-root (
delta ((4
* r),(4
* p),1)))
/ 2)))) by
Th10;
A10: (4
|^ 2)
= (4
* 4) by
Th1
.= 16;
(((1
* (y
|^ 2))
+ ((4
* p)
* y))
+ (4
* r))
=
0 iff y
= ((
- ((4
* p)
/ (2
* 1)))
+ ((2
-root (
delta ((4
* r),(4
* p),1)))
/ (2
* 1))) or y
= ((
- ((4
* p)
/ (2
* 1)))
- ((2
-root (
delta ((4
* r),(4
* p),1)))
/ (2
* 1))) by
Th12;
then
A11: (((1
* (y
|^ 2))
+ ((4
* p)
* y))
+ (4
* r))
=
0 iff z
= ((2
-root ((
- (2
* p))
+ ((2
-root (
delta ((4
* r),(4
* p),1)))
/ 2)))
- (a3
/ 4)) or z
= ((
- (2
-root ((
- (2
* p))
+ ((2
-root (
delta ((4
* r),(4
* p),1)))
/ 2))))
- (a3
/ 4)) or z
= ((2
-root ((
- (2
* p))
- ((2
-root (
delta ((4
* r),(4
* p),1)))
/ 2)))
- (a3
/ 4)) or z
= ((
- (2
-root ((
- (2
* p))
- ((2
-root (
delta ((4
* r),(4
* p),1)))
/ 2))))
- (a3
/ 4)) by
A8,
A9;
(2
-root 16)
= (2
-real-root 16) by
Th8
.= (2
-Root 16) by
POWER:def 1
.= 4 by
A10,
PREPOWER:def 2;
then ((2
-root (
delta ((4
* r),(4
* p),1)))
/ 4)
= (2
-root ((16
* ((p
* p)
- r))
/ 16)) by
Th9
.= s1 by
A6,
Th1;
hence thesis by
A3,
A5,
A7,
A11;
end;
definition
let a0,a1,a2,a3 be
Complex;
::
POLYEQ_5:def5
func
1_root_of_quartic (a0,a1,a2,a3) ->
Complex means
:
Def5: ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & it
= ((2
-root (
- (2
* (p
- s1))))
- (a3
/ 4)) if (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0
otherwise ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & it
= (((s1
+ s2)
+ s3)
- (a3
/ 4));
existence
proof
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), q = ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s2 = (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s3 = (
- (q
/ (s1
* s2))), IT = (((s1
+ s2)
+ s3)
- (a3
/ 4));
thus (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0 implies ex IT,p,r,s1 be
Complex st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & IT
= ((2
-root (
- (2
* (p
- s1))))
- (a3
/ 4))
proof
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root ((p
|^ 2)
- r)), IT = ((2
-root (
- (2
* (p
- s1))))
- (a3
/ 4));
assume (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0 ;
take IT, p, r, s1;
thus thesis;
end;
assume (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
<>
0 ;
take IT, p, q, r, s1, s2, s3;
thus thesis;
end;
uniqueness ;
correctness ;
::
POLYEQ_5:def6
func
2_root_of_quartic (a0,a1,a2,a3) ->
Complex means
:
Def6: ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & it
= ((
- (2
-root (
- (2
* (p
- s1)))))
- (a3
/ 4)) if (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0
otherwise ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & it
= ((((
- s1)
- s2)
+ s3)
- (a3
/ 4));
existence
proof
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), q = ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s2 = (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s3 = (
- (q
/ (s1
* s2))), IT = ((((
- s1)
- s2)
+ s3)
- (a3
/ 4));
thus (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0 implies ex IT,p,r,s1 be
Complex st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & IT
= ((
- (2
-root (
- (2
* (p
- s1)))))
- (a3
/ 4))
proof
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root ((p
|^ 2)
- r)), IT = ((
- (2
-root (
- (2
* (p
- s1)))))
- (a3
/ 4));
assume (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0 ;
take IT, p, r, s1;
thus thesis;
end;
assume (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
<>
0 ;
take IT, p, q, r, s1, s2, s3;
thus thesis;
end;
uniqueness ;
correctness ;
::
POLYEQ_5:def7
func
3_root_of_quartic (a0,a1,a2,a3) ->
Complex means
:
Def7: ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & it
= ((2
-root (
- (2
* (p
+ s1))))
- (a3
/ 4)) if (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0
otherwise ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & it
= ((((
- s1)
+ s2)
- s3)
- (a3
/ 4));
existence
proof
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), q = ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s2 = (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s3 = (
- (q
/ (s1
* s2))), IT = ((((
- s1)
+ s2)
- s3)
- (a3
/ 4));
thus (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0 implies ex IT,p,r,s1 be
Complex st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & IT
= ((2
-root (
- (2
* (p
+ s1))))
- (a3
/ 4))
proof
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root ((p
|^ 2)
- r)), IT = ((2
-root (
- (2
* (p
+ s1))))
- (a3
/ 4));
assume (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0 ;
take IT, p, r, s1;
thus thesis;
end;
assume (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
<>
0 ;
take IT, p, q, r, s1, s2, s3;
thus thesis;
end;
uniqueness ;
correctness ;
::
POLYEQ_5:def8
func
4_root_of_quartic (a0,a1,a2,a3) ->
Complex means
:
Def8: ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & it
= ((
- (2
-root (
- (2
* (p
+ s1)))))
- (a3
/ 4)) if (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0
otherwise ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & it
= (((s1
- s2)
- s3)
- (a3
/ 4));
existence
proof
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), q = ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s2 = (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s3 = (
- (q
/ (s1
* s2))), IT = (((s1
- s2)
- s3)
- (a3
/ 4));
thus (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0 implies ex IT,p,r,s1 be
Complex st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & IT
= ((
- (2
-root (
- (2
* (p
+ s1)))))
- (a3
/ 4))
proof
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root ((p
|^ 2)
- r)), IT = ((
- (2
-root (
- (2
* (p
+ s1)))))
- (a3
/ 4));
assume (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0 ;
take IT, p, r, s1;
thus thesis;
end;
assume (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
<>
0 ;
take IT, p, q, r, s1, s2, s3;
thus thesis;
end;
uniqueness ;
correctness ;
end
theorem ::
POLYEQ_5:26
Th26: ((((
1_root_of_quartic (a0,a1,a2,a3))
+ (
2_root_of_quartic (a0,a1,a2,a3)))
+ (
3_root_of_quartic (a0,a1,a2,a3)))
+ (
4_root_of_quartic (a0,a1,a2,a3)))
= (
- a3)
proof
per cases ;
suppose
A1: (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0 ;
then
A2: (ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
3_root_of_quartic (a0,a1,a2,a3))
= ((2
-root (
- (2
* (p
+ s1))))
- (a3
/ 4))) & ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
4_root_of_quartic (a0,a1,a2,a3))
= ((
- (2
-root (
- (2
* (p
+ s1)))))
- (a3
/ 4)) by
Def7,
Def8;
(ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
1_root_of_quartic (a0,a1,a2,a3))
= ((2
-root (
- (2
* (p
- s1))))
- (a3
/ 4))) & ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
2_root_of_quartic (a0,a1,a2,a3))
= ((
- (2
-root (
- (2
* (p
- s1)))))
- (a3
/ 4)) by
A1,
Def5,
Def6;
hence thesis by
A2;
end;
suppose
A3: (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
<>
0 ;
then
A4: (ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
3_root_of_quartic (a0,a1,a2,a3))
= ((((
- s1)
+ s2)
- s3)
- (a3
/ 4))) & ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
4_root_of_quartic (a0,a1,a2,a3))
= (((s1
- s2)
- s3)
- (a3
/ 4)) by
Def7,
Def8;
(ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
1_root_of_quartic (a0,a1,a2,a3))
= (((s1
+ s2)
+ s3)
- (a3
/ 4))) & ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
2_root_of_quartic (a0,a1,a2,a3))
= ((((
- s1)
- s2)
+ s3)
- (a3
/ 4)) by
A3,
Def5,
Def6;
hence thesis by
A4;
end;
end;
theorem ::
POLYEQ_5:27
Th27: (((((((
1_root_of_quartic (a0,a1,a2,a3))
* (
2_root_of_quartic (a0,a1,a2,a3)))
+ ((
1_root_of_quartic (a0,a1,a2,a3))
* (
3_root_of_quartic (a0,a1,a2,a3))))
+ ((
1_root_of_quartic (a0,a1,a2,a3))
* (
4_root_of_quartic (a0,a1,a2,a3))))
+ ((
2_root_of_quartic (a0,a1,a2,a3))
* (
3_root_of_quartic (a0,a1,a2,a3))))
+ ((
2_root_of_quartic (a0,a1,a2,a3))
* (
4_root_of_quartic (a0,a1,a2,a3))))
+ ((
3_root_of_quartic (a0,a1,a2,a3))
* (
4_root_of_quartic (a0,a1,a2,a3))))
= a2
proof
per cases ;
suppose
A1: (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0 ;
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root ((p
|^ 2)
- r));
set t1 = (2
-root (
- (2
* (p
- s1)))), t2 = (2
-root (
- (2
* (p
+ s1))));
A2: (ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
3_root_of_quartic (a0,a1,a2,a3))
= ((2
-root (
- (2
* (p
+ s1))))
- (a3
/ 4))) & ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
4_root_of_quartic (a0,a1,a2,a3))
= ((
- (2
-root (
- (2
* (p
+ s1)))))
- (a3
/ 4)) by
A1,
Def7,
Def8;
(ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
1_root_of_quartic (a0,a1,a2,a3))
= ((2
-root (
- (2
* (p
- s1))))
- (a3
/ 4))) & ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
2_root_of_quartic (a0,a1,a2,a3))
= ((
- (2
-root (
- (2
* (p
- s1)))))
- (a3
/ 4)) by
A1,
Def5,
Def6;
hence (((((((
1_root_of_quartic (a0,a1,a2,a3))
* (
2_root_of_quartic (a0,a1,a2,a3)))
+ ((
1_root_of_quartic (a0,a1,a2,a3))
* (
3_root_of_quartic (a0,a1,a2,a3))))
+ ((
1_root_of_quartic (a0,a1,a2,a3))
* (
4_root_of_quartic (a0,a1,a2,a3))))
+ ((
2_root_of_quartic (a0,a1,a2,a3))
* (
3_root_of_quartic (a0,a1,a2,a3))))
+ ((
2_root_of_quartic (a0,a1,a2,a3))
* (
4_root_of_quartic (a0,a1,a2,a3))))
+ ((
3_root_of_quartic (a0,a1,a2,a3))
* (
4_root_of_quartic (a0,a1,a2,a3))))
= (((((((4
+ 1)
+ 1)
* a3)
* a3)
/ 16)
- (t1
* t1))
- (t2
* t2)) by
A2
.= (((((3
* a3)
* a3)
/ 8)
- (t1
|^ 2))
- (t2
* t2)) by
Th1
.= (((((3
* a3)
* a3)
/ 8)
- (
- (2
* (p
- s1))))
- (t2
* t2)) by
Th7
.= (((((3
* a3)
* a3)
/ 8)
+ (2
* (p
- s1)))
- (t2
|^ 2)) by
Th1
.= (((((3
* a3)
* a3)
/ 8)
+ (2
* (p
- s1)))
- (
- (2
* (p
+ s1)))) by
Th7
.= ((((3
* a3)
* a3)
/ 8)
+ (((8
* a2)
- (3
* (a3
|^ 2)))
/ 8))
.= ((((3
* a3)
* a3)
/ 8)
+ (((8
* a2)
- (3
* (a3
* a3)))
/ 8)) by
Th1
.= a2;
end;
suppose
A3: (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
<>
0 ;
then
A4: (ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
3_root_of_quartic (a0,a1,a2,a3))
= ((((
- s1)
+ s2)
- s3)
- (a3
/ 4))) & ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
4_root_of_quartic (a0,a1,a2,a3))
= (((s1
- s2)
- s3)
- (a3
/ 4)) by
Def7,
Def8;
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), q = ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s2 = (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s3 = (
- (q
/ (s1
* s2)));
A5: (s2
* s2)
= (s2
|^ 2) by
Th1
.= (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))) by
Th7;
A6: (s1
* s1)
= (s1
|^ 2) by
Th1
.= (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))) by
Th7;
then
A7: (((s1
* s1)
* (s2
* s2))
* (
3_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))))
= (
- (
- (q
|^ 2))) by
A5,
Th19;
(q
* q)
<>
0 by
A3;
then
A8: ((s1
* s1)
* (s2
* s2))
<>
0 by
A7,
Th1;
A9: (s3
* s3)
= (((
- q)
/ (s1
* s2))
* (
- (q
/ (s1
* s2)))) by
XCMPLX_1: 187
.= (((
- q)
/ (s1
* s2))
* ((
- q)
/ (s1
* s2))) by
XCMPLX_1: 187
.= (((
- q)
* (
- q))
/ ((s1
* s2)
* (s1
* s2))) by
XCMPLX_1: 76
.= ((q
* q)
/ ((s1
* s1)
* (s2
* s2)))
.= (((
3_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))
* ((s1
* s1)
* (s2
* s2)))
/ ((s1
* s1)
* (s2
* s2))) by
A7,
Th1
.= (
3_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))) by
A8,
XCMPLX_1: 89;
(ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
1_root_of_quartic (a0,a1,a2,a3))
= (((s1
+ s2)
+ s3)
- (a3
/ 4))) & ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
2_root_of_quartic (a0,a1,a2,a3))
= ((((
- s1)
- s2)
+ s3)
- (a3
/ 4)) by
A3,
Def5,
Def6;
hence (((((((
1_root_of_quartic (a0,a1,a2,a3))
* (
2_root_of_quartic (a0,a1,a2,a3)))
+ ((
1_root_of_quartic (a0,a1,a2,a3))
* (
3_root_of_quartic (a0,a1,a2,a3))))
+ ((
1_root_of_quartic (a0,a1,a2,a3))
* (
4_root_of_quartic (a0,a1,a2,a3))))
+ ((
2_root_of_quartic (a0,a1,a2,a3))
* (
3_root_of_quartic (a0,a1,a2,a3))))
+ ((
2_root_of_quartic (a0,a1,a2,a3))
* (
4_root_of_quartic (a0,a1,a2,a3))))
+ ((
3_root_of_quartic (a0,a1,a2,a3))
* (
4_root_of_quartic (a0,a1,a2,a3))))
= ((
- (2
* (((s1
* s1)
+ (s2
* s2))
+ (s3
* s3))))
+ (((3
* a3)
* a3)
/ 8)) by
A4
.= ((
- (2
* (
- (2
* p))))
+ (((3
* a3)
* a3)
/ 8)) by
A6,
A5,
A9,
Th17
.= (((4
* ((8
* a2)
- (3
* (a3
|^ 2))))
/ 32)
+ (((3
* a3)
* a3)
/ 8))
.= (((4
* ((8
* a2)
- (3
* (a3
* a3))))
/ 32)
+ (((3
* a3)
* a3)
/ 8)) by
Th1
.= a2;
end;
end;
theorem ::
POLYEQ_5:28
Th28: ((((((
1_root_of_quartic (a0,a1,a2,a3))
* (
2_root_of_quartic (a0,a1,a2,a3)))
* (
3_root_of_quartic (a0,a1,a2,a3)))
+ (((
1_root_of_quartic (a0,a1,a2,a3))
* (
2_root_of_quartic (a0,a1,a2,a3)))
* (
4_root_of_quartic (a0,a1,a2,a3))))
+ (((
1_root_of_quartic (a0,a1,a2,a3))
* (
3_root_of_quartic (a0,a1,a2,a3)))
* (
4_root_of_quartic (a0,a1,a2,a3))))
+ (((
2_root_of_quartic (a0,a1,a2,a3))
* (
3_root_of_quartic (a0,a1,a2,a3)))
* (
4_root_of_quartic (a0,a1,a2,a3))))
= (
- a1)
proof
per cases ;
suppose
A1: (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0 ;
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root ((p
|^ 2)
- r));
set t1 = (2
-root (
- (2
* (p
- s1)))), t2 = (2
-root (
- (2
* (p
+ s1))));
A2: (ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
3_root_of_quartic (a0,a1,a2,a3))
= ((2
-root (
- (2
* (p
+ s1))))
- (a3
/ 4))) & ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
4_root_of_quartic (a0,a1,a2,a3))
= ((
- (2
-root (
- (2
* (p
+ s1)))))
- (a3
/ 4)) by
A1,
Def7,
Def8;
(ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
1_root_of_quartic (a0,a1,a2,a3))
= ((2
-root (
- (2
* (p
- s1))))
- (a3
/ 4))) & ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
2_root_of_quartic (a0,a1,a2,a3))
= ((
- (2
-root (
- (2
* (p
- s1)))))
- (a3
/ 4)) by
A1,
Def5,
Def6;
hence ((((((
1_root_of_quartic (a0,a1,a2,a3))
* (
2_root_of_quartic (a0,a1,a2,a3)))
* (
3_root_of_quartic (a0,a1,a2,a3)))
+ (((
1_root_of_quartic (a0,a1,a2,a3))
* (
2_root_of_quartic (a0,a1,a2,a3)))
* (
4_root_of_quartic (a0,a1,a2,a3))))
+ (((
1_root_of_quartic (a0,a1,a2,a3))
* (
3_root_of_quartic (a0,a1,a2,a3)))
* (
4_root_of_quartic (a0,a1,a2,a3))))
+ (((
2_root_of_quartic (a0,a1,a2,a3))
* (
3_root_of_quartic (a0,a1,a2,a3)))
* (
4_root_of_quartic (a0,a1,a2,a3))))
= ((((
- (t1
* t1))
+ ((a3
* a3)
/ 16))
* (
- (a3
/ 2)))
+ (((
- (t2
* t2))
+ ((a3
* a3)
/ 16))
* (
- (a3
/ 2)))) by
A2
.= ((((
- (t1
|^ 2))
+ ((a3
* a3)
/ 16))
* (
- (a3
/ 2)))
+ (((
- (t2
* t2))
+ ((a3
* a3)
/ 16))
* (
- (a3
/ 2)))) by
Th1
.= ((((
- (t1
|^ 2))
+ ((a3
* a3)
/ 16))
* (
- (a3
/ 2)))
+ (((
- (t2
|^ 2))
+ ((a3
* a3)
/ 16))
* (
- (a3
/ 2)))) by
Th1
.= ((((
- (
- (2
* (p
- s1))))
+ ((a3
* a3)
/ 16))
* (
- (a3
/ 2)))
+ (((
- (t2
|^ 2))
+ ((a3
* a3)
/ 16))
* (
- (a3
/ 2)))) by
Th7
.= ((((
- (
- (2
* (p
- s1))))
+ ((a3
* a3)
/ 16))
* (
- (a3
/ 2)))
+ (((
- (
- (2
* (p
+ s1))))
+ ((a3
* a3)
/ 16))
* (
- (a3
/ 2)))) by
Th7
.= (((a2
- ((3
* (a3
|^ 2))
/ 8))
+ ((a3
* a3)
/ 8))
* (
- (a3
/ 2)))
.= (((a2
- ((3
* (a3
* a3))
/ 8))
+ ((a3
* a3)
/ 8))
* (
- (a3
/ 2))) by
Th1
.= ((((a3
* a3)
* a3)
/ 8)
- ((a2
* a3)
/ 2))
.= (((a3
|^ 3)
/ 8)
- (((4
* a2)
* a3)
/ 8)) by
Th2
.= (
- a1) by
A1;
end;
suppose
A3: (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
<>
0 ;
then
A4: (ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
3_root_of_quartic (a0,a1,a2,a3))
= ((((
- s1)
+ s2)
- s3)
- (a3
/ 4))) & ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
4_root_of_quartic (a0,a1,a2,a3))
= (((s1
- s2)
- s3)
- (a3
/ 4)) by
Def7,
Def8;
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), q = ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s2 = (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s3 = (
- (q
/ (s1
* s2)));
A5: (s2
* s2)
= (s2
|^ 2) by
Th1
.= (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))) by
Th7;
A6: (s1
* s1)
= (s1
|^ 2) by
Th1
.= (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))) by
Th7;
then
A7: (((s1
* s1)
* (s2
* s2))
* (
3_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))))
= (
- (
- (q
|^ 2))) by
A5,
Th19;
A8: (q
* q)
<>
0 by
A3;
then
A9: ((s1
* s1)
* (s2
* s2))
<>
0 by
A7,
Th1;
((s1
* s2)
* (s1
* s2))
<>
0 by
A8,
A7,
Th1;
then
A10: (s1
* s2)
<>
0 ;
A11: (s3
* s3)
= (((
- q)
/ (s1
* s2))
* (
- (q
/ (s1
* s2)))) by
XCMPLX_1: 187
.= (((
- q)
/ (s1
* s2))
* ((
- q)
/ (s1
* s2))) by
XCMPLX_1: 187
.= (((
- q)
* (
- q))
/ ((s1
* s2)
* (s1
* s2))) by
XCMPLX_1: 76
.= ((q
* q)
/ ((s1
* s1)
* (s2
* s2)))
.= (((
3_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))
* ((s1
* s1)
* (s2
* s2)))
/ ((s1
* s1)
* (s2
* s2))) by
A7,
Th1
.= (
3_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))) by
A9,
XCMPLX_1: 89;
(ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
1_root_of_quartic (a0,a1,a2,a3))
= (((s1
+ s2)
+ s3)
- (a3
/ 4))) & ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
2_root_of_quartic (a0,a1,a2,a3))
= ((((
- s1)
- s2)
+ s3)
- (a3
/ 4)) by
A3,
Def5,
Def6;
hence ((((((
1_root_of_quartic (a0,a1,a2,a3))
* (
2_root_of_quartic (a0,a1,a2,a3)))
* (
3_root_of_quartic (a0,a1,a2,a3)))
+ (((
1_root_of_quartic (a0,a1,a2,a3))
* (
2_root_of_quartic (a0,a1,a2,a3)))
* (
4_root_of_quartic (a0,a1,a2,a3))))
+ (((
1_root_of_quartic (a0,a1,a2,a3))
* (
3_root_of_quartic (a0,a1,a2,a3)))
* (
4_root_of_quartic (a0,a1,a2,a3))))
+ (((
2_root_of_quartic (a0,a1,a2,a3))
* (
3_root_of_quartic (a0,a1,a2,a3)))
* (
4_root_of_quartic (a0,a1,a2,a3))))
= ((((((s1
* s1)
+ (s2
* s2))
+ (s3
* s3))
* a3)
- (((a3
* a3)
* a3)
/ 16))
+ (((8
* s1)
* s2)
* s3)) by
A4
.= ((((
- (2
* p))
* a3)
- (((a3
* a3)
* a3)
/ 16))
+ (((8
* s1)
* s2)
* (
- (q
/ (s1
* s2))))) by
A6,
A5,
A11,
Th17
.= ((((
- (((16
* a2)
/ 32)
* a3))
+ (((6
* (a3
|^ 2))
/ 32)
* a3))
- (((a3
* a3)
* a3)
/ 16))
- (((8
* s1)
* s2)
* (q
/ (s1
* s2))))
.= ((((
- ((a2
/ 2)
* a3))
+ (((6
* (a3
* a3))
/ 32)
* a3))
- (((a3
* a3)
* a3)
/ 16))
- (((8
* s1)
* s2)
* (q
/ (s1
* s2)))) by
Th1
.= (((
- ((a2
* a3)
/ 2))
+ ((((2
* a3)
* a3)
* a3)
/ 16))
- (8
* ((s1
* s2)
* (q
/ (s1
* s2)))))
.= (((
- ((a2
* a3)
/ 2))
+ ((((2
* a3)
* a3)
* a3)
/ 16))
- (8
* (q
/ ((s1
* s2)
/ (s1
* s2))))) by
XCMPLX_1: 81
.= (((
- ((a2
* a3)
/ 2))
+ ((((2
* a3)
* a3)
* a3)
/ 16))
- (8
* (q
/ 1))) by
A10,
XCMPLX_1: 60
.= (((
- a1)
+ ((((2
* a3)
* a3)
* a3)
/ 16))
- ((8
* (a3
|^ 3))
/ 64))
.= (((
- a1)
+ ((((2
* a3)
* a3)
* a3)
/ 16))
- ((8
* ((a3
* a3)
* a3))
/ 64)) by
Th2
.= (
- a1);
end;
end;
theorem ::
POLYEQ_5:29
Th29: ((((
1_root_of_quartic (a0,a1,a2,a3))
* (
2_root_of_quartic (a0,a1,a2,a3)))
* (
3_root_of_quartic (a0,a1,a2,a3)))
* (
4_root_of_quartic (a0,a1,a2,a3)))
= a0
proof
per cases ;
suppose
A1: (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
=
0 ;
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root ((p
|^ 2)
- r));
set t1 = (2
-root (
- (2
* (p
- s1)))), t2 = (2
-root (
- (2
* (p
+ s1))));
A2: (ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
3_root_of_quartic (a0,a1,a2,a3))
= ((2
-root (
- (2
* (p
+ s1))))
- (a3
/ 4))) & ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
4_root_of_quartic (a0,a1,a2,a3))
= ((
- (2
-root (
- (2
* (p
+ s1)))))
- (a3
/ 4)) by
A1,
Def7,
Def8;
(ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
1_root_of_quartic (a0,a1,a2,a3))
= ((2
-root (
- (2
* (p
- s1))))
- (a3
/ 4))) & ex p, r, s1 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root ((p
|^ 2)
- r)) & (
2_root_of_quartic (a0,a1,a2,a3))
= ((
- (2
-root (
- (2
* (p
- s1)))))
- (a3
/ 4)) by
A1,
Def5,
Def6;
hence ((((
1_root_of_quartic (a0,a1,a2,a3))
* (
2_root_of_quartic (a0,a1,a2,a3)))
* (
3_root_of_quartic (a0,a1,a2,a3)))
* (
4_root_of_quartic (a0,a1,a2,a3)))
= (((
- (t1
* t1))
+ ((a3
* a3)
/ 16))
* ((
- (t2
* t2))
+ ((a3
* a3)
/ 16))) by
A2
.= (((
- (t1
|^ 2))
+ ((a3
* a3)
/ 16))
* ((
- (t2
* t2))
+ ((a3
* a3)
/ 16))) by
Th1
.= (((
- (t1
|^ 2))
+ ((a3
* a3)
/ 16))
* ((
- (t2
|^ 2))
+ ((a3
* a3)
/ 16))) by
Th1
.= (((
- (
- (2
* (p
- s1))))
+ ((a3
* a3)
/ 16))
* ((
- (t2
|^ 2))
+ ((a3
* a3)
/ 16))) by
Th7
.= (((
- (
- (2
* (p
- s1))))
+ ((a3
* a3)
/ 16))
* ((
- (
- (2
* (p
+ s1))))
+ ((a3
* a3)
/ 16))) by
Th7
.= (((((4
* p)
* p)
+ (((((2
* 2)
* p)
* a3)
* a3)
/ 16))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16))
- (4
* (s1
* s1)))
.= (((((4
* p)
* p)
+ ((((4
* p)
* a3)
* a3)
/ 16))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16))
- (4
* (s1
|^ 2))) by
Th1
.= ((((4
* (p
* p))
+ ((((4
* p)
* a3)
* a3)
/ 16))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16))
- (4
* ((p
|^ 2)
- r))) by
Th7
.= ((((4
* (p
|^ 2))
+ ((((4
* p)
* a3)
* a3)
/ 16))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16))
- (4
* ((p
|^ 2)
- r))) by
Th1
.= (((((p
* a3)
* a3)
/ 4)
+ ((((a3
* a3)
* (a3
* a3))
/ 16)
/ 16))
+ (4
* r))
.= (((((p
* a3)
* a3)
/ 4)
+ ((((a3
* a3)
* (a3
|^ 2))
/ 16)
/ 16))
+ (4
* r)) by
Th1
.= (((((p
* a3)
* a3)
/ 4)
+ (((a3
* a3)
* (a3
|^ 2))
/ 256))
+ (((a0
- ((a3
* a1)
/ 4))
+ (((a3
|^ 2)
* a2)
/ 16))
- ((3
* (a3
|^ 4))
/ 256)))
.= (((((p
* a3)
* a3)
/ 4)
+ (((a3
* a3)
* (a3
|^ 2))
/ 256))
+ (((a0
- ((a3
* a1)
/ 4))
+ (((a3
|^ 2)
* a2)
/ 16))
- ((3
* (((a3
* a3)
* a3)
* a3))
/ 256))) by
Th3
.= (((((p
* a3)
* a3)
/ 4)
+ (((a3
* a3)
* (a3
|^ 2))
/ 256))
+ (((a0
- ((a3
* a1)
/ 4))
+ (((a3
|^ 2)
* a2)
/ 16))
- ((((3
* a3)
* a3)
* (a3
* a3))
/ 256)))
.= (((((p
* a3)
* a3)
/ 4)
+ (((a3
* a3)
* (a3
|^ 2))
/ 256))
+ (((a0
- ((a3
* a1)
/ 4))
+ (((a3
|^ 2)
* a2)
/ 16))
- ((((3
* a3)
* a3)
* (a3
|^ 2))
/ 256))) by
Th1
.= ((((a0
+ ((a2
* (a3
* a3))
/ 16))
- ((((4
* (a3
|^ 2))
* a3)
* a3)
/ 128))
- ((a3
* a1)
/ 4))
+ (((a3
|^ 2)
* a2)
/ 16))
.= ((((a0
+ ((a2
* (a3
|^ 2))
/ 16))
- ((((a3
|^ 2)
* a3)
* a3)
/ 32))
- ((a3
* a1)
/ 4))
+ (((a3
|^ 2)
* a2)
/ 16)) by
Th1
.= (((a0
+ (((2
* a2)
* (a3
|^ 2))
/ 16))
- ((((a3
|^ 2)
* a3)
* a3)
/ 32))
- ((a3
* a1)
/ 4))
.= (((a0
+ (((2
* a2)
* (a3
* a3))
/ 16))
- ((((a3
|^ 2)
* a3)
* a3)
/ 32))
- ((a3
* a1)
/ 4)) by
Th1
.= (((a0
+ ((((4
* a2)
* a3)
* a3)
/ 32))
- ((((a3
* a3)
* a3)
* a3)
/ 32))
- (((8
* a3)
* a1)
/ 32)) by
Th1
.= (a0
+ ((((((4
* a2)
* a3)
- ((a3
* a3)
* a3))
- (8
* a1))
* a3)
/ 32))
.= (a0
+ ((((((4
* a2)
* a3)
- (a3
|^ 3))
- (8
* a1))
* a3)
/ 32)) by
Th2
.= a0 by
A1;
end;
suppose
A3: (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
<>
0 ;
then
A4: (ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
3_root_of_quartic (a0,a1,a2,a3))
= ((((
- s1)
+ s2)
- s3)
- (a3
/ 4))) & ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
4_root_of_quartic (a0,a1,a2,a3))
= (((s1
- s2)
- s3)
- (a3
/ 4)) by
Def7,
Def8;
set p = (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32), q = ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64), r = (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024), s1 = (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s2 = (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))), s3 = (
- (q
/ (s1
* s2)));
A5: (s2
* s2)
= (s2
|^ 2) by
Th1
.= (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))) by
Th7;
set r1 = (s1
* s1), r2 = (s2
* s2), r3 = (s3
* s3);
A6: (s1
* s1)
= (s1
|^ 2) by
Th1
.= (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))) by
Th7;
then
A7: (((s1
* s1)
* (s2
* s2))
* (
3_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))))
= (
- (
- (q
|^ 2))) by
A5,
Th19;
A8: (q
* q)
<>
0 by
A3;
then ((s1
* s2)
* (s1
* s2))
<>
0 by
A7,
Th1;
then
A9: (s1
* s2)
<>
0 ;
A10: ((s1
* s1)
* (s2
* s2))
<>
0 by
A8,
A7,
Th1;
A11: (s3
* s3)
= (((
- q)
/ (s1
* s2))
* (
- (q
/ (s1
* s2)))) by
XCMPLX_1: 187
.= (((
- q)
/ (s1
* s2))
* ((
- q)
/ (s1
* s2))) by
XCMPLX_1: 187
.= (((
- q)
* (
- q))
/ ((s1
* s2)
* (s1
* s2))) by
XCMPLX_1: 76
.= ((q
* q)
/ ((s1
* s1)
* (s2
* s2)))
.= (((
3_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))
* ((s1
* s1)
* (s2
* s2)))
/ ((s1
* s1)
* (s2
* s2))) by
A7,
Th1
.= (
3_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p))) by
A10,
XCMPLX_1: 89;
then
A12: ((r1
+ r2)
+ r3)
= (
- (2
* p)) by
A6,
A5,
Th17;
(ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
1_root_of_quartic (a0,a1,a2,a3))
= (((s1
+ s2)
+ s3)
- (a3
/ 4))) & ex p, q, r, s1, s2, s3 st p
= (((8
* a2)
- (3
* (a3
|^ 2)))
/ 32) & q
= ((((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3))
/ 64) & r
= (((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4)))
/ 1024) & s1
= (2
-root (
1_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s2
= (2
-root (
2_root_of_cubic ((
- (q
|^ 2)),((p
|^ 2)
- r),(2
* p)))) & s3
= (
- (q
/ (s1
* s2))) & (
2_root_of_quartic (a0,a1,a2,a3))
= ((((
- s1)
- s2)
+ s3)
- (a3
/ 4)) by
A3,
Def5,
Def6;
hence ((((
1_root_of_quartic (a0,a1,a2,a3))
* (
2_root_of_quartic (a0,a1,a2,a3)))
* (
3_root_of_quartic (a0,a1,a2,a3)))
* (
4_root_of_quartic (a0,a1,a2,a3)))
= (((((((r1
+ r2)
+ r3)
* ((r1
+ r2)
+ r3))
- (4
* (((r1
* r2)
+ (r1
* r3))
+ (r2
* r3))))
- (((((r1
+ r2)
+ r3)
* a3)
* a3)
/ 8))
- ((((2
* s1)
* s2)
* s3)
* a3))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16)) by
A4
.= ((((((
- (2
* p))
* (
- (2
* p)))
- (4
* ((p
|^ 2)
- r)))
- ((((
- (2
* p))
* a3)
* a3)
/ 8))
- ((((2
* s1)
* s2)
* s3)
* a3))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16)) by
A6,
A5,
A11,
A12,
Th18
.= ((((((4
* p)
* p)
- (4
* ((p
|^ 2)
- r)))
+ ((((2
* p)
* a3)
* a3)
/ 8))
- ((((2
* s1)
* s2)
* s3)
* a3))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16))
.= ((((((4
* p)
* p)
- (4
* ((p
* p)
- r)))
+ ((((2
* p)
* a3)
* a3)
/ 8))
- ((((2
* s1)
* s2)
* s3)
* a3))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16)) by
Th1
.= ((((4
* r)
+ ((((2
* p)
* a3)
* a3)
/ 8))
+ ((2
* a3)
* ((s1
* s2)
* (q
/ (s1
* s2)))))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16))
.= ((((4
* r)
+ ((((2
* p)
* a3)
* a3)
/ 8))
+ ((2
* a3)
* (q
/ ((s1
* s2)
/ (s1
* s2)))))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16)) by
XCMPLX_1: 81
.= ((((4
* r)
+ ((((2
* p)
* a3)
* a3)
/ 8))
+ ((2
* a3)
* (q
/ 1)))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16)) by
A9,
XCMPLX_1: 60
.= (((((4
* ((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
|^ 2))
* a2))
- (3
* (a3
|^ 4))))
/ 1024)
+ ((((((8
* a2)
- (3
* (a3
|^ 2)))
/ 32)
* a3)
* a3)
/ 4))
+ (((2
* a3)
* (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3)))
/ 64))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16))
.= (((((4
* ((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
* a3))
* a2))
- (3
* (a3
|^ 4))))
/ 1024)
+ ((((((8
* a2)
- (3
* (a3
|^ 2)))
/ 32)
* a3)
* a3)
/ 4))
+ (((2
* a3)
* (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3)))
/ 64))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16)) by
Th1
.= (((((4
* ((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
* a3))
* a2))
- (3
* (a3
|^ 4))))
/ 1024)
+ ((((((8
* a2)
- (3
* (a3
* a3)))
/ 32)
* a3)
* a3)
/ 4))
+ (((2
* a3)
* (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3)))
/ 64))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16)) by
Th1
.= (((((4
* ((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
* a3))
* a2))
- (3
* (((a3
* a3)
* a3)
* a3))))
/ 1024)
+ ((((((8
* a2)
- (3
* (a3
* a3)))
/ 32)
* a3)
* a3)
/ 4))
+ (((2
* a3)
* (((8
* a1)
- ((4
* a2)
* a3))
+ (a3
|^ 3)))
/ 64))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16)) by
Th3
.= (((((4
* ((((256
* a0)
- ((64
* a3)
* a1))
+ ((16
* (a3
* a3))
* a2))
- (3
* (((a3
* a3)
* a3)
* a3))))
/ 1024)
+ ((((((8
* a2)
- (3
* (a3
* a3)))
/ 32)
* a3)
* a3)
/ 4))
+ (((2
* a3)
* (((8
* a1)
- ((4
* a2)
* a3))
+ ((a3
* a3)
* a3)))
/ 64))
+ (((((a3
* a3)
* a3)
* a3)
/ 16)
/ 16)) by
Th2
.= a0;
end;
end;
::$Notion-Name
theorem ::
POLYEQ_5:30
a4
<>
0 implies ((((((a4
* (z
|^ 4))
+ (a3
* (z
|^ 3)))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 iff z
= (
1_root_of_quartic ((a0
/ a4),(a1
/ a4),(a2
/ a4),(a3
/ a4))) or z
= (
2_root_of_quartic ((a0
/ a4),(a1
/ a4),(a2
/ a4),(a3
/ a4))) or z
= (
3_root_of_quartic ((a0
/ a4),(a1
/ a4),(a2
/ a4),(a3
/ a4))) or z
= (
4_root_of_quartic ((a0
/ a4),(a1
/ a4),(a2
/ a4),(a3
/ a4))))
proof
assume
A1: a4
<>
0 ;
set s4 = (
4_root_of_quartic ((a0
/ a4),(a1
/ a4),(a2
/ a4),(a3
/ a4)));
set s3 = (
3_root_of_quartic ((a0
/ a4),(a1
/ a4),(a2
/ a4),(a3
/ a4)));
set s2 = (
2_root_of_quartic ((a0
/ a4),(a1
/ a4),(a2
/ a4),(a3
/ a4)));
set s1 = (
1_root_of_quartic ((a0
/ a4),(a1
/ a4),(a2
/ a4),(a3
/ a4)));
(
- (a3
/ a4))
= (((s1
+ s2)
+ s3)
+ s4) by
Th26;
then
A2: (a3
/ a4)
= (
- (((s1
+ s2)
+ s3)
+ s4));
(
- (a1
/ a4))
= (((((s1
* s2)
* s3)
+ ((s1
* s2)
* s4))
+ ((s1
* s3)
* s4))
+ ((s2
* s3)
* s4)) by
Th28;
then
A3: (a1
/ a4)
= (
- (((((s1
* s2)
* s3)
+ ((s1
* s2)
* s4))
+ ((s1
* s3)
* s4))
+ ((s2
* s3)
* s4)));
((((((z
|^ 4)
+ ((a3
/ a4)
* (z
|^ 3)))
+ ((a2
/ a4)
* (z
|^ 2)))
+ ((a1
/ a4)
* z))
+ (a0
/ a4))
* a4)
= (((((a4
* (z
|^ 4))
+ (((a3
/ a4)
* a4)
* (z
|^ 3)))
+ (((a2
/ a4)
* a4)
* (z
|^ 2)))
+ (((a1
/ a4)
* a4)
* z))
+ ((a0
/ a4)
* a4))
.= (((((a4
* (z
|^ 4))
+ (((a3
/ a4)
* a4)
* (z
|^ 3)))
+ (((a2
/ a4)
* a4)
* (z
|^ 2)))
+ (((a1
/ a4)
* a4)
* z))
+ a0) by
A1,
XCMPLX_1: 87
.= (((((a4
* (z
|^ 4))
+ (((a3
/ a4)
* a4)
* (z
|^ 3)))
+ (((a2
/ a4)
* a4)
* (z
|^ 2)))
+ (a1
* z))
+ a0) by
A1,
XCMPLX_1: 87
.= (((((a4
* (z
|^ 4))
+ (((a3
/ a4)
* a4)
* (z
|^ 3)))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0) by
A1,
XCMPLX_1: 87
.= (((((a4
* (z
|^ 4))
+ (a3
* (z
|^ 3)))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0) by
A1,
XCMPLX_1: 87;
then
A4: (((((z
|^ 4)
+ ((a3
/ a4)
* (z
|^ 3)))
+ ((a2
/ a4)
* (z
|^ 2)))
+ ((a1
/ a4)
* z))
+ (a0
/ a4))
=
0 iff (((((a4
* (z
|^ 4))
+ (a3
* (z
|^ 3)))
+ (a2
* (z
|^ 2)))
+ (a1
* z))
+ a0)
=
0 by
A1;
(a2
/ a4)
= ((((((s1
* s2)
+ (s1
* s3))
+ (s1
* s4))
+ (s2
* s3))
+ (s2
* s4))
+ (s3
* s4)) & (a0
/ a4)
= (((s1
* s2)
* s3)
* s4) by
Th27,
Th29;
hence thesis by
A4,
A2,
A3,
Th22;
end;