let a, b be Nat; :: thesis: for x being Integer st a <> 0 & b <> 0 holds
(a + (x * b)) gcd b = a gcd b
let xx be Integer; :: thesis: ( a <> 0 & b <> 0 implies (a + (xx * b)) gcd b = a gcd b )
assume ( a <> 0 & b <> 0 ) ; :: thesis: (a + (xx * b)) gcd b = a gcd b
then A1: ( a > 0 & b > 0 ) ;
set i = a gcd b;
A2: ( a = abs a & b = abs b ) by ABSVALUE:def 1;
A3: ( a gcd b divides a & a gcd b divides b ) by NAT_D:def 5;
then A4: ( a = (a gcd b) * (a div (a gcd b)) & b = (a gcd b) * (b div (a gcd b)) ) by NAT_D:3;
A5: 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 A6: 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 A4;
hence a gcd b divides abs (a + (xx * b)) by A6, INT_1:def 9; :: thesis: verum

end;

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

then A7: 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 A4;
hence a gcd b divides abs (a + (xx * b)) by A7, INT_1:def 9; :: thesis: verum

end;

end;

end;

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 A8: ( mm divides abs (a + (xx * b)) & mm divides abs b ) ; :: thesis: mm divides a gcd b
then consider n being Nat such that
A9: b = mm * n by A2, 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
A10: a + (xx * b) = mm * t by A8, INT_1:def 9;
A11: a = (mm * t) - (mm * (xx * n)) by A9, A10, XCMPLX_1:26
.= mm * (t - (xx * n)) ;
then t - (xx * n) >= 0 by A1;
then reconsider tt = t - (xx * n) as Element of NAT by INT_1:16;
a = mm * tt by A11;
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
A12: - (a + (xx * b)) = mm * t by A8, INT_1:def 9;
A13: a = (- (mm * t)) - (mm * (xx * n)) by A9, A12, XCMPLX_1:26
.= mm * ((- t) - (xx * n)) ;
then (- t) - (xx * n) >= 0 by A1;
then reconsider tt = (- t) - (xx * n) as Element of NAT by INT_1:16;
a = mm * tt by A13;
hence mm divides a by NAT_D:def 3; :: thesis: verum

end;

end;

end;

hence mm divides a gcd b by A2, A8, NEWTON:63; :: thesis: verum

end;

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