let a, b be Nat; :: thesis: for x being Integer st a <> 0 holds
(a + (x * b)) gcd b = a gcd b
let xx be Integer; :: thesis: ( a <> 0 implies (a + (xx * b)) gcd b = a gcd b )
set i = a gcd b;
A1: b = abs b by ABSVALUE:def 1;
assume A2: a <> 0 ; :: thesis: (a + (xx * b)) gcd b = a gcd b
A3: for m being Nat st m divides abs (a + (xx * b)) & m divides abs b holds
m divides a gcd b

proof

let mm be Nat; :: thesis: ( mm divides abs (a + (xx * b)) & mm divides abs b implies mm divides a gcd b )
assume that
A4: mm divides abs (a + (xx * b)) and
A5: mm divides abs b ; :: thesis: mm divides a gcd b
consider n being Nat such that
A6: b = mm * n by A1, A5, NAT_D:def 3;
reconsider mm = mm as Element of NAT by ORDINAL1:def 13;

now

per cases ( a + (xx * b) >= 0 or a + (xx * b) < 0 ) ;

suppose a + (xx * b) >= 0 ; :: thesis: mm divides a

then abs (a + (xx * b)) = a + (xx * b) by ABSVALUE:def 1;
then consider t being Integer such that
A7: a + (xx * b) = mm * t by A4, INT_1:def 9;
A8: a = (mm * t) - (mm * (xx * n)) by A6, A7, XCMPLX_1:26
.= mm * (t - (xx * n)) ;
then t - (xx * n) >= 0 by A2;
then reconsider tt = t - (xx * n) as Element of NAT by INT_1:16;
a = mm * tt by A8;
hence mm divides a by NAT_D:def 3; :: thesis: verum

end;

suppose a + (xx * b) < 0 ; :: thesis: mm divides a

then abs (a + (xx * b)) = - (a + (xx * b)) by ABSVALUE:def 1;
then consider t being Integer such that
A9: - (a + (xx * b)) = mm * t by A4, INT_1:def 9;
A10: a = (- (mm * t)) - (mm * (xx * n)) by A6, A9, XCMPLX_1:26
.= mm * ((- t) - (xx * n)) ;
then (- t) - (xx * n) >= 0 by A2;
then reconsider tt = (- t) - (xx * n) as Element of NAT by INT_1:16;
a = mm * tt by A10;
hence mm divides a by NAT_D:def 3; :: thesis: verum

end;

end;

end;

hence mm divides a gcd b by A1, A5, NEWTON:63; :: thesis: verum

end;

a gcd b divides a by NAT_D:def 5;
then A11: a = (a gcd b) * (a div (a gcd b)) by NAT_D:3;
A12: a gcd b divides b by NAT_D:def 5;
then A13: b = (a gcd b) * (b div (a gcd b)) by NAT_D:3;
a gcd b divides abs (a + (xx * b))

proof

per cases ( a + (xx * b) < 0 or a + (xx * b) >= 0 ) ;

suppose a + (xx * b) < 0 ; :: thesis: a gcd b divides abs (a + (xx * b))

then A14: abs (a + (xx * b)) = - (a + (xx * b)) by ABSVALUE:def 1;
- (a + (xx * b)) = (a gcd b) * (- ((a div (a gcd b)) + (xx * (b div (a gcd b))))) by A11, A13;
hence a gcd b divides abs (a + (xx * b)) by A14, INT_1:def 9; :: thesis: verum

end;

suppose a + (xx * b) >= 0 ; :: thesis: a gcd b divides abs (a + (xx * b))

then A15: abs (a + (xx * b)) = a + (xx * b) by ABSVALUE:def 1;
a + (xx * b) = (a gcd b) * ((a div (a gcd b)) + (xx * (b div (a gcd b)))) by A11, A13;
hence a gcd b divides abs (a + (xx * b)) by A15, INT_1:def 9; :: thesis: verum

end;

end;

end;

then (abs (a + (xx * b))) gcd (abs b) = a gcd b by A1, A12, A3, NAT_D:def 5;
hence (a + (xx * b)) gcd b = a gcd b by INT_2:51; :: thesis: verum