let F be Field; :: thesis: for p being non zero Polynomial of F
for a being Element of F
for n being Element of NAT holds
( (X- a) `^ n divides p iff multiplicity (p,a) >= n )
let p be non zero Polynomial of F; :: thesis: for a being Element of F
for n being Element of NAT holds
( (X- a) `^ n divides p iff multiplicity (p,a) >= n )
let a be Element of F; :: thesis: for n being Element of NAT holds
( (X- a) `^ n divides p iff multiplicity (p,a) >= n )
let n be Element of NAT ; :: thesis: ( (X- a) `^ n divides p iff multiplicity (p,a) >= n )
set m = multiplicity (p,a);
H: ( (X- a) `^ (multiplicity (p,a)) divides p & not (X- a) `^ ((multiplicity (p,a)) + 1) divides p ) by FIELD_14:67;

now :: thesis: ( (X- a) `^ n divides p implies multiplicity (p,a) >= n )

assume B: (X- a) `^ n divides p ; :: thesis: multiplicity (p,a) >= n

now :: thesis: not multiplicity (p,a) < n

assume multiplicity (p,a) < n ; :: thesis: contradiction
then (multiplicity (p,a)) + 1 <= n by INT_1:7;
hence contradiction by H, B, FIELD_14:40; :: thesis: verum

end;

hence multiplicity (p,a) >= n ; :: thesis: verum

end;

hence ( (X- a) `^ n divides p iff multiplicity (p,a) >= n ) by H, FIELD_14:40; :: thesis: verum