let L be non degenerated comRing; 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; for x being Element of L holds
( x is_a_root_of p iff multiplicity (p,x) >= 1 )
let x be Element of L; ( 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;
consider q being Polynomial of L such that
A6:
p = (<%(- x),(1. L)%> `^ k) *' q
by A4;
assume
multiplicity (p,x) >= 1
; 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; verum