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 )
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;
now :: thesis: not rpoly (1,a) divides p
assume 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;
hence not rpoly (1,a) divides p ; :: thesis: verum
end;
now :: thesis: ( multiplicity (p,a) <> 0 implies rpoly (1,a) divides p )
assume 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;
hence ( multiplicity (p,a) = 0 iff not rpoly (1,a) divides p ) by A; :: thesis: verum