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 )

A0: ( z <= 0 implies (t + (u * z)) gcd z = t gcd z )

proof

( z > 0 implies (t + (u * z)) gcd z = t gcd z )
assume A1:
z <= 0
; :: thesis: (t + (u * z)) gcd z = t gcd z

then A1a: - z in NAT by INT_1:3;

end;then A1a: - z in NAT by INT_1:3;

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

end;

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;(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

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;(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

proof

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

then A1a: z in NAT by INT_1:3;

end;then A1a: z in NAT by INT_1:3;