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

for a being Element of R holds

( multiplicity (p,a) = 0 iff not rpoly (1,a) divides p )

let p be non zero Polynomial of R; :: thesis: for a being Element of R holds

( multiplicity (p,a) = 0 iff not rpoly (1,a) divides p )

let a be Element of R; :: thesis: ( multiplicity (p,a) = 0 iff not rpoly (1,a) divides p )

for a being Element of R holds

( multiplicity (p,a) = 0 iff not rpoly (1,a) divides p )

let p be non zero Polynomial of R; :: thesis: for a being Element of R holds

( multiplicity (p,a) = 0 iff not rpoly (1,a) divides p )

let a be Element of R; :: thesis: ( multiplicity (p,a) = 0 iff not rpoly (1,a) divides p )

A: now :: thesis: ( multiplicity (p,a) = 0 implies not rpoly (1,a) divides p )

assume
multiplicity (p,a) = 0
; :: thesis: not rpoly (1,a) divides p

then C: not a is_a_root_of p by UPROOTS:52;

end;then C: not a is_a_root_of p by UPROOTS:52;

now :: thesis: not rpoly (1,a) divides p

hence
not rpoly (1,a) divides p
; :: thesis: verumassume
rpoly (1,a) divides p
; :: thesis: contradiction

then consider s being Polynomial of R such that

B: p = (rpoly (1,a)) *' s by RING_4:1;

thus contradiction by C, B, prl2, HURWITZ:30; :: thesis: verum

end;then consider s being Polynomial of R such that

B: p = (rpoly (1,a)) *' s by RING_4:1;

thus contradiction by C, B, prl2, HURWITZ:30; :: thesis: verum

now :: thesis: ( multiplicity (p,a) <> 0 implies rpoly (1,a) divides p )

hence
( multiplicity (p,a) = 0 iff not rpoly (1,a) divides p )
by A; :: thesis: verumassume
multiplicity (p,a) <> 0
; :: thesis: rpoly (1,a) divides p

then (multiplicity (p,a)) + 1 > 0 + 1 by XREAL_1:6;

then multiplicity (p,a) >= 1 by NAT_1:13;

then ex s being Polynomial of R st p = (rpoly (1,a)) *' s by UPROOTS:52, HURWITZ:33;

hence rpoly (1,a) divides p by RING_4:1; :: thesis: verum

end;then (multiplicity (p,a)) + 1 > 0 + 1 by XREAL_1:6;

then multiplicity (p,a) >= 1 by NAT_1:13;

then ex s being Polynomial of R st p = (rpoly (1,a)) *' s by UPROOTS:52, HURWITZ:33;

hence rpoly (1,a) divides p by RING_4:1; :: thesis: verum