let L be Field; :: thesis: for p being Polynomial of L
for q being non zero Polynomial of L holds deg (p mod q) < deg q
let p be Polynomial of L; :: thesis: for q being non zero Polynomial of L holds deg (p mod q) < deg q
let q be non zero Polynomial of L; :: thesis: deg (p mod q) < deg q
set u = p div q;
q <> 0_. L ;
then consider r being Polynomial of L such that
A: ( p = ((p div q) *' q) + r & deg r < deg q ) by HURWITZ:def 5;
p mod q = p - ((p div q) *' q) by HURWITZ:def 6
.= (((p div q) *' q) + r) + (- ((p div q) *' q)) by A, POLYNOM3:def 6
.= (((p div q) *' q) + (- ((p div q) *' q))) + r by POLYNOM3:26
.= (((p div q) *' q) - ((p div q) *' q)) + r by POLYNOM3:def 6
.= (0_. L) + r by POLYNOM3:29
.= r by POLYNOM3:28 ;
hence deg (p mod q) < deg q by A; :: thesis: verum