begin
theorem
canceled;
theorem Th2:
theorem Th3:
begin
:: deftheorem defines canFS UPROOTS:def 1 :
theorem
canceled;
theorem Th5:
theorem Th6:
theorem Th7:
begin
:: deftheorem defines -bag UPROOTS:def 2 :
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
:: deftheorem Def3 defines Sum UPROOTS:def 3 :
:: deftheorem Def4 defines degree UPROOTS:def 4 :
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
begin
:: deftheorem Def5 defines non-zero UPROOTS:def 5 :
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
begin
:: deftheorem Def6 defines poly_shift UPROOTS:def 6 :
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
definition
let L be non
degenerated comRing;
let r be
Element of ;
let p be
Polynomial of
L;
assume A1:
r is_a_root_of p
;
func poly_quotient p,
r -> Polynomial of
L means :
Def7:
(
(len it) + 1
= len p & ( for
i being
Nat holds
it . i = eval (poly_shift p,(i + 1)),
r ) )
if len p > 0 otherwise it = 0_. L;
existence
( ( len p > 0 implies ex b1 being Polynomial of L st
( (len b1) + 1 = len p & ( for i being Nat holds b1 . i = eval (poly_shift p,(i + 1)),r ) ) ) & ( not len p > 0 implies ex b1 being Polynomial of L st b1 = 0_. L ) )
uniqueness
for b1, b2 being Polynomial of L holds
( ( len p > 0 & (len b1) + 1 = len p & ( for i being Nat holds b1 . i = eval (poly_shift p,(i + 1)),r ) & (len b2) + 1 = len p & ( for i being Nat holds b2 . i = eval (poly_shift p,(i + 1)),r ) implies b1 = b2 ) & ( not len p > 0 & b1 = 0_. L & b2 = 0_. L implies b1 = b2 ) )
consistency
for b1 being Polynomial of L holds verum
;
end;
:: deftheorem Def7 defines poly_quotient UPROOTS:def 7 :
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
Lm1:
now
let L be
domRing;
for p being non-zero Polynomial of L holds
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )let p be
non-zero Polynomial of
L;
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )defpred S1[
Nat]
means for
p being
Polynomial of
L st
len p = $1 holds
(
Roots p is
finite & ex
n being
Element of
NAT st
(
n = card (Roots p) &
n < len p ) );
p <> 0_. L
by Def5;
then
len p <> 0
by POLYNOM4:8;
then A1:
len p >= 0 + 1
by NAT_1:13;
A2:
for
n being
Nat st
n >= 1 &
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( n >= 1 & S1[n] implies S1[n + 1] )
assume that
n >= 1
and A3:
S1[
n]
;
S1[n + 1]
let p be
Polynomial of
L;
( len p = n + 1 implies ( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) ) )
assume A4:
len p = n + 1
;
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
per cases
( p is with_roots or not p is with_roots )
;
suppose
p is
with_roots
;
( Roots p is finite & ex n being Element of NAT st
( n = card (Roots p) & n < len p ) )
then consider x being
Element of
such that A5:
x is_a_root_of p
by POLYNOM5:def 7;
set r =
<%(- x),(1. L)%>;
set pq =
poly_quotient p,
x;
A6:
p = <%(- x),(1. L)%> *' (poly_quotient p,x)
by A5, Th52;
then A7:
Roots p = (Roots <%(- x),(1. L)%>) \/ (Roots (poly_quotient p,x))
by Th25;
A8:
Roots <%(- x),(1. L)%> = {x}
by Th50;
then reconsider Rr =
Roots <%(- x),(1. L)%> as
finite set ;
A9:
(len (poly_quotient p,x)) + 1
= len p
by A4, A5, Def7;
then consider k being
Element of
NAT such that A10:
k = card (Roots (poly_quotient p,x))
and A11:
k < len (poly_quotient p,x)
by A3, A4;
reconsider Rpq =
Roots (poly_quotient p,x) as
finite set by A3, A4, A9;
reconsider Rp =
Rpq \/ Rr as
finite set ;
card Rr = 1
by A8, CARD_1:50;
then A12:
card Rp <= k + 1
by A10, CARD_2:62;
Roots (poly_quotient p,x) is
finite
by A3, A4, A9;
hence
Roots p is
finite
by A8, A7;
ex n being Element of NAT st
( n = card (Roots p) & n < len p )take m =
card Rp;
( m = card (Roots p) & m < len p )thus
m = card (Roots p)
by A6, Th25;
m < len p
k + 1
< n + 1
by A4, A9, A11, XREAL_1:10;
hence
m < len p
by A4, A12, XXREAL_0:2;
verum
end;
end;
end;
A16:
S1[1]
for
n being
Nat st
n >= 1 holds
S1[
n]
from NAT_1:sch 8(A16, A2);
hence
(
Roots p is
finite & ex
n being
Element of
NAT st
(
n = card (Roots p) &
n < len p ) )
by A1;
verum
end;
begin
:: deftheorem Def8 defines multiplicity UPROOTS:def 8 :
theorem Th54:
theorem Th55:
:: deftheorem Def9 defines BRoots UPROOTS:def 9 :
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem
:: deftheorem Def10 defines fpoly_mult_root UPROOTS:def 10 :
:: deftheorem Def11 defines poly_with_roots UPROOTS:def 11 :
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem
theorem
theorem