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

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;

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

hence
not (rpoly (1,a)) `^ (n + 1) divides p
; :: thesis: verumassume
(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;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

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

hence
( multiplicity (p,a) = n iff ( (rpoly (1,a)) `^ n divides p & not (rpoly (1,a)) `^ (n + 1) divides p ) )
by A; :: thesis: verumassume 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;

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

hence
multiplicity (p,a) = n
by B, C, XXREAL_2:def 8; :: thesis: verumk <= 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;

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

hence
k <= n
by C, NAT_1:13; :: thesis: verumassume
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;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