let R be domRing; for p being Ppoly of R holds p is Ppoly of R, BRoots p
let p be Ppoly of R; p is Ppoly of R, BRoots p
defpred S1[ Nat] means for p being Ppoly of R st deg p = $1 holds
p is Ppoly of R, BRoots p;
IA:
S1[1]
proof
now for p being Ppoly of R st deg p = 1 holds
p is Ppoly of R, BRoots plet p be
Ppoly of
R;
( deg p = 1 implies p is Ppoly of R, BRoots p )assume A0:
deg p = 1
;
p is Ppoly of R, BRoots pconsider F being non
empty FinSequence of
(Polynom-Ring R) such that A1:
(
p = Product F & ( for
i being
Nat st
i in dom F holds
ex
a being
Element of
R st
F . i = rpoly (1,
a) ) )
by dpp1;
len F = 1
by A0, A1, lemppoly;
then A2:
F = <*(F . 1)*>
by FINSEQ_1:40;
then A3:
dom F = Seg 1
by FINSEQ_1:38;
then consider a being
Element of
R such that A4:
F . 1
= rpoly (1,
a)
by A1, FINSEQ_1:1;
reconsider e = 1 as
Element of
dom F by A3, FINSEQ_1:1;
A5:
Product F = F . e
by A2, GROUP_4:9;
rpoly (1,
a)
= <%(- a),(1. R)%>
by repr;
then
BRoots (rpoly (1,a)) = Bag {a}
by UPROOTS:54;
hence
p is
Ppoly of
R,
BRoots p
by A1, A4, A5, lemacf;
verum end;
hence
S1[1]
;
verum
end;
IS:
now for k being Nat st k >= 1 & S1[k] holds
S1[k + 1]let k be
Nat;
( k >= 1 & S1[k] implies S1[k + 1] )assume AS:
k >= 1
;
( S1[k] implies S1[k + 1] )assume IV:
S1[
k]
;
S1[k + 1]now for p being Ppoly of R st deg p = k + 1 holds
p is Ppoly of R, BRoots plet p be
Ppoly of
R;
( deg p = k + 1 implies p is Ppoly of R, BRoots p )assume B0:
deg p = k + 1
;
p is Ppoly of R, BRoots pconsider F being non
empty FinSequence of
(Polynom-Ring R) such that B1:
(
p = Product F & ( for
i being
Nat st
i in dom F holds
ex
a being
Element of
R st
F . i = rpoly (1,
a) ) )
by dpp1;
B1a:
len F = k + 1
by B0, B1, lemppoly;
consider G being
FinSequence,
y being
object such that B2:
F = G ^ <*y*>
by FINSEQ_1:46;
B2a:
rng G c= rng F
by B2, FINSEQ_1:29;
B2b:
rng F c= the
carrier of
(Polynom-Ring R)
by FINSEQ_1:def 4;
then reconsider G =
G as
FinSequence of
(Polynom-Ring R) by B2a, XBOOLE_1:1, FINSEQ_1:def 4;
B3:
len F =
(len G) + (len <*y*>)
by B2, FINSEQ_1:22
.=
(len G) + 1
by FINSEQ_1:39
;
then reconsider G =
G as non
empty FinSequence of
(Polynom-Ring R) by B1a, AS;
reconsider q =
Product G as
Polynomial of
R by POLYNOM3:def 10;
C:
dom G c= dom F
by B2, FINSEQ_1:26;
then reconsider q =
q as
Ppoly of
R by dpp1;
set B =
BRoots q;
deg q = k
by B1a, B3, D, lemppoly;
then reconsider q =
q as
Ppoly of
R,
BRoots q by IV;
rng <*y*> = {y}
by FINSEQ_1:39;
then G5:
y in rng <*y*>
by TARSKI:def 1;
rng <*y*> c= rng F
by B2, FINSEQ_1:30;
then
y in rng F
by G5;
then reconsider y =
y as
Element of
(Polynom-Ring R) by B2b;
dom <*y*> = {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
then
1
in dom <*y*>
by TARSKI:def 1;
then B6:
F . (k + 1) =
<*y*> . 1
by B2, B3, B1a, FINSEQ_1:def 7
.=
y
by FINSEQ_1:def 8
;
dom F = Seg (k + 1)
by B1a, FINSEQ_1:def 3;
then consider a being
Element of
R such that B9:
y = rpoly (1,
a)
by B1, B6, FINSEQ_1:4;
reconsider r =
y as
Ppoly of
R,
Bag {a} by lemacf, B9;
B10:
p =
(Product G) * y
by B1, B2, GROUP_4:6
.=
q *' r
by POLYNOM3:def 10
;
reconsider B1 =
(BRoots q) + (Bag {a}) as non
zero bag of the
carrier of
R ;
rpoly (1,
a)
= <%(- a),(1. R)%>
by repr;
then
BRoots (rpoly (1,a)) = Bag {a}
by UPROOTS:54;
then
BRoots p = (BRoots q) + (Bag {a})
by B9, B10, UPROOTS:56;
hence
p is
Ppoly of
R,
BRoots p
by B10, lemacf2;
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);
reconsider n = deg p as Element of NAT by INT_1:3;
n + 1 > 0 + 1
by RATFUNC1:def 2, XREAL_1:6;
then
n >= 1
by NAT_1:13;
hence
p is Ppoly of R, BRoots p
by I; verum