let i1, i2, i3 be Integer; :: thesis: ( i1,i2 are_congruent_mod i3 implies i1 gcd i3 = i2 gcd i3 )
set d = i2 gcd i3;
reconsider d = i2 gcd i3 as Nat ;
assume i1,i2 are_congruent_mod i3 ; :: thesis: i1 gcd i3 = i2 gcd i3
then i3 divides i1 - i2 by INT_2:15;
then consider i being Integer such that
A1: i1 - i2 = i3 * i by INT_1:def 3;
A2: d = (abs i2) gcd (abs i3) by INT_2:34;
then d divides abs i2 by NAT_D:def 5;
then abs d divides abs i2 by ABSVALUE:def 1;
then A3: d divides i2 by INT_2:16;
A4: i2 = i1 - (i3 * i) by A1;
A5: for n being Nat st n divides abs i1 & n divides abs i3 holds
n divides d

proof

let n be Nat; :: thesis: ( n divides abs i1 & n divides abs i3 implies n divides d )
assume that
A6: n divides abs i1 and
A7: n divides abs i3 ; :: thesis: n divides d
abs n divides abs i3 by A7, ABSVALUE:def 1;
then n divides i3 by INT_2:16;
then A8: n divides i3 * i by INT_2:2;
abs n divides abs i1 by A6, ABSVALUE:def 1;
then n divides i1 by INT_2:16;
then n divides i2 by A4, A8, Lm4;
then abs n divides abs i2 by INT_2:16;
then n divides abs i2 by ABSVALUE:def 1;
hence n divides d by A2, A7, NAT_D:def 5; :: thesis: verum

end;

A9: d divides abs i3 by A2, NAT_D:def 5;
then abs d divides abs i3 by ABSVALUE:def 1;
then d divides i3 by INT_2:16;
then A10: d divides i3 * i by INT_2:2;
i1 = (i3 * i) + i2 by A1;
then ( abs d = d & d divides i1 ) by A3, A10, ABSVALUE:def 1, WSIERP_1:4;
then d divides abs i1 by INT_2:16;
then (abs i1) gcd (abs i3) = d by A9, A5, NAT_D:def 5;
hence i1 gcd i3 = i2 gcd i3 by INT_2:34; :: thesis: verum