let p, q, t, z be Integer; :: thesis: p + q divides (p * ((t * (p + q)) + z)) + (q * z)
A1: z = ((q * t) * 0) + z ;
(p * (t * (p + q))) + (q * (t * 0)) = ((p * t) * (p + q)) + ((q * t) * 0) ;
hence p + q divides (p * ((t * (p + q)) + z)) + (q * z) by A1, INT_1:def 3, Th29; :: thesis: verum