let t, u, z be Integer; :: thesis: (t + (u * z)) gcd z = t gcd z
A0: ( z <= 0 implies (t + (u * z)) gcd z = t gcd z )

proof

assume A1: z <= 0 ; :: thesis: (t + (u * z)) gcd z = t gcd z
then A1a: - z in NAT by INT_1:3;

per cases ( t >= 0 or t < 0 ) ;

suppose t >= 0 ; :: thesis: (t + (u * z)) gcd z = t gcd z

then A2: ( t in NAT & - z in NAT ) by A1, INT_1:3;
(t + (u * z)) gcd z = (t + ((- u) * (- z))) gcd (- z) by Th1
.= t gcd (- z) by A2, Lm0c ;
hence (t + (u * z)) gcd z = t gcd z by Th1; :: thesis: verum

end;

suppose t < 0 ; :: thesis: (t + (u * z)) gcd z = t gcd z

then A3: - t in NAT by INT_1:3;
(t + (u * z)) gcd z = (- ((- t) - (u * z))) gcd (- z) by Th1
.= ((- t) + (u * (- z))) gcd (- z) by Th1
.= (- t) gcd (- z) by A1a, A3, Lm0c
.= (- t) gcd z by Th1
.= t gcd z by Th1 ;
hence (t + (u * z)) gcd z = t gcd z ; :: thesis: verum

end;

end;

end;

( z > 0 implies (t + (u * z)) gcd z = t gcd z )

proof

assume A1: z > 0 ; :: thesis: (t + (u * z)) gcd z = t gcd z
then A1a: z in NAT by INT_1:3;

per cases ( t >= 0 or t < 0 ) ;

suppose t >= 0 ; :: thesis: (t + (u * z)) gcd z = t gcd z

then ( t in NAT & z in NAT ) by A1, INT_1:3;
hence (t + (u * z)) gcd z = t gcd z by Lm0c; :: thesis: verum

end;

suppose t < 0 ; :: thesis: (t + (u * z)) gcd z = t gcd z

then A3: - t in NAT by INT_1:3;
(t + (u * z)) gcd z = (- ((- t) - (u * z))) gcd z
.= ((- t) + ((- u) * z)) gcd z by Th1
.= (- t) gcd z by A1a, A3, Lm0c
.= t gcd z by Th1 ;
hence (t + (u * z)) gcd z = t gcd z ; :: thesis: verum

end;

end;

end;

hence (t + (u * z)) gcd z = t gcd z by A0; :: thesis: verum