let L be non degenerated comRing; :: thesis: for p being non-zero Polynomial of L

for x being Element of L holds

( x is_a_root_of p iff multiplicity (p,x) >= 1 )

let p be non-zero Polynomial of L; :: thesis: for x being Element of L holds

( x is_a_root_of p iff multiplicity (p,x) >= 1 )

let x be Element of L; :: thesis: ( x is_a_root_of p iff multiplicity (p,x) >= 1 )

set r = <%(- x),(1. L)%>;

set m = multiplicity (p,x);

consider F being non empty finite Subset of NAT such that

A1: F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } and

A2: multiplicity (p,x) = max F by Def7;

multiplicity (p,x) in F by A2, XXREAL_2:def 8;

then consider k being Element of NAT such that

A3: multiplicity (p,x) = k and

A4: ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q by A1;

A6: p = (<%(- x),(1. L)%> `^ k) *' q by A4;

assume multiplicity (p,x) >= 1 ; :: thesis: x is_a_root_of p

then consider k1 being Nat such that

A7: k = k1 + 1 by A3, NAT_1:6;

reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;

p = (<%(- x),(1. L)%> *' (<%(- x),(1. L)%> `^ k1)) *' q by A6, A7, POLYNOM5:19

.= <%(- x),(1. L)%> *' ((<%(- x),(1. L)%> `^ k1) *' q) by POLYNOM3:33 ;

hence x is_a_root_of p by Th46; :: thesis: verum

for x being Element of L holds

( x is_a_root_of p iff multiplicity (p,x) >= 1 )

let p be non-zero Polynomial of L; :: thesis: for x being Element of L holds

( x is_a_root_of p iff multiplicity (p,x) >= 1 )

let x be Element of L; :: thesis: ( x is_a_root_of p iff multiplicity (p,x) >= 1 )

set r = <%(- x),(1. L)%>;

set m = multiplicity (p,x);

consider F being non empty finite Subset of NAT such that

A1: F = { k where k is Element of NAT : ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q } and

A2: multiplicity (p,x) = max F by Def7;

multiplicity (p,x) in F by A2, XXREAL_2:def 8;

then consider k being Element of NAT such that

A3: multiplicity (p,x) = k and

A4: ex q being Polynomial of L st p = (<%(- x),(1. L)%> `^ k) *' q by A1;

hereby :: thesis: ( multiplicity (p,x) >= 1 implies x is_a_root_of p )

consider q being Polynomial of L such that assume
x is_a_root_of p
; :: thesis: multiplicity (p,x) >= 1

then A5: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by Th47;

<%(- x),(1. L)%> `^ 1 = <%(- x),(1. L)%> by POLYNOM5:16;

then 1 in F by A1, A5;

hence multiplicity (p,x) >= 1 by A2, XXREAL_2:def 8; :: thesis: verum

end;then A5: p = <%(- x),(1. L)%> *' (poly_quotient (p,x)) by Th47;

<%(- x),(1. L)%> `^ 1 = <%(- x),(1. L)%> by POLYNOM5:16;

then 1 in F by A1, A5;

hence multiplicity (p,x) >= 1 by A2, XXREAL_2:def 8; :: thesis: verum

A6: p = (<%(- x),(1. L)%> `^ k) *' q by A4;

assume multiplicity (p,x) >= 1 ; :: thesis: x is_a_root_of p

then consider k1 being Nat such that

A7: k = k1 + 1 by A3, NAT_1:6;

reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;

p = (<%(- x),(1. L)%> *' (<%(- x),(1. L)%> `^ k1)) *' q by A6, A7, POLYNOM5:19

.= <%(- x),(1. L)%> *' ((<%(- x),(1. L)%> `^ k1) *' q) by POLYNOM3:33 ;

hence x is_a_root_of p by Th46; :: thesis: verum