let n be Nat; :: thesis: for R being domRing
for p being non zero Polynomial of R
for a being Element of R holds
( multiplicity (p,a) = n iff ( (rpoly (1,a)) `^ n divides p & not (rpoly (1,a)) `^ (n + 1) divides p ) )
let R be domRing; :: thesis: for p being non zero Polynomial of R
for a being Element of R holds
( multiplicity (p,a) = n iff ( (rpoly (1,a)) `^ n divides p & not (rpoly (1,a)) `^ (n + 1) divides p ) )
let p be non zero Polynomial of R; :: thesis: for a being Element of R holds
( multiplicity (p,a) = n iff ( (rpoly (1,a)) `^ n divides p & not (rpoly (1,a)) `^ (n + 1) divides p ) )
let a be Element of R; :: thesis: ( multiplicity (p,a) = n iff ( (rpoly (1,a)) `^ n divides p & not (rpoly (1,a)) `^ (n + 1) divides p ) )

A: now :: thesis: ( multiplicity (p,a) = n implies ( (rpoly (1,a)) `^ n divides p & not (rpoly (1,a)) `^ (n + 1) divides p ) )

assume multiplicity (p,a) = n ; :: thesis: ( (rpoly (1,a)) `^ n divides p & not (rpoly (1,a)) `^ (n + 1) divides p )
then consider F being non empty finite Subset of NAT such that
B: ( F = { k where k is Element of NAT : ex q being Polynomial of R st p = (<%(- a),(1. R)%> `^ k) *' q } & n = max F ) by UPROOTS:def 8;
n in F by B, XXREAL_2:def 6;
then consider k being Element of NAT such that
C: ( k = n & ex q being Polynomial of R st p = (<%(- a),(1. R)%> `^ k) *' q ) by B;
consider q being Polynomial of R such that
D: p = (<%(- a),(1. R)%> `^ n) *' q by C;
p = ((rpoly (1,a)) `^ n) *' q by D, repr;
hence (rpoly (1,a)) `^ n divides p by RING_4:1; :: thesis: not (rpoly (1,a)) `^ (n + 1) divides p
F: n is UpperBound of F by B, XXREAL_2:def 3;

now :: thesis: not (rpoly (1,a)) `^ (n + 1) divides p

assume (rpoly (1,a)) `^ (n + 1) divides p ; :: thesis: contradiction
then consider q being Polynomial of R such that
E: p = ((rpoly (1,a)) `^ (n + 1)) *' q by RING_4:1;
p = (<%(- a),(1. R)%> `^ (n + 1)) *' q by E, repr;
then n + 1 in F by B;
hence contradiction by F, XXREAL_2:def 1, NAT_1:16; :: thesis: verum

end;

hence not (rpoly (1,a)) `^ (n + 1) divides p ; :: thesis: verum

end;

now :: thesis: ( (rpoly (1,a)) `^ n divides p & not (rpoly (1,a)) `^ (n + 1) divides p implies multiplicity (p,a) = n )

assume X: ( (rpoly (1,a)) `^ n divides p & not (rpoly (1,a)) `^ (n + 1) divides p ) ; :: thesis: multiplicity (p,a) = n
set n0 = multiplicity (p,a);
consider F being non empty finite Subset of NAT such that
B: ( F = { k where k is Element of NAT : ex q being Polynomial of R st p = (<%(- a),(1. R)%> `^ k) *' q } & multiplicity (p,a) = max F ) by UPROOTS:def 8;
consider q being Polynomial of R such that
E: p = ((rpoly (1,a)) `^ n) *' q by X, RING_4:1;
K: n in NAT by ORDINAL1:def 12;
p = (<%(- a),(1. R)%> `^ n) *' q by E, repr;
then C: n in F by B, K;

now :: thesis: for k being ExtReal st k in F holds
k <= n

let k be ExtReal; :: thesis: ( k in F implies k <= n )
assume k in F ; :: thesis: k <= n
then consider k0 being Element of NAT such that
C: ( k0 = k & ex q being Polynomial of R st p = (<%(- a),(1. R)%> `^ k0) *' q ) by B;
consider q being Polynomial of R such that
D: p = (<%(- a),(1. R)%> `^ k0) *' q by C;

now :: thesis: not k0 >= n + 1

assume k0 >= n + 1 ; :: thesis: contradiction
then consider j being Nat such that
E: k0 = (n + 1) + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
p = ((rpoly (1,a)) `^ k0) *' q by D, repr
.= (((rpoly (1,a)) `^ (n + 1)) *' ((rpoly (1,a)) `^ j)) *' q by E, UPROOTS:30
.= ((rpoly (1,a)) `^ (n + 1)) *' (((rpoly (1,a)) `^ j) *' q) by POLYNOM3:33 ;
hence contradiction by X, RING_4:1; :: thesis: verum

end;

hence k <= n by C, NAT_1:13; :: thesis: verum

end;

hence multiplicity (p,a) = n by B, C, XXREAL_2:def 8; :: thesis: verum

end;

hence ( multiplicity (p,a) = n iff ( (rpoly (1,a)) `^ n divides p & not (rpoly (1,a)) `^ (n + 1) divides p ) ) by A; :: thesis: verum