let R be domRing; for p being non zero with_roots Polynomial of R ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p )
let p be non zero with_roots Polynomial of R; ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p )
defpred S1[ Nat] means for p being non zero with_roots Polynomial of R st deg p = $1 holds
ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p );
IA:
S1[1]
proof
let p be non
zero with_roots Polynomial of
R;
( deg p = 1 implies ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p ) )
assume AS:
deg p = 1
;
ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p )
consider a being
Element of
R such that A1:
a is_a_root_of p
by POLYNOM5:def 8;
eval (
p,
a)
= 0. R
by A1, POLYNOM5:def 7;
then consider p1 being
Polynomial of
R such that A2:
p = (rpoly (1,a)) *' p1
by Th9, RING_4:1;
reconsider q =
rpoly (1,
a) as
Ppoly of
R by lemppoly1;
reconsider B =
BRoots p as non
zero bag of the
carrier of
R ;
(
p1 <> 0_. R &
rpoly (1,
a)
<> 0_. R )
by A2;
then deg p =
(deg (rpoly (1,a))) + (deg p1)
by A2, HURWITZ:23
.=
1
+ (deg p1)
by HURWITZ:27
;
then reconsider p1 =
p1 as non
with_roots Polynomial of
R by AS, HURWITZ:24;
reconsider p1 =
p1 as non
zero non
with_roots Polynomial of
R ;
A7:
rpoly (1,
a)
= <%(- a),(1. R)%>
by repr;
BRoots p =
(BRoots (rpoly (1,a))) + (BRoots p1)
by A2, UPROOTS:56
.=
(({a},1) -bag) + (BRoots p1)
by A7, UPROOTS:54
.=
(({a},1) -bag) + (EmptyBag the carrier of R)
by lemacf1
.=
Bag {a}
by PRE_POLY:53
;
then reconsider q =
rpoly (1,
a) as
Ppoly of
R,
BRoots p by lemacf;
take
q
;
ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p )
take
p1
;
( p = q *' p1 & Roots q = Roots p )
thus
q *' p1 = p
by A2;
Roots q = Roots p
thus Roots p =
(Roots q) \/ (Roots p1)
by A2, UPROOTS:23
.=
Roots q
;
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 p being non zero with_roots Polynomial of R st deg p = k + 1 holds
ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p )let p be non
zero with_roots Polynomial of
R;
( deg p = k + 1 implies ex q being Ppoly of R, BRoots q ex r being non with_roots Polynomial of R st
( q = r *' b3 & Roots r = Roots q ) )assume AS1:
deg p = k + 1
;
ex q being Ppoly of R, BRoots q ex r being non with_roots Polynomial of R st
( q = r *' b3 & Roots r = Roots q )consider a being
Element of
R such that A1:
a is_a_root_of p
by POLYNOM5:def 8;
consider s being
Polynomial of
R such that A2:
p = (rpoly (1,a)) *' s
by A1, HURWITZ:33;
reconsider s =
s as non
zero Polynomial of
R by A2;
per cases
( not s is with_roots or s is with_roots )
;
suppose A4:
not
s is
with_roots
;
ex q being Ppoly of R, BRoots q ex r being non with_roots Polynomial of R st
( q = r *' b3 & Roots r = Roots q )then A5:
Roots s = {}
;
reconsider q =
rpoly (1,
a) as
Ppoly of
R,
Bag {a} by lemacf;
A7:
rpoly (1,
a)
= <%(- a),(1. R)%>
by repr;
A6:
BRoots p =
(BRoots (rpoly (1,a))) + (BRoots s)
by A2, UPROOTS:56
.=
(BRoots (rpoly (1,a))) + (EmptyBag the carrier of R)
by A4, lemacf1
.=
BRoots (rpoly (1,a))
by PRE_POLY:53
.=
Bag {a}
by A7, UPROOTS:54
;
Roots p =
(Roots q) \/ (Roots s)
by A2, UPROOTS:23
.=
Roots q
by A5
;
hence
ex
q being
Ppoly of
R,
BRoots p ex
r being non
with_roots Polynomial of
R st
(
p = q *' r &
Roots q = Roots p )
by A2, A4, A6;
verum end; suppose
s is
with_roots
;
ex q being Ppoly of R, BRoots q ex r being non with_roots Polynomial of R st
( q = r *' b3 & Roots r = Roots q )then reconsider s =
s as non
zero with_roots Polynomial of
R ;
(
s <> 0_. R &
rpoly (1,
a)
<> 0_. R )
;
then deg p =
(deg (rpoly (1,a))) + (deg s)
by A2, HURWITZ:23
.=
1
+ (deg s)
by HURWITZ:27
;
then consider qs being
Ppoly of
R,
BRoots s,
rs being non
with_roots Polynomial of
R such that B1:
(
s = qs *' rs &
Roots qs = Roots s )
by AS1, IV;
reconsider rs =
rs as non
zero non
with_roots Polynomial of
R ;
set q =
(rpoly (1,a)) *' qs;
B2:
p = ((rpoly (1,a)) *' qs) *' rs
by A2, B1, POLYNOM3:33;
reconsider B =
(Bag {a}) + (BRoots s) as non
zero bag of the
carrier of
R ;
rpoly (1,
a) is
Ppoly of
R,
Bag {a}
by lemacf;
then reconsider q =
(rpoly (1,a)) *' qs as
Ppoly of
R,
B by lemacf2;
B7:
rpoly (1,
a)
= <%(- a),(1. R)%>
by repr;
B4:
BRoots p =
(BRoots q) + (BRoots rs)
by B2, UPROOTS:56
.=
(BRoots q) + (EmptyBag the carrier of R)
by lemacf1
.=
BRoots q
by PRE_POLY:53
.=
(BRoots (rpoly (1,a))) + (BRoots qs)
by UPROOTS:56
.=
(Bag {a}) + (BRoots qs)
by B7, UPROOTS:54
.=
B
by pf2
;
B3:
Roots p =
(Roots q) \/ (Roots rs)
by B2, UPROOTS:23
.=
Roots q
;
thus
ex
q being
Ppoly of
R,
BRoots p ex
r being non
with_roots Polynomial of
R st
(
p = q *' r &
Roots q = Roots p )
by B2, B3, B4;
verum end; end; hence
S1[
k + 1]
;
verum end;
I:
for k being Nat st 1 <= k holds
S1[k]
from NAT_1:sch 8(IA, IS);
K:
deg p >= 0 + 1
by INT_1:7, RATFUNC1:def 2;
p <> 0_. R
;
then
deg p is Element of NAT
by T8;
then consider d being Nat such that
H:
deg p = d
;
thus
ex q being Ppoly of R, BRoots p ex r being non with_roots Polynomial of R st
( p = q *' r & Roots q = Roots p )
by K, H, I; verum