let R be domRing; for a being Element of R
for F being non empty FinSequence of (Polynom-Ring R) st ( for k being Nat st k in dom F holds
F . k = rpoly (1,a) ) holds
for p being Polynomial of R st p = Product F holds
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )
let a be Element of R; for F being non empty FinSequence of (Polynom-Ring R) st ( for k being Nat st k in dom F holds
F . k = rpoly (1,a) ) holds
for p being Polynomial of R st p = Product F holds
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )
let F be non empty FinSequence of (Polynom-Ring R); ( ( for k being Nat st k in dom F holds
F . k = rpoly (1,a) ) implies for p being Polynomial of R st p = Product F holds
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )
assume AS1:
for k being Nat st k in dom F holds
F . k = rpoly (1,a)
; for p being Polynomial of R st p = Product F holds
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )
let p be Polynomial of R; ( p = Product F implies ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )
assume AS2:
p = Product F
; ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )
defpred S1[ Nat] means for F being FinSequence of (Polynom-Ring R) st len F = $1 & ( for k being Nat st k in dom F holds
F . k = rpoly (1,a) ) holds
for p being Polynomial of R st p = Product F holds
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} );
IA:
S1[1]
proof
now for F being FinSequence of (Polynom-Ring R) st len F = 1 & ( for k being Nat st k in dom F holds
F . k = rpoly (1,a) ) holds
for p being Polynomial of R st p = Product F holds
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )let F be
FinSequence of
(Polynom-Ring R);
( len F = 1 & ( for k being Nat st k in dom F holds
F . k = rpoly (1,a) ) implies for p being Polynomial of R st p = Product F holds
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )assume AS1:
(
len F = 1 & ( for
k being
Nat st
k in dom F holds
F . k = rpoly (1,
a) ) )
;
for p being Polynomial of R st p = Product F holds
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )let p be
Polynomial of
R;
( p = Product F implies ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )assume AS2:
p = Product F
;
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )B:
F = <*(F . 1)*>
by AS1, FINSEQ_1:40;
then A:
dom F = Seg 1
by FINSEQ_1:38;
then C:
F . 1
in rng F
by FUNCT_1:3, FINSEQ_1:3;
rng F c= the
carrier of
(Polynom-Ring R)
by FINSEQ_1:def 4;
then reconsider x =
F . 1 as
Element of the
carrier of
(Polynom-Ring R) by C;
thus p =
x
by AS2, B, GROUP_4:9
.=
rpoly (1,
a)
by A, AS1, FINSEQ_1:3
.=
(rpoly (1,a)) `^ (len F)
by AS1, POLYNOM5:16
;
Roots p = {a}then
p = rpoly (1,
a)
by AS1, POLYNOM5:16;
hence
Roots p = {a}
by ro4;
verum end;
hence
S1[1]
;
verum
end;
IS:
now for k being Nat st 1 <= k & S1[k] holds
S1[k + 1]let k be
Nat;
( 1 <= k & S1[k] implies S1[k + 1] )assume
1
<= k
;
( S1[k] implies S1[k + 1] )assume IV:
S1[
k]
;
S1[k + 1]now for F being FinSequence of (Polynom-Ring R) st len F = k + 1 & ( for i being Nat st i in dom F holds
F . i = rpoly (1,a) ) holds
for p being Polynomial of R st p = Product F holds
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )let F be
FinSequence of
(Polynom-Ring R);
( len F = k + 1 & ( for i being Nat st i in dom F holds
F . i = rpoly (1,a) ) implies for p being Polynomial of R st p = Product F holds
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )assume AS1:
(
len F = k + 1 & ( for
i being
Nat st
i in dom F holds
F . i = rpoly (1,
a) ) )
;
for p being Polynomial of R st p = Product F holds
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )let p be
Polynomial of
R;
( p = Product F implies ( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} ) )assume AS2:
p = Product F
;
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )consider G being
FinSequence of
(Polynom-Ring R),
x being
Element of
(Polynom-Ring R) such that A1:
F = G ^ <*x*>
by AS1, FINSEQ_2:19;
A3:
F . ((len G) + 1) = x
by A1, FINSEQ_1:42;
A4:
len F =
(len G) + (len <*x*>)
by A1, FINSEQ_1:22
.=
(len G) + 1
by FINSEQ_1:40
;
len F in Seg (len F)
by AS1, FINSEQ_1:3;
then
len F in dom F
by FINSEQ_1:def 3;
then A2:
x = rpoly (1,
a)
by AS1, A3, A4;
reconsider q =
Product G as
Polynomial of
R by POLYNOM3:def 10;
then A6:
(
q = (rpoly (1,a)) `^ (len G) &
Roots q = {a} )
by AS1, A4, IV;
A7:
p =
(Product G) * x
by AS2, A1, GROUP_4:6
.=
q *' (rpoly (1,a))
by A2, POLYNOM3:def 10
;
hence
p = (rpoly (1,a)) `^ (len F)
by A4, A6, POLYNOM5:19;
Roots p = {a}thus Roots p =
(Roots q) \/ (Roots (rpoly (1,a)))
by A7, UPROOTS:23
.=
{a} \/ {a}
by A6, ro4
.=
{a}
;
verum end; hence
S1[
k + 1]
;
verum end;
I:
for k being Nat st k >= 1 holds
S1[k]
from NAT_1:sch 8(IA, IS);
len F >= 1
by FINSEQ_1:20;
hence
( p = (rpoly (1,a)) `^ (len F) & Roots p = {a} )
by I, AS1, AS2; verum