let F be Field; :: thesis: for p, r being Polynomial of F
for q being non zero Polynomial of F holds
( (p + r) div q = (p div q) + (r div q) & (p + r) mod q = (p mod q) + (r mod q) )
let p, r be Polynomial of F; :: thesis: for q being non zero Polynomial of F holds
( (p + r) div q = (p div q) + (r div q) & (p + r) mod q = (p mod q) + (r mod q) )
let q be non zero Polynomial of F; :: thesis: ( (p + r) div q = (p div q) + (r div q) & (p + r) mod q = (p mod q) + (r mod q) )
H: q <> 0_. F ;
A: p + r = (((p div q) *' q) + (p mod q)) + r by div5
.= (((p div q) *' q) + (p mod q)) + (((r div q) *' q) + (r mod q)) by div5
.= ((p div q) *' q) + ((p mod q) + (((r div q) *' q) + (r mod q))) by POLYNOM3:26
.= ((p div q) *' q) + (((p mod q) + (r mod q)) + ((r div q) *' q)) by POLYNOM3:26
.= (((p div q) *' q) + ((r div q) *' q)) + ((p mod q) + (r mod q)) by POLYNOM3:26
.= (((p div q) + (r div q)) *' q) + ((p mod q) + (r mod q)) by POLYNOM3:32 ;
B: deg ((p mod q) + (r mod q)) <= max ((deg (p mod q)),(deg (r mod q))) by HURWITZ:22;
C: deg (p mod q) < deg q by RING_2:29;
deg (r mod q) < deg q by RING_2:29;
then max ((deg (p mod q)),(deg (r mod q))) < max ((deg q),(deg q)) by C, XXREAL_0:27;
then D: deg ((p mod q) + (r mod q)) < deg q by B, XXREAL_0:2;
hence (p + r) div q = (p div q) + (r div q) by A, H, HURWITZ:def 5; :: thesis: (p + r) mod q = (p mod q) + (r mod q)
thus (p + r) mod q = ((((p div q) + (r div q)) *' q) + ((p mod q) + (r mod q))) - (((p div q) + (r div q)) *' q) by D, A, H, HURWITZ:def 5
.= ((((p div q) + (r div q)) *' q) - (((p div q) + (r div q)) *' q)) + ((p mod q) + (r mod q)) by POLYNOM3:26
.= (0_. F) + ((p mod q) + (r mod q)) by POLYNOM3:29
.= (p mod q) + (r mod q) by POLYNOM3:28 ; :: thesis: verum