let R be domRing; :: thesis: 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; :: thesis: 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 S_{1}[ 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: S_{1}[1]

S_{1}[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; :: thesis: verum

( p = q *' r & Roots q = Roots p )

let p be non zero with_roots Polynomial of R; :: thesis: 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 S

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: S

proof

let p be non zero with_roots Polynomial of R; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ex r being non with_roots Polynomial of R st

( p = q *' r & Roots q = Roots p )

take p1 ; :: thesis: ( p = q *' p1 & Roots q = Roots p )

thus q *' p1 = p by A2; :: thesis: Roots q = Roots p

thus Roots p = (Roots q) \/ (Roots p1) by A2, UPROOTS:23

.= Roots q ; :: thesis: verum

end;( p = q *' r & Roots q = Roots p ) )

assume AS: deg p = 1 ; :: thesis: 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 ; :: thesis: ex r being non with_roots Polynomial of R st

( p = q *' r & Roots q = Roots p )

take p1 ; :: thesis: ( p = q *' p1 & Roots q = Roots p )

thus q *' p1 = p by A2; :: thesis: Roots q = Roots p

thus Roots p = (Roots q) \/ (Roots p1) by A2, UPROOTS:23

.= Roots q ; :: thesis: verum

IS: now :: thesis: for k being Nat st 1 <= k & S_{1}[k] holds

S_{1}[k + 1]

I:
for k being Nat st 1 <= k holds S

let k be Nat; :: thesis: ( 1 <= k & S_{1}[k] implies S_{1}[k + 1] )

assume 1 <= k ; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume IV: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume 1 <= k ; :: thesis: ( S

assume IV: S

now :: thesis: 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 )

hence
Sex 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; :: thesis: ( 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 *' b_{3} & Roots r = Roots q ) )

assume AS1: deg p = k + 1 ; :: thesis: ex q being Ppoly of R, BRoots q ex r being non with_roots Polynomial of R st

( q = r *' b_{3} & 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;

end;( q = r *' b

assume AS1: deg p = k + 1 ; :: thesis: ex q being Ppoly of R, BRoots q ex r being non with_roots Polynomial of R st

( q = r *' b

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 )
;

end;

suppose A4:
not s is with_roots
; :: thesis: ex q being Ppoly of R, BRoots q ex r being non with_roots Polynomial of R st

( q = r *' b_{3} & Roots r = Roots q )

( q = r *' b

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; :: thesis: verum

end;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; :: thesis: verum

suppose
s is with_roots
; :: thesis: ex q being Ppoly of R, BRoots q ex r being non with_roots Polynomial of R st

( q = r *' b_{3} & Roots r = Roots q )

( q = r *' b

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; :: thesis: verum

end;( 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; :: thesis: verum

S

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; :: thesis: verum